Is _Respects₂_ sufficient? about agda-stdlib HOT 2 CLOSED

Very old issue but still outstanding I think. I would second this, as the new form proposed above is far more convenient to use.

The current form is particularly irritating if the relation _~_ is not transitive as you can no longer perform dual substitution.

The proposed Respects₂' would require reflexivity of _≈_ in order to recover the current Respects₂ so the current form probably shouldn't be replaced. However would anyone object to the new form being added?

from agda-stdlib.

@mechvel I agree with you, your form is definitely easier to work with and if the library was redesigned from the bottom up we'd use yours. However in the two years since my last comment, I'm afraid I've had a change of heart. The current form is usable, and in my opinion adding a ticked version will result in more confusion than time saved, and we'll end up with conversion lemmas everywhere.

I've added <-respˡ-≈ and <-respʳ-≈ proofs to the record hierarchies in bfd3636. This should make the existing form much easier to use as you no longer have to mess around with projecting them out.

Given that, I'm afraid I'm closing this issue. I hope the new proofs help.

from agda-stdlib.