[ DRY ] Streamline Function.* hierarchy

[jamesmckinna]

Now that #2568 / #2569 establish that (for Setoids) Bijection and Inverse are equivalent concepts, we should perhaps do a wholesale refactoring of the Function hierarchy to (choose and) deprecate whichever definitions (and their Propositional friends) we now deem to be redundant? See also #2565 .

Revised: I had previously badged this as v2.3, but I suspect the effects will be so large-scale that it had probably better be tackled as a v3.0 series of tasks... not least the cleanup of the *WithoutCongruent definitions introduced by #2569 to restore the 'old' names, but now with stronger/sharper types than before.

[JacquesCarette]

Can you give us a preview of what you think this would entail?

[jamesmckinna]

Well, the obvious 'minimal' fix/streamlining I envisaged after #2568 would be to:

• [ DRY ] pick one of Bijection or Inverse (and their Propositional counterparts), and deprecate the other in its favour, with Biased implementations replacing them?
• all the knock-ons which might flow from such... including to remove the current WithoutCongruence qualifier, introduced for the sake of standardising the names apart for a non-breaking v2.3 deprecation...

But, the more I worked on that PR, the more threads seemed to get pulled... so it's a bit hard to see exactly how things might cash out? Eg.

• how much of Function.Consequences do we need, or how best to organise it wrt any proposed refactoring?

Maybe it isn't too dramatic as it first seemed to me, cf. Zero in *Ring etc. but ... I also have at the back of my mind the tension between Structures/IsEquivalence and Bundles/Setoid that I've already started to worry away at in Algebra.*... cf. #2502 etc.

[jamesmckinna]

Can you give us a preview of what you think this would entail?

@JacquesCarette The other way to answer your question might be: I have no idea, my brain hurts, so I'd like someone else to think about the possible knock-on consequences of #2569 ... ;-) (with shoutouts to @alexarice for the #1156 redefinition of Surjective and to @MatthewDaggitt for all his heroic work in landing #759 , without which, ...)

[jamesmckinna]

See also: my recent annotations to #2569 identifying possible inlining/deprecation opportunities.