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

[jamesmckinna]

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]

I definitely think so. Breaking as it might be.

[jamesmckinna]

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?

[MatthewDaggitt]

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...