search

agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
585 stars 237 forks source link

Missing structure/bundle in the `Relation.Binary.*` hierarchy? #2482

Closed jamesmckinna closed 1 month ago

jamesmckinna commented 2 months ago

We don't seem to define as IsDecPreorder an independent entity 'between' IsPreorder and IsTotalPreorder... and the associated bundle.

Should we?

JacquesCarette commented 2 months ago

I thought that all the IsDec* properties were parallel, not 'in between' ? Or maybe there is an implication that I am missing?

jamesmckinna commented 2 months ago

Perhaps I phrased things badly... the 'betweennness' refers both to the hierarchical addition of structure, and also to the way the things are literally defined, with each relational structure/bundle introduced in its fully general, and then immediately followed by its (Is)Dec form... ... so indeed the (Is)Dec* properties do define a parallel hierarchy, except that IsDecPreorder is missing: it does not appear after IsPreorder: rather, only IsTotalPreorder is defined after IsPreorder... ... and AFAICR, IsTotalPreorder doesn't imply decidability?

JacquesCarette commented 2 months ago

In which case, yes, we should definitely add it, it looks like a pure 'oops' omission.