Infrastructure for homotopies between maps out of a suspension

[morphismz]

This pr builds upon the infrastructure for constrcting and working with homotopies between maps out of a suspension. This includes:

• characterizing the inverse of the equivalence between homotopies of maps and homotopies of suspension structures
• computing the value of a homotopy defined with this equivalence when applied to north-suspension and south-suspension
• characterizing equalities in the type htyp-suspension-structure

It remains to compute the value of such a homotopy when applied to meridian-suspension. Additionally, it remains to construct a simplified version of the equivalence for maps of the form map-inv-up-suspension X Y c, for some c : suspension-structure X Y.

[morphismz]

Would it make sense to have a file just for homotopies of suspension structures? Right now all code related to that subject is living in the suspensions file. But there are a fair amount of auxiliary lemmas and equivalences kinda crowding that file up. And there will likely be a few more that I need to add.

[fredrik-bakke]

Although I don't have the files in memory, that sounds very reasonable to me. We do a similar thing for many other concepts, and if that makes things more navigable in your opinion, then I say go ahead.

[morphismz]

I had hoped to add a bit more code to this pr before marking it ready, But it seems that some refactoring and creating new files is necessary to make that work. Thus I'm going to clean up this pr by removing the unsolved goals and unfinished code, and then mark it as ready. Then I will subsequently sumbit a refactoring pr followed by a pr to finish off building up the infrastructure for homotopies. I hope this last pr will include some "proof of concept" code, showing that the infrastructure works and is easy to use.

[fredrik-bakke]

I haven't taken the time to review the namings of all the definitions in this PR yet, but I'll say the quality of the PR looks excellent over all.

One remark: I noticed there is a recurring theme of misindented code where this would be easy to detect with rainbow parentheses (i.e. colorcoded parentheses). Have you looked into whether such a feature exists for your editor? I can highly recommend it. 👍

[morphismz]

One remark: I noticed there is a recurring theme of misindented code where this would be easy to detect with rainbow parentheses (i.e. colorcoded parentheses). Have you looked into whether such a feature exists for your editor? I can highly recommend it. 👍

Thanks for the pointer, I should be able to get that set up in emacs! Sorry about all those formatting errors... Thank you for taking the time to look through this pr so closely

[morphismz]

Re @fredrik-bakke suggestion to move the computation of inverses of equiv-tot and equiv-Pi-equiv-family next to the the definitions of the respective equivalences: this works fine for equiv-Pi-equiv-family. But this causes cyclic module dependencies for equiv-tot since I have to import foundation-core.injective-maps into foundation-core.functoriality-dependent-pair-types. Specifically, I get the following:

cyclic module dependency:
  foundation-core.functoriality-dependent-pair-types
  foundation-core.injective-maps
  foundation-core.sets
  foundation.fundamental-theorem-of-identity-types
  foundation-core.functoriality-dependent-pair-types

I could leave the computation of the inverse of equiv-tot in foundation.functoriality-dependent-pair-types and just leave a note next to the definition of equiv-tot? Not sure whats best.