Eckmann-Hilton in the Universe (#703)

morphismz · fredrik-bakke · web-flow · commit db1621789ed3 · 2023-08-28T13:37:58.000+02:00
This pr formalizes most of the "Eckmann-Hilton in the universe" idea, thus bringing partial completion to one of the task on the issue "Formalize the Hopf Fibration" ( #702 ). The main theorem of the pr, named `tr³-htpy-swap-path-swap`, establishes that `tr³` sends `path-swap` to `htpy-swap`. --------- Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
diff --git a/src/foundation/homotopies.lagda.md b/src/foundation/homotopies.lagda.md
@@ -15,6 +15,7 @@ open import foundation.dependent-pair-types
 open import foundation.function-extensionality
 open import foundation.identity-systems
 open import foundation.identity-types
+open import foundation.path-algebra
 open import foundation.universe-levels
 
 open import foundation-core.contractible-types
@@ -297,6 +298,27 @@ module _
         ( inv right-unit))
 ```
 
+### Eckmann-Hilton for homotopies
+
+```agda
+htpy-swap-nat-right-htpy :
+  {l0 l1 l2 : Level} {X : UU l0} {Y : UU l1} {Z : UU l2}
+  {f g : X → Y} {f' g' : Y → Z} (H' : f' ~ g')
+  (H : f ~ g) →
+  (htpy-right-whisk H' f ∙h htpy-left-whisk g' H) ~
+  (htpy-left-whisk f' H ∙h htpy-right-whisk H' g)
+htpy-swap-nat-right-htpy H' H x =
+    nat-htpy H' (H x)
+
+eckmann-hilton-htpy :
+  {l : Level} {X : UU l} (H K : id {A = X} ~ id) →
+  (H ∙h K) ~ (K ∙h H)
+eckmann-hilton-htpy H K x =
+  ( inv (identification-left-whisk (H x) (ap-id (K x))) ∙
+  ( htpy-swap-nat-right-htpy H K x)) ∙
+  ( identification-right-whisk (ap-id (K x)) (H x))
+```
+
 ## See also
 
 - We postulate that homotopies characterize identifications in (dependent)
diff --git a/src/foundation/path-algebra.lagda.md b/src/foundation/path-algebra.lagda.md
@@ -158,6 +158,26 @@ horizontal-concat-Id² :
 horizontal-concat-Id² α β = ap-binary (λ s t → s ∙ t) α β
 ```
 
+#### Identification whiskering
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z : A}
+  where
+
+  identification-left-whisk :
+    (p : x ＝ y) {q q' : y ＝ z} → q ＝ q' → (p ∙ q) ＝ (p ∙ q')
+  identification-left-whisk p β = ap (p ∙_) β
+
+  identification-right-whisk :
+    {p p' : x ＝ y} → p ＝ p' → (q : y ＝ z) → (p ∙ q) ＝ (p' ∙ q)
+  identification-right-whisk α q = ap (_∙ q) α
+
+  htpy-identification-left-whisk :
+    {q q' : y ＝ z} → q ＝ q' → (_∙ q) ~ (_∙ q')
+  htpy-identification-left-whisk β p = identification-left-whisk p β
+```
+
 ### Both horizontal and vertical concatenation of 2-paths are binary equivalences
 
 ```agda
@@ -197,12 +217,30 @@ right-unit-law-horizontal-concat-Id² :
 right-unit-law-horizontal-concat-Id² α = right-unit-ap-binary (λ s t → s ∙ t) α
 ```
 
+#### The whiskering operations allow us to commute higher identifications
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y z : A}
+  where
+
+  path-swap-nat-identification-left-whisk :
+    {q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') →
+    coherence-square-identifications
+      ( identification-left-whisk p β)
+      ( identification-right-whisk α q')
+      ( identification-right-whisk α q)
+      ( identification-left-whisk p' β)
+  path-swap-nat-identification-left-whisk β =
+    nat-htpy (htpy-identification-left-whisk β)
+```
+
 Horizontal concatination satisfies an additional "2-dimensional" unit law (on
 both the left and right) induced by the unit laws on the boundary 1-paths.
 
 ```agda
 module _
-  {l : Level} {A : UU l} {a0 a1 : A} {p p' : a0 ＝ a1} (α : p ＝ p')
+  {l : Level} {A : UU l} {x y : A} {p p' : x ＝ y} (α : p ＝ p')
   where
 
   nat-sq-right-unit-Id² :
@@ -227,7 +265,7 @@ module _
 
 ```agda
 module _
-  {l : Level} {A : UU l} {a0 a1 : A} {p p' : a0 ＝ a1}
+  {l : Level} {A : UU l} {x y : A} {p p' : x ＝ y}
   where
 
   horizontal-inv-Id² : p ＝ p' → (inv p) ＝ (inv p')
@@ -239,7 +277,7 @@ This operation satisfies a left and right idenity induced by the inverse laws on
 
 ```agda
 module _
-  {l : Level} {A : UU l} {a0 a1 : A} {p p' : a0 ＝ a1} (α : p ＝ p')
+  {l : Level} {A : UU l} {x y : A} {p p' : x ＝ y} (α : p ＝ p')
   where
 
   nat-sq-right-inv-Id² :
@@ -322,8 +360,8 @@ Functions have an induced action on 2-paths
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} {a0 a1 : A}
-  {p p' : a0 ＝ a1} (f : A → B) (α : p ＝ p')
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
+  {p p' : x ＝ y} (f : A → B) (α : p ＝ p')
   where
 
   ap² : (ap f p) ＝ (ap f p')
@@ -337,8 +375,8 @@ Inverse law.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} {a0 a1 : A}
-  {p p' : a0 ＝ a1} (f : A → B) (α : p ＝ p')
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
+  {p p' : x ＝ y} (f : A → B) (α : p ＝ p')
   where
 
   nat-sq-ap-inv-Id² :
@@ -357,8 +395,8 @@ Identity law and constant law.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {B : UU l2} {a0 a1 : A}
-  {p p' : a0 ＝ a1} (α : p ＝ p')
+  {l1 l2 : Level} {A : UU l1} {B : UU l2} {x y : A}
+  {p p' : x ＝ y} (α : p ＝ p')
   where
 
   nat-sq-ap-id-Id² :
@@ -383,7 +421,7 @@ Composition law
 ```agda
 module _
   {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {C : UU l3}
-  {a0 a1 : A} {p p' : a0 ＝ a1} (g : B → C) (f : A → B) (α : p ＝ p')
+  {x y : A} {p p' : x ＝ y} (g : B → C) (f : A → B) (α : p ＝ p')
   where
 
   nat-sq-ap-comp-Id² :
diff --git a/src/foundation/transport.lagda.md b/src/foundation/transport.lagda.md
@@ -10,12 +10,14 @@ open import foundation-core.transport public
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.commuting-squares-of-identifications
 open import foundation.dependent-pair-types
+open import foundation.homotopies
+open import foundation.path-algebra
 open import foundation.universe-levels
 
 open import foundation-core.equivalences
 open import foundation-core.function-types
-open import foundation-core.homotopies
 open import foundation-core.identity-types
 ```
 
@@ -37,12 +39,19 @@ recorded in this file.
 
 ```agda
 module _
-  {l1 l2 : Level} {A : UU l1} {a0 a1 : A} {p0 p1 : a0 ＝ a1}
-  (B : A → UU l2)
+  {l1 l2 : Level} {A : UU l1} {x y : A} {p p' : x ＝ y}
   where
 
-  tr² : (α : p0 ＝ p1) (b0 : B a0) → (tr B p0 b0) ＝ (tr B p1 b0)
-  tr² α b0 = ap (λ t → tr B t b0) α
+  tr² : (B : A → UU l2) (α : p ＝ p') (b : B x) → (tr B p b) ＝ (tr B p' b)
+  tr² B α b = ap (λ t → tr B t b) α
+
+module _
+  {l1 l2 : Level} {A : UU l1} {x y : A} {p p' : x ＝ y}
+  {α α' : p ＝ p'}
+  where
+
+  tr³ : (B : A → UU l2) (β : α ＝ α') (b : B x) → (tr² B α b) ＝ (tr² B α' b)
+  tr³ B β b = ap (λ t → tr² B t b) β
 ```
 
 ## Properties
@@ -93,3 +102,92 @@ tr-subst :
   tr B (ap f p) x' ＝ tr (B ∘ f) p x'
 tr-subst B f refl = refl
 ```
+
+### Coherences and algebraic identities for `tr²`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {x y : A}
+  {B : A → UU l2}
+  where
+
+  tr²-concat :
+    {p p' p'' : x ＝ y} (α : p ＝ p') (α' : p' ＝ p'') (b : B x) →
+    (tr² B (α ∙ α') b) ＝ (tr² B α b ∙ tr² B α' b)
+  tr²-concat α α' b = ap-concat (λ t → tr B t b) α α'
+
+module _
+  {l1 l2 : Level} {A : UU l1} {x y z : A}
+  {B : A → UU l2}
+  where
+
+  tr²-left-whisk :
+    (p : x ＝ y) {q q' : y ＝ z} (β : q ＝ q') (b : B x) →
+    coherence-square-identifications
+      ( tr² B (identification-left-whisk p β) b)
+      ( tr-concat p q' b)
+      ( tr-concat p q b)
+      ( htpy-right-whisk (tr² B β) (tr B p) b)
+  tr²-left-whisk refl refl b = refl
+
+  tr²-right-whisk :
+    {p p' : x ＝ y} (α : p ＝ p') (q : y ＝ z) (b : B x) →
+    coherence-square-identifications
+      ( tr² B (identification-right-whisk α q) b)
+      ( tr-concat p' q b)
+      ( tr-concat p q b)
+      ( htpy-left-whisk (tr B q) (tr² B α) b)
+  tr²-right-whisk refl refl b = inv right-unit
+```
+
+#### Coherences and algebraic identities for `tr³`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {x y z : A}
+  {B : A → UU l2}
+  where
+
+  tr³-htpy-swap-path-swap :
+    {q q' : y ＝ z} (β : q ＝ q') {p p' : x ＝ y} (α : p ＝ p') (b : B x) →
+    coherence-square-identifications
+      ( identification-right-whisk
+        ( tr³
+          ( B)
+          ( path-swap-nat-identification-left-whisk β α)
+          ( b))
+        ( tr-concat p' q' b))
+      ( ( identification-right-whisk
+          ( tr²-concat
+            ( identification-right-whisk α q)
+            ( identification-left-whisk p' β) b)
+          ( tr-concat p' q' b)) ∙
+      ( vertical-concat-square
+        ( tr² B (identification-right-whisk α q) b)
+        ( tr² B (identification-left-whisk p' β) b)
+        ( tr-concat p' q' b)
+        ( tr-concat p' q b)
+        ( tr-concat p q b)
+        ( htpy-left-whisk (tr B q) (tr² B α) b)
+        ( htpy-right-whisk (tr² B β) (tr B p') b)
+        ( tr²-right-whisk α q b)
+        ( tr²-left-whisk p' β b)))
+      ( ( identification-right-whisk
+          ( tr²-concat (identification-left-whisk p β)
+          ( identification-right-whisk α q') b)
+          ( tr-concat p' q' b)) ∙
+      ( vertical-concat-square
+        ( tr² B (identification-left-whisk p β) b)
+        ( tr² B (identification-right-whisk α q') b)
+        ( tr-concat p' q' b)
+        ( tr-concat p q' b)
+        ( tr-concat p q b)
+        ( htpy-right-whisk (tr² B β) (tr B p) b)
+        ( htpy-left-whisk (tr B q') (tr² B α) b)
+        ( tr²-left-whisk p β b)
+        ( tr²-right-whisk α q' b)))
+      ( identification-left-whisk
+        ( tr-concat p q b)
+        ( htpy-swap-nat-right-htpy (tr² B β) (tr² B α) b))
+  tr³-htpy-swap-path-swap {q = refl} refl {p = refl} refl b = refl
+```
