Agda-stdlib: Confusion about _↔_ (Function.Inverse and Function.Bundles)

[JacquesCarette]

There are two definitions of _↔_ in the library, at Function.Inverse and Function.Bundles. They are closely related, but different.

First, one must be careful to not import both Function (which re-exports Function.Bundles) and Function.Inverse in the same module, else all sorts of clashes on Inverse ensures.

As far as I can tell, the one in Function.Bundles is newer, and likely the one to be used in the future.

However, internally the library uses the one from Function.Inverse a lot more. In particular, Function.Related.TypeIsomorphisms.

So: which _↔_ should I be using? [The answer will lead to a bunch of follow-up questions...]

[ajrouvoet]

I ran into the same yesterday.

I believe you are correct that Function/Function.Definitions/Function.Structures/Function.Bundles are the new modules. AFAI can tell, the TypeIsomorphisms have just not yet been ported to the new hierarchy. I suspect that the fact that the std. lib has not yet ported its proofs is the main reason that the old modules have not yet been properly deprecated.

Personally I would recommend using the new hierarchy, even if you need to port some proofs from the std lib. It is much easier to work with IMO.

[MatthewDaggitt]

Yes apologies, this is my fault. I failed to add sufficient documentation and this has tripped several people up recently. As @ajrouvoet says, Function(.Definitions/Structures/Bundles) is the new code and it's use is encouraged.

I've opened #1188 to add this information to the files.

Personally I would recommend using the new hierarchy, even if you need to port some proofs from the std lib. It is much easier to work with IMO.

That's fantastic to hear that you've found it easier to use :tada: If you have ported any proofs using the new hierarchy any PRs would be greatly appreciated. I've got several lurking around in branches that I need to tidy up and submit.

[MatthewDaggitt]

The answer will lead to a bunch of follow-up questions...

I should have added: bring on the follow-up questions!

[ajrouvoet]

That's fantastic to hear that you've found it easier to use

For sure! Having quick access to the f and its inverse is so much more pleasant. And finding what you're looking for is much easier.

If you have ported any proofs using the new hierarchy

I haven't, but of course!

[ajrouvoet]

@MatthewDaggitt Should what used to be in TypeIsomorphisms not just be in the appropriate Properties modules of various type formers?

I would expect the following for example in Data.Sum.Properties:

⊎-isMagma      : IsMagma _↔_ _⊎_
⊎-isSemigroup : IsSemigroup _↔_ _⊎_
⊎-isMonoid      : IsMonoid _↔_ _⊎_ ⊥

etc

[MatthewDaggitt]

Should what used to be in TypeIsomorphisms not just be in the appropriate Properties modules of various type formers?

They should definitely be under the type formers directory. I think as we discussed in #1141 it would be more appropriate for them to go under Data.Sum.Function

[MatthewDaggitt]

Sorry I meant Data.Sum.Algebra

[ajrouvoet]

I have some of these around now, using the new function hierarchy and will make a PR sometime soon.

[MatthewDaggitt]

By the way, what do you think of @alexarice's suggestion in #1156? His definitions seem to make the properties compose much better? We could still export the existing definitions from the structures and bundles for use?

[JacquesCarette]

@ajrouvoet could you post here which ones you do have? I have some too, and I don't want to duplicate the work. [Mine need a lot of work to submit as PR as they're embedded in an old library.]

[ajrouvoet]

Not many, just the ones I needed. Which was (for now) just the CommutativeMonoid structure of uplus and its dependencies.

[ajrouvoet]

By the way, what do you think of @alexarice's suggestion in #1156?

Looks nice; I haven't used the new setup enough to have run in the issues this solves, so I can't really say something useful.

[JacquesCarette]

Ok, I've got up to CommutativeSemiring (well, Symmetric Rig Groupoid, to be fancy) in pi-dual. I've been meaning to port. My time is finally freeing up a bit, so I think I might be able to do it.

[ajrouvoet]

There is always a bigger fish :) I'll wait for your PR then, since I have what I need and am not in a hurry.

[JacquesCarette]

Sorry to take a while on this. The biggest follow-up question was indeed where to put the ported routines. Data.Sum.Algebra and Data.Product.Algebra are good. Where should distributivity go?

Also, I was going to try hard to 'deconstruct' the Inverse witnesses into its component parts, as the routines (and proofs) are often independently useful. Some of these will belong under Data.Sum and Data.Product, but again the distributivity-related ones don't have a natural home.