Eckmann-Hilton Updates #1133
Open
Eckmann-Hilton Updates #1133
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
VojtechStep
reviewed
Apr 28, 2024
|
Hey Raymond, welcome back! It's good to see you're active again. Looking forward to seeing what's coming next. 🙂 |
Hey Fredrik, thanks! I'm spinning up for the summer, hoping to get a good chunk of math formalized. Hoping to get the Hopf fibration finally all formalized. I figured I'd acquaint myself with the updates to the library by making a few small prs first. Though it seems like I should reacquaint myself with the style guide first 😄 |
|
I've added a bit more work to this pr. The main result is a finished computation of transporting along an eckmann-hilton identification, resolving one of the tasks in issue #702 . There is a bit more clean up I need to do before this pr is ready for review. I'll mark it ready when the time comes. |
|
I think this pr is now ready for review. There is one more lemma I will add later, namely computing transport along the eckmann-hilton 3-loop. But this relies on some infrastructure related to 3-automorphisms that I will be building in a different pr. So that lemma will wait. Please let me know if I should tone down the prose, I feel like there is a lot on the Eckamnn-Hilton page. I added a bit of an explanation of how we compute transport along an Eckmann-Hilton identification. Let me know if there should be more or less of an explanation |
VojtechStep
reviewed
May 28, 2024
There was a problem hiding this comment.
Great work! Those coherences look like a major PITA, so good job. I'd say 95% of my comments are just formatting. I think this amount of prose is very reasonable, it's always better to have more than less, and most of the content on that page is taken by arguments to lemmas which would be implicit in an ideal world. Keep it up!
src/foundation-core/whiskering-identifications-concatenation.lagda.md
Outdated
Show resolved
Hide resolved
Comment on lines
+483
to
+563
| concat-bottom-homotopy-coherence-square-homotopies | ||
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | ||
| ( tr³ | ||
| ( B) | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β))) | ||
| ( left-whisker-concat-htpy | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β))) | ||
| ( tr²-concat α β ∙h refl-htpy) | ||
| ( right-unit-htpy) | ||
| ( horizontal-pasting-coherence-square-homotopies | ||
| ( tr²-concat | ||
| ( left-whisker-concat refl α) | ||
| ( right-whisker-concat β refl)) | ||
| ( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β) | ||
| ( tr³ | ||
| ( B) | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β))) | ||
| ( horizontal-concat-htpy² | ||
| ( tr³ | ||
| ( B) | ||
| ( left-unit-law-left-whisker-Ω² α)) | ||
| ( tr³ | ||
| ( B) | ||
| ( right-unit-law-right-whisker-Ω² β))) | ||
| ( left-whisker-concat-htpy | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β))) | ||
| ( tr²-concat α β) | ||
| ( refl-htpy) | ||
| ( tr³-horizontal-concat | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β)) | ||
| ( inv-concat-right-homotopy-coherence-square-homotopies | ||
| ( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β) | ||
| ( horizontal-concat-htpy² | ||
| ( tr³ B (left-unit-law-left-whisker-Ω² α)) | ||
| ( tr³ B (right-unit-law-right-whisker-Ω² β))) | ||
| ( left-whisker-concat-htpy | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β))) | ||
| ( refl-htpy) | ||
| ( inv-htpy | ||
| ( compute-left-refl-htpy-horizontal-concat-htpy² | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)))) | ||
| ( ( right-unit-htpy) ∙h | ||
| ( z-concat-htpy³ | ||
| ( inv-htpy right-unit-htpy) | ||
| ( ( inv-htpy right-unit-htpy) ∙h | ||
| ( left-whisker-concat-htpy | ||
| ( tr³ | ||
| ( B) | ||
| ( inv | ||
| ( right-unit-law-right-whisker-concat β ∙ right-unit))) | ||
| ( inv-htpy | ||
| ( left-inv-htpy | ||
| ( left-unit-law-left-whisker-comp (tr² B β))))) ∙h | ||
| ( inv-htpy | ||
| ( assoc-htpy | ||
| ( tr³ | ||
| ( B) | ||
| ( inv | ||
| ( ( right-unit-law-right-whisker-concat β) ∙ | ||
| ( right-unit)))) | ||
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β))) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)))))) ∙h | ||
| ( interchange-htpy² | ||
| ( tr³ B (left-unit-law-left-whisker-concat α)) | ||
| ( refl-htpy) | ||
| ( ( tr³ | ||
| ( B) | ||
| ( inv | ||
| ( ( right-unit-law-right-whisker-concat β) ∙ | ||
| ( right-unit)))) ∙h | ||
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β)))) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)))))) |
There was a problem hiding this comment.
Suggested change
| concat-bottom-homotopy-coherence-square-homotopies | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( tr²-concat α β ∙h refl-htpy) | |
| ( right-unit-htpy) | |
| ( horizontal-pasting-coherence-square-homotopies | |
| ( tr²-concat | |
| ( left-whisker-concat refl α) | |
| ( right-whisker-concat β refl)) | |
| ( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( horizontal-concat-htpy² | |
| ( tr³ | |
| ( B) | |
| ( left-unit-law-left-whisker-Ω² α)) | |
| ( tr³ | |
| ( B) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( tr²-concat α β) | |
| ( refl-htpy) | |
| ( tr³-horizontal-concat | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)) | |
| ( inv-concat-right-homotopy-coherence-square-homotopies | |
| ( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β) | |
| ( horizontal-concat-htpy² | |
| ( tr³ B (left-unit-law-left-whisker-Ω² α)) | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( refl-htpy) | |
| ( inv-htpy | |
| ( compute-left-refl-htpy-horizontal-concat-htpy² | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( ( right-unit-htpy) ∙h | |
| ( z-concat-htpy³ | |
| ( inv-htpy right-unit-htpy) | |
| ( ( inv-htpy right-unit-htpy) ∙h | |
| ( left-whisker-concat-htpy | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( right-unit-law-right-whisker-concat β ∙ right-unit))) | |
| ( inv-htpy | |
| ( left-inv-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β))))) ∙h | |
| ( inv-htpy | |
| ( assoc-htpy | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( ( right-unit-law-right-whisker-concat β) ∙ | |
| ( right-unit)))) | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β))) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))))) ∙h | |
| ( interchange-htpy² | |
| ( tr³ B (left-unit-law-left-whisker-concat α)) | |
| ( refl-htpy) | |
| ( ( tr³ | |
| ( B) | |
| ( inv | |
| ( ( right-unit-law-right-whisker-concat β) ∙ | |
| ( right-unit)))) ∙h | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))))) | |
| concat-bottom-homotopy-coherence-square-homotopies | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( tr²-concat α β ∙h refl-htpy) | |
| ( right-unit-htpy) | |
| ( horizontal-pasting-coherence-square-homotopies | |
| ( tr²-concat | |
| ( left-whisker-concat refl α) | |
| ( right-whisker-concat β refl)) | |
| ( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( horizontal-concat-htpy² | |
| ( tr³ | |
| ( B) | |
| ( left-unit-law-left-whisker-Ω² α)) | |
| ( tr³ | |
| ( B) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( tr²-concat α β) | |
| ( refl-htpy) | |
| ( tr³-horizontal-concat | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)) | |
| ( inv-concat-right-homotopy-coherence-square-homotopies | |
| ( tr²-left-whisker-concat-tr²-right-whisker-concat-Ω² α β) | |
| ( horizontal-concat-htpy² | |
| ( tr³ B (left-unit-law-left-whisker-Ω² α)) | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( refl-htpy) | |
| ( inv-htpy | |
| ( compute-left-refl-htpy-horizontal-concat-htpy² | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( ( right-unit-htpy) ∙h | |
| ( z-concat-htpy³ | |
| ( inv-htpy right-unit-htpy) | |
| ( ( inv-htpy right-unit-htpy) ∙h | |
| ( left-whisker-concat-htpy | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( right-unit-law-right-whisker-concat β ∙ right-unit))) | |
| ( inv-htpy | |
| ( left-inv-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β))))) ∙h | |
| ( inv-htpy | |
| ( assoc-htpy | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( ( right-unit-law-right-whisker-concat β) ∙ | |
| ( right-unit)))) | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β))) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))))) ∙h | |
| ( interchange-htpy² | |
| ( tr³ B (left-unit-law-left-whisker-concat α)) | |
| ( refl-htpy) | |
| ( ( tr³ | |
| ( B) | |
| ( inv | |
| ( ( right-unit-law-right-whisker-concat β) ∙ | |
| ( right-unit)))) ∙h | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))))) |
Comment on lines
+580
to
+632
| inv-concat-left-homotopy-coherence-square-homotopies | ||
| ( tr²-concat α β) | ||
| ( tr³ | ||
| ( B) | ||
| ( inv | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β)))) | ||
| ( inv-htpy | ||
| ( left-whisker-concat-htpy | ||
| (tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)))) | ||
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | ||
| ( tr⁴ | ||
| ( B) | ||
| ( distributive-inv-horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β))) | ||
| ( concat-left-homotopy-coherence-square-homotopies | ||
| ( tr²-concat α β) | ||
| ( inv-htpy | ||
| ( tr³ | ||
| ( B) | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β)))) | ||
| ( inv-htpy | ||
| ( left-whisker-concat-htpy | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)))) | ||
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | ||
| ( ( inv-htpy | ||
| ( tr³-inv | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β)))) ∙h | ||
| ( tr⁴ | ||
| ( B) | ||
| ( distributive-inv-horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-concat α) | ||
| ( right-unit-law-right-whisker-Ω² β)))) | ||
| ( vertical-inv-coherence-square-homotopies | ||
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | ||
| ( tr³ | ||
| ( B) | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β))) | ||
| ( left-whisker-concat-htpy | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β))) | ||
| ( tr²-concat α β) | ||
| ( tr³-horizontal-concat-left-unit-law-left-whisker-right-unit-law-right-whisker-Ω²))) |
There was a problem hiding this comment.
Suggested change
| inv-concat-left-homotopy-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| (tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr⁴ | |
| ( B) | |
| ( distributive-inv-horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( concat-left-homotopy-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( inv-htpy | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( ( inv-htpy | |
| ( tr³-inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) ∙h | |
| ( tr⁴ | |
| ( B) | |
| ( distributive-inv-horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-concat α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( vertical-inv-coherence-square-homotopies | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( tr²-concat α β) | |
| ( tr³-horizontal-concat-left-unit-law-left-whisker-right-unit-law-right-whisker-Ω²))) | |
| inv-concat-left-homotopy-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr⁴ | |
| ( B) | |
| ( distributive-inv-horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( concat-left-homotopy-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( inv-htpy | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( ( inv-htpy | |
| ( tr³-inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) ∙h | |
| ( tr⁴ | |
| ( B) | |
| ( distributive-inv-horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-concat α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( vertical-inv-coherence-square-homotopies | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β))) | |
| ( tr²-concat α β) | |
| ( tr³-horizontal-concat-left-unit-law-left-whisker-right-unit-law-right-whisker-Ω²))) |
Comment on lines
+651
to
+723
| concat-bottom-homotopy-coherence-square-homotopies | ||
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | ||
| ( tr³ | ||
| ( B) | ||
| ( horizontal-concat-Id² | ||
| ( right-unit-law-right-whisker-Ω² β) | ||
| ( left-unit-law-left-whisker-Ω² α))) | ||
| ( right-whisker-concat-htpy | ||
| ( left-unit-law-left-whisker-comp (tr² B β)) | ||
| ( tr² B α)) | ||
| ( ( tr²-concat β α) ∙h refl-htpy) | ||
| ( right-unit-htpy) | ||
| ( horizontal-pasting-coherence-square-homotopies | ||
| ( tr²-concat | ||
| ( right-whisker-concat β refl) | ||
| ( left-whisker-concat refl α)) | ||
| ( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² β α) | ||
| ( tr³ | ||
| ( B) | ||
| ( horizontal-concat-Id² | ||
| ( right-unit-law-right-whisker-Ω² β) | ||
| ( left-unit-law-left-whisker-Ω² α))) | ||
| ( horizontal-concat-htpy² | ||
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | ||
| ( tr³ B (left-unit-law-left-whisker-Ω² α))) | ||
| ( right-whisker-concat-htpy | ||
| ( left-unit-law-left-whisker-comp (tr² B β)) | ||
| ( tr² B α)) | ||
| ( tr²-concat β α) | ||
| ( refl-htpy) | ||
| ( tr³-horizontal-concat | ||
| ( right-unit-law-right-whisker-Ω² β) | ||
| ( left-unit-law-left-whisker-Ω² α)) | ||
| ( inv-concat-right-homotopy-coherence-square-homotopies | ||
| ( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² β α) | ||
| ( horizontal-concat-htpy² | ||
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | ||
| ( tr³ B (left-unit-law-left-whisker-Ω² α))) | ||
| ( right-whisker-concat-htpy | ||
| ( left-unit-law-left-whisker-comp (tr² B β)) | ||
| ( tr² B α)) | ||
| ( refl-htpy) | ||
| ( inv-htpy | ||
| ( compute-right-refl-htpy-horizontal-concat-htpy² | ||
| ( left-unit-law-left-whisker-comp (tr² B β)) | ||
| ( tr² B α))) | ||
| ( ( right-unit-htpy | ||
| {H = (horizontal-concat-htpy² | ||
| (tr³ B (right-unit-law-right-whisker-Ω² β)) | ||
| (tr³ B (left-unit-law-left-whisker-Ω² α)))}) ∙h | ||
| ( z-concat-htpy³ | ||
| ( ( inv-htpy right-unit-htpy) ∙h | ||
| ( left-whisker-concat-htpy | ||
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | ||
| ( inv-htpy | ||
| ( left-inv-htpy | ||
| ( left-unit-law-left-whisker-comp (tr² B β))))) ∙h | ||
| ( inv-htpy | ||
| ( assoc-htpy | ||
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | ||
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β))) | ||
| ( left-unit-law-left-whisker-comp (tr² B β))))) | ||
| ( inv-htpy right-unit-htpy)) ∙h | ||
| ( interchange-htpy² | ||
| ( ( tr³ | ||
| ( B) | ||
| ( inv | ||
| ( ( right-unit-law-right-whisker-concat β) ∙ | ||
| ( right-unit)))) ∙h | ||
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β)))) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)) | ||
| ( tr³ B (left-unit-law-left-whisker-concat α)) | ||
| ( refl-htpy))))) |
There was a problem hiding this comment.
Suggested change
| concat-bottom-homotopy-coherence-square-homotopies | |
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α)) | |
| ( ( tr²-concat β α) ∙h refl-htpy) | |
| ( right-unit-htpy) | |
| ( horizontal-pasting-coherence-square-homotopies | |
| ( tr²-concat | |
| ( right-whisker-concat β refl) | |
| ( left-whisker-concat refl α)) | |
| ( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² β α) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α))) | |
| ( horizontal-concat-htpy² | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( tr³ B (left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α)) | |
| ( tr²-concat β α) | |
| ( refl-htpy) | |
| ( tr³-horizontal-concat | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α)) | |
| ( inv-concat-right-homotopy-coherence-square-homotopies | |
| ( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² β α) | |
| ( horizontal-concat-htpy² | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( tr³ B (left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α)) | |
| ( refl-htpy) | |
| ( inv-htpy | |
| ( compute-right-refl-htpy-horizontal-concat-htpy² | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α))) | |
| ( ( right-unit-htpy | |
| {H = (horizontal-concat-htpy² | |
| (tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| (tr³ B (left-unit-law-left-whisker-Ω² α)))}) ∙h | |
| ( z-concat-htpy³ | |
| ( ( inv-htpy right-unit-htpy) ∙h | |
| ( left-whisker-concat-htpy | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( inv-htpy | |
| ( left-inv-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β))))) ∙h | |
| ( inv-htpy | |
| ( assoc-htpy | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β))) | |
| ( left-unit-law-left-whisker-comp (tr² B β))))) | |
| ( inv-htpy right-unit-htpy)) ∙h | |
| ( interchange-htpy² | |
| ( ( tr³ | |
| ( B) | |
| ( inv | |
| ( ( right-unit-law-right-whisker-concat β) ∙ | |
| ( right-unit)))) ∙h | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr³ B (left-unit-law-left-whisker-concat α)) | |
| ( refl-htpy))))) | |
| concat-bottom-homotopy-coherence-square-homotopies | |
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α)) | |
| ( tr²-concat β α ∙h refl-htpy) | |
| ( right-unit-htpy) | |
| ( horizontal-pasting-coherence-square-homotopies | |
| ( tr²-concat | |
| ( right-whisker-concat β refl) | |
| ( left-whisker-concat refl α)) | |
| ( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² β α) | |
| ( tr³ | |
| ( B) | |
| ( horizontal-concat-Id² | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α))) | |
| ( horizontal-concat-htpy² | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( tr³ B (left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α)) | |
| ( tr²-concat β α) | |
| ( refl-htpy) | |
| ( tr³-horizontal-concat | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α)) | |
| ( inv-concat-right-homotopy-coherence-square-homotopies | |
| ( tr²-right-whisker-concat-tr²-left-whisker-concat-Ω² β α) | |
| ( horizontal-concat-htpy² | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( tr³ B (left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α)) | |
| ( refl-htpy) | |
| ( inv-htpy | |
| ( compute-right-refl-htpy-horizontal-concat-htpy² | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr² B α))) | |
| ( ( right-unit-htpy | |
| { H = | |
| ( horizontal-concat-htpy² | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( tr³ B (left-unit-law-left-whisker-Ω² α)))}) ∙h | |
| ( z-concat-htpy³ | |
| ( ( inv-htpy right-unit-htpy) ∙h | |
| ( left-whisker-concat-htpy | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( inv-htpy | |
| ( left-inv-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β))))) ∙h | |
| ( inv-htpy | |
| ( assoc-htpy | |
| ( tr³ B (right-unit-law-right-whisker-Ω² β)) | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β))) | |
| ( left-unit-law-left-whisker-comp (tr² B β))))) | |
| ( inv-htpy right-unit-htpy)) ∙h | |
| ( interchange-htpy² | |
| ( ( tr³ | |
| ( B) | |
| ( inv | |
| ( ( right-unit-law-right-whisker-concat β) ∙ | |
| ( right-unit)))) ∙h | |
| ( inv-htpy (left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( left-unit-law-left-whisker-comp (tr² B β)) | |
| ( tr³ B (left-unit-law-left-whisker-concat α)) | |
| ( refl-htpy))))) |
Comment on lines
+736
to
+787
| inv-concat-left-homotopy-coherence-square-homotopies | ||
| ( tr²-concat α β) | ||
| ( tr³ B (eckmann-hilton-Ω² α β)) | ||
| ( eckmann-hilton-htpy (tr² B α) (tr² B β)) | ||
| ( tr²-concat β α) | ||
| ( tr³-concat-eckmann-hilton) | ||
| ( vertical-pasting-coherence-square-homotopies | ||
| ( tr²-concat α β) | ||
| ( tr³ B | ||
| ( inv | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β))) ∙h | ||
| ( tr³ B (commutative-left-whisker-right-whisker-concat α β))) | ||
| ( ( inv-htpy | ||
| ( left-whisker-concat-htpy | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)))) ∙h | ||
| ( commutative-right-whisker-left-whisker-htpy | ||
| ( tr² B α) | ||
| ( tr² B β))) | ||
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | ||
| ( tr³ B | ||
| ( horizontal-concat-Id² | ||
| ( right-unit-law-right-whisker-Ω² β) | ||
| ( left-unit-law-left-whisker-Ω² α))) | ||
| ( right-whisker-concat-htpy | ||
| ( left-unit-law-left-whisker-comp (tr² B β)) (tr² B α)) | ||
| ( tr²-concat β α) | ||
| ( vertical-pasting-coherence-square-homotopies | ||
| ( tr²-concat α β) | ||
| ( tr³ | ||
| ( B) | ||
| ( inv | ||
| ( horizontal-concat-Id² | ||
| ( left-unit-law-left-whisker-Ω² α) | ||
| ( right-unit-law-right-whisker-Ω² β)))) | ||
| ( inv-htpy | ||
| ( left-whisker-concat-htpy | ||
| ( tr² B α) | ||
| ( left-unit-law-left-whisker-comp (tr² B β)))) | ||
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | ||
| ( tr³ | ||
| ( B) | ||
| ( commutative-left-whisker-right-whisker-concat α β)) | ||
| ( commutative-right-whisker-left-whisker-htpy | ||
| ( tr² B α) | ||
| ( tr² B β)) | ||
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | ||
| ( tr³-horizontal-concat-inv-left-unit-law-left-whisker-right-unit-law-right-whisker-Ω²) | ||
| ( tr³-commutative-left-whisker-right-whisker-concat-Ω² α β)) | ||
| ( tr³-horizontal-concat-right-unit-law-right-whisker-left-unit-law-left-whisker-Ω²)) |
There was a problem hiding this comment.
Suggested change
| inv-concat-left-homotopy-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ B (eckmann-hilton-Ω² α β)) | |
| ( eckmann-hilton-htpy (tr² B α) (tr² B β)) | |
| ( tr²-concat β α) | |
| ( tr³-concat-eckmann-hilton) | |
| ( vertical-pasting-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ B | |
| ( inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) ∙h | |
| ( tr³ B (commutative-left-whisker-right-whisker-concat α β))) | |
| ( ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) ∙h | |
| ( commutative-right-whisker-left-whisker-htpy | |
| ( tr² B α) | |
| ( tr² B β))) | |
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | |
| ( tr³ B | |
| ( horizontal-concat-Id² | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) (tr² B α)) | |
| ( tr²-concat β α) | |
| ( vertical-pasting-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr³ | |
| ( B) | |
| ( commutative-left-whisker-right-whisker-concat α β)) | |
| ( commutative-right-whisker-left-whisker-htpy | |
| ( tr² B α) | |
| ( tr² B β)) | |
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | |
| ( tr³-horizontal-concat-inv-left-unit-law-left-whisker-right-unit-law-right-whisker-Ω²) | |
| ( tr³-commutative-left-whisker-right-whisker-concat-Ω² α β)) | |
| ( tr³-horizontal-concat-right-unit-law-right-whisker-left-unit-law-left-whisker-Ω²)) | |
| inv-concat-left-homotopy-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ B (eckmann-hilton-Ω² α β)) | |
| ( eckmann-hilton-htpy (tr² B α) (tr² B β)) | |
| ( tr²-concat β α) | |
| ( tr³-concat-eckmann-hilton) | |
| ( vertical-pasting-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ B | |
| ( inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β))) ∙h | |
| ( tr³ B (commutative-left-whisker-right-whisker-concat α β))) | |
| ( ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) ∙h | |
| ( commutative-right-whisker-left-whisker-htpy (tr² B α) (tr² B β))) | |
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | |
| ( tr³ B | |
| ( horizontal-concat-Id² | |
| ( right-unit-law-right-whisker-Ω² β) | |
| ( left-unit-law-left-whisker-Ω² α))) | |
| ( right-whisker-concat-htpy | |
| ( left-unit-law-left-whisker-comp (tr² B β)) (tr² B α)) | |
| ( tr²-concat β α) | |
| ( vertical-pasting-coherence-square-homotopies | |
| ( tr²-concat α β) | |
| ( tr³ | |
| ( B) | |
| ( inv | |
| ( horizontal-concat-Id² | |
| ( left-unit-law-left-whisker-Ω² α) | |
| ( right-unit-law-right-whisker-Ω² β)))) | |
| ( inv-htpy | |
| ( left-whisker-concat-htpy | |
| ( tr² B α) | |
| ( left-unit-law-left-whisker-comp (tr² B β)))) | |
| ( tr²-concat-left-whisker-concat-right-whisker-concat-Ω² α β) | |
| ( tr³ B (commutative-left-whisker-right-whisker-concat α β)) | |
| ( commutative-right-whisker-left-whisker-htpy (tr² B α) (tr² B β)) | |
| ( tr²-concat-right-whisker-concat-left-whisker-concat-Ω² β α) | |
| ( tr³-horizontal-concat-inv-left-unit-law-left-whisker-right-unit-law-right-whisker-Ω²) | |
| ( tr³-commutative-left-whisker-right-whisker-concat-Ω² α β)) | |
| ( tr³-horizontal-concat-right-unit-law-right-whisker-left-unit-law-left-whisker-Ω²)) |
Yes, yes they were... Thanks for the diligent review process and all the feed back! |
Co-authored-by: Vojtěch Štěpančík <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes links and makes consistent naming changes related to the Eckmann-Hilton file. Also adds an updated reference to the page.