Transport along and action on equivalences

[fredrik-bakke]

Summary

• Define transport along equivalences tr-equiv in foundation.transport-along-equvalences using transport along identifications
• Define action on equivalences ap-equiv in foundation.action-on-equivalences-functions using action on identifications
• Show that these notions coincide
• Prove a collection of basic properties for each
• Do some refactoring surrounding this

[fredrik-bakke]

Should the module* transport be renamed to transport-along-identifications?

[morphismz]

Should transport be renamed to transport-along-identifications?

this could be helpful. Then you could rename your tr-equiv to transport-along-equiv. This will help disambiguate the latter from equiv-tr.

[morphismz]

Since this is a draft, does this mean you have plans to add a few more definitions and lemmas? I can think of a few that would be nice to have but I can't find in this pr

[fredrik-bakke]

Yes, I'm planning to add a couple more.

[fredrik-bakke]

Should transport be renamed to transport-along-identifications?

this could be helpful. Then you could rename your tr-equiv to transport-along-equiv. This will help disambiguate the latter from equiv-tr.

I like the name tr-equiv. Hopefully the similar naming won't cause too much confusion.

[morphismz]

Should transport be renamed to transport-along-identifications?

this could be helpful. Then you could rename your tr-equiv to transport-along-equiv. This will help disambiguate the latter from equiv-tr.

I like the name tr-equiv. Hopefully the similar naming won't cause too much confusion.

fair enough. Then, may I ask, why rename transport to transport-along-identifications?

[fredrik-bakke]

Should transport be renamed to transport-along-identifications?

this could be helpful. Then you could rename your tr-equiv to transport-along-equiv. This will help disambiguate the latter from equiv-tr.

I like the name tr-equiv. Hopefully the similar naming won't cause too much confusion.

fair enough. Then, may I ask, why rename transport to transport-along-identifications?

Ah, I think I see your confusion! I was talking about the module names, so that we have transport-along-identifications in line with transport-along-equivalences and similar for actions.

[morphismz]

Should transport be renamed to transport-along-identifications?

this could be helpful. Then you could rename your tr-equiv to transport-along-equiv. This will help disambiguate the latter from equiv-tr.

I like the name tr-equiv. Hopefully the similar naming won't cause too much confusion.

fair enough. Then, may I ask, why rename transport to transport-along-identifications?

Ah, I think I see your confusion! I was talking about the module names, so that we have transport-along-identifications in line with transport-along-equivalences and similar for actions.

Gotcha, that makes much more sense! I'm on board

[EgbertRijke]

I think it's a good idea to rename the transport module to transport-along-identifications

[fredrik-bakke]

So... I just realized that foundation.univalence-action-on-equivalences exists...

[fredrik-bakke]

I'll try and merge the two modules. Which name do you prefer?

[EgbertRijke]

transport-along-equivalences sounds better to me than univalence-action-on-equivalences

[EgbertRijke]

Alright, I am done reviewing. I would like to propose an alternative naming scheme for the ap-equiv naming scheme. I am ok with the tr-equiv naming scheme, but what I don't like about ap-equiv is that in the agda-unimath naming scheme it reads too much like the action on paths of an equivalence, which it isn't. So I would really like to convince you that action-equiv is better. Here is what I propose:

eq-ap-equiv -> action-equiv-function
ap-equiv -> action-equiv-family
map-ap-equiv -> map-action-equiv-family
ap-equiv-subuniverse -> action-equiv-family-on-subuniverse

and so on. I think the preposition on is necessary in this case, to disambiguate from families of types in a subuniverse.

Another possibility for the last one, is action-equiv-subuniverse-family, because we are already using the naming scheme equiv-subuniverse for equivalences in a subuniverse.

[EgbertRijke]

Perhaps I would also like to propose to rename ap to action-eq, but that will be for another day:)

[fredrik-bakke]

As a counter-proposal, we could switch the phrasing "action on identifications" to "application to identifications"

[fredrik-bakke]

I do like the new names you've suggested for the action on equivalences though. Thank you for that

[EgbertRijke]

The transport -> transport-along-identifications renaming looks good too. It was indeed easy to scroll through the separate commit. Thank you for separating this out.

[EgbertRijke]

Can I merge it?

[fredrik-bakke]

I think so :)

[EgbertRijke]

Thanks for all the changes!