`Relation.Binary.Definitions._Respects₂_` seems to exchange 'left' and 'right' in its left/right projections?

agda / agda-stdlib

The Agda standard library

https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary

Other

585 stars 237 forks source link

`Relation.Binary.Definitions._Respects₂_` seems to exchange 'left' and 'right' in its left/right projections? #2471

Open jamesmckinna opened 2 months ago

jamesmckinna commented 2 months ago

The definition:

-- Respecting - relatedness is preserved on both sides by equality

_Respects₂_ : Rel A ℓ₁ → Rel A ℓ₂ → Set _
P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_)

has

left component the proof of _Respectsʳ_
right component that of _Respectsˡ_

This seems a like bug (cognitive dissonance at the very least). Worth fixing?

JacquesCarette commented 2 months ago

I definitely think so. Breaking as it might be.

jamesmckinna commented 2 months ago

One way to tackle breaking would be to have an interim v2.2-badged PR which introduces, say, _Respects²_, and deprecates _Respects₂_ in its favour, ahead of agreeing a/the 'right' name (possibly the original? I'm not thrilled by it...) for v3.0?