Refactor files about identity types and homotopies

[EgbertRijke]

The following files were significantly cleaned up:

• foundation.path-algebra

The following files were created:

• foundation.action-on-higher-identifications-functions
• foundation.whiskering-higher-homotopies
• foundation.whiskering-identifications

The following other actions were performed:

• Adding detailed informal explanations to many entries affected by this pull request.
• Replace whisk with whisker throughout the library.
• Making the order of arguments uniform for various operations on commuting squares and triangles of identifications.
• Fixing names so that operator names go before the entity that they act on:
  • htpy-left-whisker to htpy-left-whisker
  • coherence-square-identifications-horizontal-inv to horizontal-inv-coherence-square-identifications
  • coherence-square-identifications-left-paste to left-concat-identification-coherence-square-identification, and variants
• Replace ap (ap f) with ap² f throughout the library. I also renamed the various nat-sq-entries about ap².
• Moving the entries about squares of identifications from path-algebra to commuting-squares-of-identifications.
• There were duplicate entries that did the same pasting lemmas of commuting squares of identifications, spread out over several files including commuting-squares-of-identifications and path-algebra. These separate formalization attempts have been unified.
• Removing "iterated inverse laws" from path-algebra since they were duplicate entries and they were not actually iterated.
• Rename ap-concat-eq to map-coherence-triangle-identifications, change the order of its arguments to match with coherence-triangle-identifications, and move it to commuting-triangles-of-identifications.
• Rename coherence-square-identifications-ap to map-coherence-square-identifications.
• Remove entries inv-htpy-left-whisk-inv-htpy and inv-htpy-right-whisk-inv-htpy.
• Rename ap-left-whisk-htpy to left-whisker-htpy², and ap-right-whisk-htpy to right-whisker-htpy² and move them to whiskering-higher-homotopies.
• Correcting a statement that refl-htpy is a unit element on the homotopy side for whiskering. Instead, it is an absorbing element.

[EgbertRijke]

I thought this would be a quicky but I'm encountering a lot of substandard programming while editing the entries about whiskering, so I better put my shoulders under this and do the refactoring well. I'll mark this PR as a draft for now.

[fredrik-bakke]

DONE! 🥵

[EgbertRijke]

I have addressed all the comments now. I defer all the future comments to future pull requests

[EgbertRijke]

Also I am happy to share this PR with @fredrik-bakke, for his heroic efforts of reviewing this monster. Thank you!

[fredrik-bakke]

Hooray! 🎉