Jacques Carette
Jacques Carette
So we need an approve from @MatthewDaggitt .
Sounds good to me -- @jmougeot , want to give this a try?
> Any particular reason to introduce this material as a separate sub-hierarchy under `Relation.Binary.Domain`? Increased findability, because of the occurrence of `Domain`, I would think. This is a port from...
Could you please resolve the CHANGELOG conflicts?
Also: you don't seem to have addressed the latest 2 items that I asked about?
Depending on what others think (and my review being taken into account), I do think this could make it to 2.3.
Since the attributions are correct in that further PR, it's probably best to close this one.
[ refactor ] Symmetry of `Bijection` as a consequence of properties of a given `Surjective` function
> which of this and https://github.com/agda/agda-stdlib/pull/2569 do you prefer? There's a lot in common between them, so I'm having a hard time spotting exactly where the differences are?
Is it fundamental that the bulk of this is blocked on something breaking?
Anything I could do to help?