agda
[ refactor ] Symmetry of `Bijection` as a consequence of properties of a given `Surjective` function
Alternative version of #2569 which dispenses with much of the deprecation cruft, in favour of badging this as a bug fix.
No separate module Section added, in favour of folding everything into the definitions of Function.Structures.IsBijection and Function.Bundles.Bijection.
NB. there may now be some further redundancy that could be pruned out: manifest fields, or Properties?
@JacquesCarette which of this and #2569 do you prefer? We should (probably) only merge one of them...
I'll only return to the merge conflicts once we choose between this v3.0 version, and the clunkier v2.3 #2569
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?
which of this and #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?
The main difference is that
- the v2.3 version carries around a lot of extra cruft, in order to be backwards-compatible
- the v3.0 is much more streamlined, as I was able to jettison all that cruft
This was the one that made me seriously think we should simply leapfrog to a full, breaking, v3.0... and I am still considering withdrawing the v2.3 one as too compromised to be worth the effort? Hence the request for comment.
I've downgraded/closed the earlier #2569 in favour of this one. Will fix the merge conflicts, and tidy up the comments to sort out the discussion of congruence. DONE.