Orders without equivalence relations

[laMudri]

Sometimes we come across types which naturally have an order, but for which the appropriate equivalence relation is, intensionally, the intersection of the order and its inverse. For example, if we have types about which we only care about inhabitedness (propositions), then the order is given by →, while the equivalence relation is given by bi-implication. Giving this definition using Poset from Relation.Binary is annoying because we have to prove reflexivity and transitivity for implication, then prove them twice more for equivalence, and then give (simple, but slightly tedious) proofs of symmetry and antisymmetry.

It would be nice if there were some general code to take a type with a reflexive transitive relation and produce the corresponding poset. Could the structure be slotted into the Relation.Binary hierarchy, perhaps even before Setoid, together with the construction suggested above? I've occasionally heard the term “proset” used for a partially ordered set without an equivalence relation, though nLab doesn't distinguish this from partially ordered sets in the normal sense.

[gallais]

I suppose we could have something like:

http://agda.github.io/agda-stdlib/Relation.Binary.Construct.Closure.Equivalence.html

[MatthewDaggitt]

Yup adding a Construct module seems to be the right way to go about it.

[laMudri]

See #2071.

[jamesmckinna]

'Inverse' or 'converse' relation?
One reason I'm less happy on the PR with 'core groupoid' as justification for the terminology 'core' is that you're not actually inverting anything here, are you, in the sense of having left- and right- inverses to an arrow? (Or are you, if I squint hard enough?)

Calling the opposite/converse of a relation 'inverse' seems... perverse, to me at least.

[jamesmckinna]

As for the lexicon shift from core to interior (as a dual to closure, in the context of topology originally, AFAIK):

Just as the P-closure of a relation R for some property P is the least relation S containing R such that P S, the P-interior is the dual notion, vs. the greatest relation S contained in R such that P S, for any suitable P.

This issue/PR addresses the case P = Symmetric.

For a citation, and some sufficient conditions on P to be 'suitable', you could look at the treatment of 'intersection-closed' and 'union-closed' families of sets/predicates/relations defined in Paul M. Cohn's "Universal Algebra" (1965) and their application to defining closures and interiors, and inductive/coinductive definitions generally (see also Peter Aczel's article on inductive definitions in the Handbook of Mathematical Logic (1977) (ISBN: 9780720422856)). NB impredicative definitions! (cf. Tarski's proof of his fixed-point theorem)

Being Symmetric is, IIRC, an example of a property which is both intersection- and union-closed, and hence has a corresponding closure and interior, as here.

[jamesmckinna]

Regarding the introduction (and subsequent removal;-)) of Proset from the Relation.Bundle hierarchy, suggest that any such proposal file under the hypothetical-rewrite milestone. I think there's potential for it, but as @MatthewDaggitt points out on #2071 such a thing would involve a (much!) large(r)-scale reconsideration of many things, so, for good or bad, IMHO should wait for such time as we have time/person-power to undertake that...

[jamesmckinna]

Has this issue been successfully closed by #2071 ?

[JacquesCarette]

It doesn't look like #2071 closes this, it 'only' provides the underlying machinery to get there. It feels like this new machinery should get actively used in combinators to make one's life easier, as per the original issue.