Refactor Eckmann-Hilton

src/foundation.lagda.md

@@ -137,6 +137,7 @@ open import foundation.functoriality-set-truncation public
 open import foundation.functoriality-truncation public
 open import foundation.fundamental-theorem-of-identity-types public
 open import foundation.global-choice public
+open import foundation.higher-transport-along-identifications public
 open import foundation.hilberts-epsilon-operators public
 open import foundation.homotopies public
 open import foundation.homotopy-induction public

src/foundation/dependent-identifications.lagda.md

@@ -11,6 +11,7 @@ open import foundation-core.dependent-identifications public
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.dependent-pair-types
+open import foundation.higher-transport-along-identifications
 open import foundation.transport-along-identifications
 open import foundation.universe-levels
 

src/foundation/higher-transport-along-identifications.lagda.md

@@ -0,0 +1,147 @@
+# Higher transport along identifications
+
+```agda
+module foundation.higher-transport-along-identifications where
+```
+
+<details><summary>Imports</summary>
+
+```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.identity-types
+open import foundation.path-algebra
+open import foundation.transport-along-identifications
+open import foundation.universe-levels
+open import foundation.whiskering-homotopies
+```
+
+</details>
+
+### The action on identifications of transport
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} {x y : A} {p p' : x ＝ y}
+  where
+
+  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) β
+```
+
+### Computing 2-dimensional transport in a family of identifications with a fixed source
+
+```agda
+module _
+  {l : Level} {A : UU l} {a b c : A} {q q' : b ＝ c}
+  where
+
+  tr²-Id-right :
+    (α : q ＝ q') (p : a ＝ b) →
+    coherence-square-identifications
+      ( tr² (Id a) α p)
+      ( tr-Id-right q' p)
+      ( tr-Id-right q p)
+      ( identification-left-whisk p α)
+  tr²-Id-right α p =
+    inv-nat-htpy (λ (t : b ＝ c) → tr-Id-right t p) α
+```
+
+### 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
+```

src/foundation/identity-types.lagda.md

@@ -11,6 +11,7 @@ open import foundation-core.identity-types public
 ```agda
 open import foundation.action-on-identifications-functions
 open import foundation.binary-equivalences
+open import foundation.commuting-squares-of-identifications
 open import foundation.dependent-pair-types
 open import foundation.equivalence-extensionality
 open import foundation.function-extensionality

src/foundation/path-algebra.lagda.md

@@ -229,7 +229,7 @@ horizontal-concat-Id² :
 horizontal-concat-Id² α β = ap-binary (λ s t → s ∙ t) α β
 ```
 
-#### Identification whiskering
+### Definition of identification whiskering
 
 ```agda
 module _
@@ -279,33 +279,17 @@ right-unit-law-vertical-concat-Id² = right-unit
 
 left-unit-law-horizontal-concat-Id² :
   {l : Level} {A : UU l} {x y z : A} {p : x ＝ y} {u v : y ＝ z} (γ : u ＝ v) →
-  horizontal-concat-Id² (refl {x = p}) γ ＝ ap (concat p z) γ
+  horizontal-concat-Id² (refl {x = p}) γ ＝
+  identification-left-whisk p γ
 left-unit-law-horizontal-concat-Id² γ = left-unit-ap-binary (λ s t → s ∙ t) γ
 
 right-unit-law-horizontal-concat-Id² :
   {l : Level} {A : UU l} {x y z : A} {p q : x ＝ y} (α : p ＝ q) {u : y ＝ z} →
-  horizontal-concat-Id² α (refl {x = u}) ＝ ap (concat' x u) α
+  horizontal-concat-Id² α (refl {x = u}) ＝
+  identification-right-whisk α u
 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.
 
@@ -316,20 +300,63 @@ module _
 
   nat-sq-right-unit-Id² :
     coherence-square-identifications
-      right-unit α (horizontal-concat-Id² α refl) right-unit
+      ( right-unit)
+      ( α)
+      ( horizontal-concat-Id² α refl)
+      ( right-unit)
   nat-sq-right-unit-Id² =
     ( ( horizontal-concat-Id² refl (inv (ap-id α))) ∙
       ( nat-htpy htpy-right-unit α)) ∙
     ( horizontal-concat-Id² (inv (right-unit-law-horizontal-concat-Id² α)) refl)
 
   nat-sq-left-unit-Id² :
     coherence-square-identifications
-      left-unit α (horizontal-concat-Id² (refl {x = refl}) α) left-unit
+      ( left-unit)
+      ( α)
+      ( horizontal-concat-Id² (refl {x = refl}) α)
+      ( left-unit)
   nat-sq-left-unit-Id² =
     ( ( (inv (ap-id α) ∙ (nat-htpy htpy-left-unit α)) ∙ right-unit) ∙
     ( inv (left-unit-law-horizontal-concat-Id² α))) ∙ inv right-unit
 ```
 
+### Unit laws for whiskering
+
+```agda
+module _
+  {l : Level} {A : UU l} {x y : A}
+  where
+
+  left-unit-law-identification-left-whisk :
+    {p p' : x ＝ y} (α : p ＝ p') →
+    identification-left-whisk refl α ＝ α
+  left-unit-law-identification-left-whisk refl = refl
+
+  right-unit-law-identification-right-whisk :
+    {p p' : x ＝ y} (α : p ＝ p') →
+    identification-right-whisk α refl ＝
+    right-unit ∙ α ∙ inv right-unit
+  right-unit-law-identification-right-whisk {p = refl} refl = refl
+```
+
+### 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 β)
+```
+
 ### Definition of horizontal inverse
 
 2-paths have an induced inverse operation from the operation on boundary 1-paths