agda-stdlib
agda-stdlib copied to clipboard
agda
`Relation.Binary.Definitions._Respects₂_` seems to exchange 'left' and 'right' in its left/right projections?
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?
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?
Hmm while this would be one possible route, it would end up with us breaking the convention of always using subscripts to indicate arity. I think better to make the breaking change rather than end up in an unsatisfactory situation...
