Skip to content

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

New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

#

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Jump to bottom
Open
jamesmckinna opened this issue Sep 2, 2024 · 3 comments · May be fixed by #2515
Open

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

jamesmckinna opened this issue Sep 2, 2024 · 3 comments · May be fixed by #2515
Labels
breaking bug
Milestone
v3.0

Comments

@jamesmckinna
Copy link
Contributor

jamesmckinna commented Sep 2, 2024 •
edited
Loading

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?
@jamesmckinna jamesmckinna mentioned this issue Sep 2, 2024
Merged
@JacquesCarette
Copy link
Contributor

I definitely think so. Breaking as it might be.

@jamesmckinna
Copy link
Contributor Author

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
Copy link
Contributor

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

jamesmckinna added a commit to jamesmckinna/agda-stdlib that referenced this issue Dec 9, 2024
@jamesmckinna
Fixes agda#2471
67adc1d
@jamesmckinna jamesmckinna linked a pull request Dec 9, 2024 that will close this issue
Open
@jamesmckinna jamesmckinna added this to the v3.0 milestone Dec 11, 2024
# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees
No one assigned
Labels
breaking bug
Projects
None yet
Milestone
v3.0
3 participants
@JacquesCarette @MatthewDaggitt @jamesmckinna