[ refactor ] fixes #2568; proves full symmetry for Bijection

[jamesmckinna]

A comprehensive overhaul building on the proposed refactoring in #2568 . Finally finished, I think!

UPDATED: now all 'done', and a lot tighter/smoother/cleaner

• refactor Function.Consequences? (check implicit/explicit bindings of lemmas there, esp. in their use later)
• BUT: full symmetry for Bijection now proved, old weaker form sym-≡ etc. now deprecated (this was a bug!)
• AND can prove Congruent ≈₂ ≈₁ section outright under similar equational assumptions!
• HENCE: in Function.Construct.Symmetry
  • indeed, can remove hypothesis of Congruent ≈₁ ≈₂ f from {injective|bijective}
  • hence, symmetry of IsBijective, and of Bijection, without detour via Inverse

TODO:

• CHANGELOG
• refactor Function.Construct.Symmetry Function.Properties.Bijection to prove full symmetry of IsBijective etc.

NB.

• the deprecations considered in [ DRY ] Refactor Function.* to rationalise the existence of a section to a given Surjective f #2568 are optional, it's more a case of agreeing the 'right' names; existing commits make the change so as to highlight where the work has happened
• the other changes above do necessitate deprecations, of the former, weaker (!), proofs
• these are badged as v2.3 deprecations in favour of *WithoutCongruence constructions, but a v3.0 cleanup PR would remove the old proofs entirely and rename to remove that suffix
• not entirely sure I've quite got the deprecation messages correct, given how gnarly the refactoring has been.... it's typically not a straightforward like-for-like deprecation, because the types have changed
• likewise, there may still be one or two outstanding DRY opportunities for further refactoring, but downstream!

[jamesmckinna]

Should this module be lifted out from Consequences to the top-level of Function.*? Or somewhere else?

[jamesmckinna]

Given that the only property used in the Section module is surjective⇒strictlySurjective, it is tempting to inline that, against lifting out the whole module, and deprecating Function.Consequences.* entirely, as those properties are nowhere else used in stdlib? ... downstream PR... ?

[jamesmckinna]

Hmmm... not 'nowhere':

• Data.Product.Function.Dependent.Setoid (using Function.Consequences.Setoid)
• Data.Nat.Binary.Properties ... (typical in using Function.Consequences.Propositional)
• Data.List.Relation.Unary.Enumerates.Setoid.Properties (which can be simplified!) [ refactor ] Data.List.Relation.Unary.Enumerates.Setoid.Properties using tighter lemma from Function.Consequences #2574
• the various uses in Function

[jamesmckinna]

It's tempting to want to deprecate/remove this whole section, else move to Function.Consequences.
In any case, the use of the lemmas in this module has been inlined away, against such a move.

[jamesmckinna]

It is tempting to want to inline these, as, in the Propositional case, they each take on a particularly simple form which is obscured by the three levels of indirection in these definitions...

[JacquesCarette]

inline these where?

[jamesmckinna]

Firstly, in Function.Consequences.Propositional (see latest commit), but one could even imagine inlining these definitions (given how simple they are) at any call-site...?

[jamesmckinna]

Last words on this:

• I think it is better, given that the types of the corresponding lemmas in Function.Consequences.Propositional differ from those in Function.Consequences{.Setoid} (by making f explicit), we can, moreover should, feel free to reimplement them, as is now done;
• the explicit quantification seems necessary in the handful of call-sites where these lemmas are actually used (and with enough of them, that I no longer propose inlining them there)...
• ... BUT is wrong for strictlyInverseʳ⇒inverseʳ where it is f⁻¹ which should be supplied explicitly, and not f! Fixing this should form part of [ DRY ] Streamline Function.* hierarchy #2570

[JacquesCarette]

Spectacular work. Just one question and one nitpick.

[JacquesCarette]

inline these where?

[JacquesCarette]

I understand that the way variables work, this declaration of f and f⁻¹ will actually have the 'right' things in practice, I find the declaration here confusion, i.e. I would prefer an additional line with f⁻¹ : B → A for clarity.

And I thought you'd rename f to to and f⁻¹ to from everywhere?

[jamesmckinna]

Re: variables.
You're absolutely right. Much clearer for ux/ergonomic reasons, and the typechecker needn't care!

Re: inlining.
Two things about this:

• I'd thought these lemmas weren't used quite as much as they are (I was really focused on their use in Function.*), so the case for inlining is less strong now
• that said, the Function.Consequences.Propositional version probably should be inlined/redefined in that module, because in that setting, the way cong and trans are defined for _≡_ means that they take a much simpler form than that inheriting from Setoid...

Re: f and f⁻¹.
I'd thought to have to and from for the new uses (and not simply those in Structures/Bundles), but I'm not really a fan of 'gratuitous' alpha-conversion elsewhere, if only for the sake of keeping the footprint of the PR smaller. But I could be persuaded... ;-)