[ 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]

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 confusing, 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... ;-)

[MatthewDaggitt]

Named modules like this are usually an indication that they deserve their own top-level module? Do we really need a named module?

[jamesmckinna]

Hmmm... the perennial debate between us about sub-modules!

Here, I would push back and say: yes, because when we instantiate that module in Function.Structures.{IsSurjection|IsBijection} and Function.Bundles.{Surjection|Bijection}, we precisely want to import a whole bunch of related definitions and properties; that is, as the comment says, this is a whole theory of the left inverse map from.

That being said, I'm now more tempted to say that it should therefore be lifted out as a top-level module, but for the fact that it also is worth specialising this theory to Setoids in Function.Consequences.Setoid, and I wasn't entirely clear what the linked module structure of those would look like:

• Function.Consequences.Section.Base for what is now Function.Consequences.Section?
• Function.Consequences.Section.Setoid for what is now Function.Consequences.Setoid.Section?

each importing from the appropriate Function.Consequences module? or simply Function.Section.{Base|Setoid} instead?

Advice welcome!

[jamesmckinna]

So... I've had time to sleep on this, and I'm coming round to your way of thinking, or at least, some way towards it:

• initially, I followed the path of
  • start with properties of an arbitrary Surjective f relative to arbitrary 'equalities', in Function.Consequences
  • specialise to those equalities being derived from Setoids, in Function.Consequences.Setoid
  • import those in Function.Structures
  • and in Function.Bundles
  • deploy in Function.Construct.Symmetry
    (Of course, there's a lot of post-hoc rationalisation involved here... but the layering of abstractions did seem at least congruent with other existing development paths in stdlib, so I'm not going to litigate this idealised design process further)

To your question about separate top-level modules, I suppose we could now say: only the last three points of the list above matter, and the only real deployment of module Section is in Function.Structures.{IsSurjection|IsBijection}, EXCEPT for the deprecations of injective, surjective, bijective in Function.Construct.Symmetry. Grrrrr.

So a possible refactoring (modulo those deprecations, which seem to REQUIRE the definition of Function.Consequences.Section, so perhaps could be further inlined in that deprecation block?) ahead of merging might be to lift all of Function.Consequences.Setoid.Section directly into Function.Structures.{IsSurjection|IsBijection}

Is that more what you had in mind?

[jamesmckinna]

Summarising the discussion above:

• if we want the new definitions to be inlined in Function.Structures and Function.Bundles, then Function.Construct.Symmetry really can't have the extensive suite of deprecations without excessive duplication... so maybe that's sufficiently breaking to make this v3.0, unless we argue that we are fixing a 'bug' with non-backwards-compatible changes...
• if we want a fully backwards-compatible v2.3 approach, then the current architecture developed so far is the way to go.

Let me know how you see this going forward! UPDATED: given how much cleaner is the PR if we just go straight to the breaking version, I think on balance I'd rather do that. Even better if we can make it v2.3 under the rubric of a bug fix. I'll open an 'alternative' PR, and we can choose which seems best? #2583