Add/fix RightInverse for dependent products

[cspollard]

This PR contains two changes:

• adds a dependent product right inverse Σ-↪, which is dual to Σ-↩
• renames left-inverse to right-inverse at src/Data/Product/Function/Dependent/Setoid.agda: as far as I can tell, this was a typo.

If there's interest, I could try to add a left-inverse dual to right-inverse in a similar way to what has been done for PropositionalEquality.

@jamesmckinna points out that this may be in conflict with #2583 . Since the PR here is rather small, it probably could be added after that one is merged -- I didn't look at what would be required.

(also: will make changes to ChangeLog if it's agreed this should be merged.)

[JacquesCarette]

Looks great to me - but needs a CHANGELOG entry.

[jamesmckinna]

@cspollard this looks fine to me, modulo:

• as an addition, it's easily badged as v2.3, so mergeable now, moreover I see no conflict with the larger-scale [ refactor ] Symmetry of Bijection as a consequence of properties of a given Surjective function #2583 (at least on a first glance)
• but as a breaking change, because of the fixing of the name, it would have to be v3.0, even though you're correcting an obvious bug

So I think a slightly more conservative, but backwards compatible (and hence mergeable now), version, would be to reinsert left-inverse as a deprecated name (and... defined equal to right-inverse), and then in v3.0 we'll fix things up by removing that deprecation (even that goes beyond our usual practice, but I think we're planning to make so many wholesale changes in v3.0 that it won't matter in the great scheme of things).

Separately, and as a different solution to the problem, but one moreover future-proofed for your other suggestion about a 'real' left-inverse dual to right-inverse, would be to change the names entirely:

• your new right-inverse (old: left-inverse) becomes rightInverse
• left-inverse is deprecated as an alias of rightInverse
• leftInverse becomes a name free to define now as part of this PR, or downstream, without any clash with the deprecated name.

The rationale for this is that for all of our other CamelCase record type/bundle names, we tend to observe the heuristic that concrete (typically: 'module-locally-canonical') instances should be named camelCase : CamelCase... and the usage left-inverse/right-inverse here seems a wart on such a naming scheme, which is otherwise observed everywhere else in Data.Product.Function.Dependent.Setoid!

The only contra argument to the above would be if we could somehow weaken the restriction to PropositionalEquality in the first component, in the spirit of the generalisations in #2583 but even if we could/can, those would similarly be an API change we could fold into a v3.0 breaking PR.

[jamesmckinna]

Regarding the possible conflict:

• sorry for having introduced that noise in the discussion on Zulip without thinking things through
• the imports you make in Data.Product.Function.Dependent.Propositional from Function.Construct.Symmetry in any case do not touch those lemmas affected by [ refactor ] Symmetry of Bijection as a consequence of properties of a given Surjective function #2583 , so I think there is no actual conflict
• the separate question of whether the constructions can all be generalised to non-propositional first components is a much larger one, and out-of-scope for this PR

[cspollard]

Hi @jamesmckinna @JacquesCarette ,

Thanks for the careful review. Here's what I have done:

• used the names rightInverse and leftInverse (which was easy enough to provide), as suggested by @jamesmckinna
• deprecated left-inverse, as suggested by @jamesmckinna
• added a note to CHANGELOG.md, as requested by @JacquesCarette

Please let me know if you see any other worthwhile changes!

I leave other updates for a future PR.

[jamesmckinna]

CHANGELOG entries need fixing, and one or two other nitpicks, but otherwise looks great!

[jamesmckinna]

One last typo, but otherwise looks great! Thanks!

[jamesmckinna]

@JacquesCarette I'll set it to merge when ready, so once the typo is fixed, and you approve, we're good to go?

[jamesmckinna]

Ugh! I was too hasty in setting to merge when ready before the typo got fixed... we'll have to 'fix it up in the edit` ahead of any v2.3 release.

[cspollard]

Hi @jamesmckinna sorry I missed it: what was the last typo?