Refactor Eckmann-Hilton

[morphismz]

This pr formalizes eckmann-hilton as the naturality condition of htpy-identification-left-whisk.

I added a file just for eckmann-hilton since it was over crowding the double loop space file. We will later need lemmas showing that, e.g., eckmann-hilton is preserved by tr and arbitrary functions, which now have a natural home in the new file. I wrote out an explanation preceding this new construction of eckmann-hilton. However, the explanation is long. If it is too long, let me know and maybe suggest a part that is unnecessary.

I added a higher-transport-along-identifications file because of cyclic module dependency issues. This will probably need to be organized a bit better.

This pr resolves a task from issue #702

[EgbertRijke]

Very good! Instead of speaking of "higher transport", how about speaking of "transport along higher identifications"? This may seem like a minor detail, but then we can call the file transport-along-higher-identifications and it will appear right there among the other transport-along files.

[EgbertRijke]

Would you also be so kind to add the new transport-along-higher-identifications file to the overview tables in foundation-core/identity-types and foundation/identity-types?

See here how it should look like: https://unimath.github.io/agda-unimath/foundation.identity-types.html#list-of-files-directly-related-to-identity-types

[morphismz]

Very good! Instead of speaking of "higher transport", how about speaking of "transport along higher identifications"? This may seem like a minor detail, but then we can call the file transport-along-higher-identifications and it will appear right there among the other transport-along files.

That's a much better, name! Will do later today

[morphismz]

Would you also be so kind to add the new transport-along-higher-identifications file to the overview tables in foundation-core/identity-types and foundation/identity-types?

See here how it should look like: https://unimath.github.io/agda-unimath/foundation.identity-types.html#list-of-files-directly-related-to-identity-types

Should I also add the eckmann hilton file to this table? Not sure if it counts, since its specific to loops

[EgbertRijke]

There aren't any files specific about loop spaces in this table. Perhaps a smaller table in synthetic-homotopy-theory.loop-spaces that points to all the files about loops would be better.

[morphismz]

There aren't any files specific about loop spaces in this table. Perhaps a smaller table in synthetic-homotopy-theory.loop-spaces that points to all the files about loops would be better.

I can go ahead an make that, though the only thing I can think of adding is the eckmann-hilton file. And that has more to do with double loop spaces than it does with spaces.

[EgbertRijke]

If we would make a table for anything to do with loop spaces of general pointed types, then it would make sense to include the double loop spaces and iterated loop spaces.

A quick search for the keyword "loop" on the indexing file for synthetic homotopy theory page

https://unimath.github.io/agda-unimath/synthetic-homotopy-theory.html

highlights all the files you could list in that table (9 in total, but 10 with your new EH file).

[fredrik-bakke]

I think it is really nice that you add context and discussion about the Eckmann-Hilton argument!

[EgbertRijke]

I had a quick look and your PR looks absolutely beautiful Raymond! Really good!

[morphismz]

I had a quick look and your PR looks absolutely beautiful Raymond! Really good!

This might be the least number of formatting errors I've made in a pr 😎 We'll see if I can keep it up and turn it into a streak lmao