Split `Equality` and `Order` out of `Relation.Binary`

[MatthewDaggitt]

Okay, the AIM discussion on Monday and reviewing #1760 has crystallised something in my mind.

Relation.Binary is fundamentally different from Relation.Unary and Relation.Nullary as it contains hierarchies for both equalities and orderings. I was reviewing #1760 and was about to suggest that we add a ton of more stuff to do with Galois connections under Relation.Binary which seems totally the wrong place for it, but at the same time the only sensible place for it under the current structure.

Proposal: break out the two hierarchies in Relation.Binary into new top-level modules Equality and Order respectively, to give them parity with Function and Algebra hierarchies. e.g. we would have (Order/Equality).(Definitions/Structures/Bundles).

Consequences

• to import IsEquivalence, Setoid etc., you would use Equality instead of Relation.Binary
• to import IsPreorder, Preorder, Poset, etc. you would use Order instead of Relation.Binary
• to import _≡_, refl etc. you would use Equality.Propositional instead of Relation.Binary.PropositionalEquality

Advantages

• Makes it far easier for new users to find equality, arguably the first thing they need and look for.
• Typing open import Relation.Binary.PropositionalEquality in every module is frankly a pain in the neck. open import Equality.Propositional is much shorter.
• Order theory is a rich area, and this would provide a dedicated top-level folder for it.
• Separates out orderings from equality.
• Much lighter dependencies for equalities, as you are no longer forced to import a load of order theory as well.

Obviously we would maintain backwards compatibility for such a big change, by having the existing Relation.Binary(.Structures/Bundles) re-export all the content of the new modules.

What are people's thoughts?

[jespercockx]

I am very much in favour of this proposal! I'm already looking forward to the last day I have to type out Relation.Binary.PropositionalEquality in full :)

[sstucki]

I like the idea, but boy is it going to break backwards compatibility! 😉

That being said, I think people are generally used to the library being in flux at this point. (At least I've heard statements to that effect from many Agda users around me.) So breaking changes might not be as big a deal as one might at first assume.

So 👍 from me.

[MatthewDaggitt]

I like the idea, but boy is it going to break backwards compatibility!

@sstucki can you explain why it would? As mentioned before, the modules Relation.Binary/Relation.Binary.Structures etc. will still exist and will publicly re-export the same content from their new location. Some of the existing modules may have deprecation warnings attached, but I don't think any code should actively break?

[jamesmckinna]

In principle, this seems like a useful/well-motivated change. And as with recent changes I helped push through, I'm not necessarily against breaking changes. That's usually what I expect from a major version bump, even given the maintainers' heroic (truly!) efforts in maintaining deprecation warnings and so forth.

That said, I'm not clear about the various import dependencies (esp. on ...Properties) and ...Definitions) when it comes to proving results about relations (such as reflexive-transitive closures of reduction relations in semantics) which, while they are surely Preorders, that structure is not the 'interesting' structure at hand. Would I now need to import Order.* in order to talk about transitivity? Where would relations which aren't either equivalences or preorders, eg PERs, or uniformities in topology, now belong? Etc.
ADDED sorry if this remark seems stupid; those things have to be imported from somewhere, obviously. But the neutrality of Relation.Binary enjoys (well: YMMV ;-)) the cognitive/conceptual advantage that it brings no baggage with it... and the proposal makes the case for "no, we'd really like stdlib to carry some baggage (of conceptual/structuring expectations) around, because this (cognitively) optimises for the common case", which as I said above, seems (potentially) useful/well-motivated.

[sstucki]

@sstucki can you explain why it would? [...] Some of the existing modules may have deprecation warnings attached, but I don't think any code should actively break?

Yes, sorry, bad wording on my part. I guess "boy will this cause deprecation warnings" would be more accurate.

[MatthewDaggitt]

That said, I'm not clear about the various import dependencies (esp. on ...Properties) and ...Definitions) when it comes to proving results about relations (such as reflexive-transitive closures of reduction relations in semantics) which, while they are surely Preorders, that structure is not the 'interesting' structure at hand. Would I now need to import Order.* in order to talk about transitivity?

This is an excellent question and something I'd been thinking about as well. I think the answer is that we'd keep Relation.Binary.Definitions as is (although probably merging with Relation.Binary), because as you say all these definitions make sense outside of a context of the order. Then Order.Definitions and Equality.Definitions would publicly re-export the relevant ones?

Where would relations which aren't either equivalences or preorders, eg PERs, or uniformities in topology, now belong? Etc.

I would imagine that PERs would move into Equality as well. If a serious amount of topology was then added, I think it would indicate the need for a new top-level folder Topology? Does that make sense to you?

[jamesmckinna]

Thanks Matthew, I always like to have asked an "excellent" question (:blush:), especially if/when I don't already know the/my preferred answer ;-)

Regarding PER moving with Equality... I suppose so, although I'm not sure... do we have much development of PERs yet? (Perhaps they don't need much?) Would that end up under Equality.Partial.*? Maybe that's fine; and/because memorable... part of the cognitive load/availability that users have to share with stdlib lies in maintaining that balance...

Regarding 'other' kinds of Binary relations: yes, I guess they might float up to the top level once they have proved their worth. Perhaps we don't (yet) have much Topology is because the classical notions are notoriously... delicate... as to constructivisation, wrt impredicativity, and points, among other things. So my 'objection', such as it is, might be considered moot, for the time being. (And with it, any other discussion of 'a library for now' vs. 'a library for all time', cf. Bourbaki)

[nad]

I think you should be very careful about starting to use new top-level module names like Equality, at least until issue agda/agda#4029 has been fixed.

I have another library with modules like Equality and Equality.Propositional. This library and some other developments that make use of it contain something like 400 modules, and the library imports the standard library. If the standard library starts using Equality.Propositional (say), then my library stops working.

[MatthewDaggitt]

Okay marking this blocked upstream by agda/agda#4029