Refactoring of retractions, sections, and equivalences, and adding the 6-for-2 property of equivalences

src/foundation-core/commuting-squares-of-maps.lagda.md

@@ -7,11 +7,13 @@ module foundation-core.commuting-squares-of-maps where
 <details><summary>Imports</summary>
 
 ```agda
+open import foundation.action-on-identifications-functions
 open import foundation.universe-levels
 
 open import foundation-core.commuting-triangles-of-maps
 open import foundation-core.function-types
 open import foundation-core.homotopies
+open import foundation-core.identity-types
 open import foundation-core.whiskering-homotopies
 ```
 
@@ -113,3 +115,110 @@ module _
       ( pasting-vertical-coherence-square-maps sq-top sq-bottom)) ∙h
     ( inv-htpy (K ·r top))
 ```
+
+### Associativity of horizontal pasting
+
+**Proof:** Consider a commuting diagram of the form
+
+```text
+        α₀       β₀       γ₀
+    A -----> X -----> U -----> K
+    |        |        |        |
+  f |   α  g |   β  h |   γ    | i
+    V        V        V        V
+    B -----> Y -----> V -----> L.
+        α₁       β₁       γ₁
+```
+
+Then we can make the following calculation, in which we write `□` for horizontal
+pasting of squares:
+
+```text
+  (α □ β) □ γ
+  ＝ (γ₁ ·l ((β₁ ·l α) ∙h (β ·r α₀))) ∙h (γ ·r (β₀ ∘ α₀))
+  ＝ ((γ₁ ·l (β₁ ·l α)) ∙h (γ₁ ·l (β ·r α₀))) ∙h (γ ·r (β₀ ∘ α₀))
+  ＝ ((γ₁ ∘ β₁) ·l α) ∙h (((γ₁ ·l β) ·r α₀) ∙h ((γ ·r β₀) ·r α₀))
+  ＝ ((γ₁ ∘ β₁) ·l α) ∙h (((γ₁ ·l β) ∙h (γ ·r β₀)) ·r α₀)
+  ＝ α □ (β □ γ)
+```
+
+```agda
+module _
+  {l1 l2 l3 l4 l5 l6 l7 l8 : Level}
+  {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4} {U : UU l5} {V : UU l6}
+  {K : UU l7} {L : UU l8}
+  (α₀ : A → X) (β₀ : X → U) (γ₀ : U → K)
+  (f : A → B) (g : X → Y) (h : U → V) (i : K → L)
+  (α₁ : B → Y) (β₁ : Y → V) (γ₁ : V → L)
+  (α : coherence-square-maps α₀ f g α₁)
+  (β : coherence-square-maps β₀ g h β₁)
+  (γ : coherence-square-maps γ₀ h i γ₁)
+  where
+
+  assoc-pasting-horizontal-coherence-square-maps :
+    pasting-horizontal-coherence-square-maps
+      ( β₀ ∘ α₀)
+      ( γ₀)
+      ( f)
+      ( h)
+      ( i)
+      ( β₁ ∘ α₁)
+      ( γ₁)
+      ( pasting-horizontal-coherence-square-maps α₀ β₀ f g h α₁ β₁ α β)
+      ( γ) ~
+    pasting-horizontal-coherence-square-maps
+      ( α₀)
+      ( γ₀ ∘ β₀)
+      ( f)
+      ( g)
+      ( i)
+      ( α₁)
+      ( γ₁ ∘ β₁)
+      ( α)
+      ( pasting-horizontal-coherence-square-maps β₀ γ₀ g h i β₁ γ₁ β γ)
+  assoc-pasting-horizontal-coherence-square-maps a =
+    ( ap
+      ( _∙ _)
+      ( ( ap-concat γ₁ (ap β₁ (α a)) (β (α₀ a))) ∙
+        ( inv (ap (_∙ _) (ap-comp γ₁ β₁ (α a)))))) ∙
+    ( assoc (ap (γ₁ ∘ β₁) (α a)) (ap γ₁ (β (α₀ a))) (γ (β₀ (α₀ a))))
+```
+
+### The unit laws for horizontal pasting of commuting squares of maps
+
+#### The left unit law
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (i : A → X) (f : A → B) (g : X → Y) (j : B → Y)
+  (α : coherence-square-maps i f g j)
+  where
+
+  left-unit-law-pasting-horizontal-coherence-square-maps :
+    pasting-horizontal-coherence-square-maps id i f f g id j refl-htpy α ~ α
+  left-unit-law-pasting-horizontal-coherence-square-maps = refl-htpy
+```
+
+### The right unit law
+
+```agda
+module _
+  {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {X : UU l3} {Y : UU l4}
+  (i : A → X) (f : A → B) (g : X → Y) (j : B → Y)
+  (α : coherence-square-maps i f g j)
+  where
+
+  right-unit-law-pasting-horizontal-coherence-square-maps :
+    pasting-horizontal-coherence-square-maps i id f g g j id α refl-htpy ~ α
+  right-unit-law-pasting-horizontal-coherence-square-maps a =
+    right-unit ∙ ap-id (α a)
+```
+
+## See also
+
+Several structures make essential use of commuting squares of maps:
+
+- [Cones over cospans](foundation.cones-over-cospans.md)
+- [Cocones under spans](synthetic-homotopy-theory.cocones-under-spans.md)
+- [Morphisms of arrows](foundation.morphisms-arrows.md)

src/foundation-core/commuting-triangles-of-maps.lagda.md

@@ -10,8 +10,9 @@ module foundation-core.commuting-triangles-of-maps where
 open import foundation.universe-levels
 
 open import foundation-core.function-types
-open import foundation-core.functoriality-function-types
 open import foundation-core.homotopies
+open import foundation-core.retractions
+open import foundation-core.sections
 open import foundation-core.whiskering-homotopies
 ```
 
@@ -22,16 +23,16 @@ open import foundation-core.whiskering-homotopies
 A triangle of maps
 
 ```text
-      top
-   A ----> B
-    \     /
-left \   / right
-      V V
-       X
+        top
+     A ----> B
+      \     /
+  left \   / right
+        V V
+         X
 ```
 
-is said to commute if there is a homotopy between the map on the left and the
-composite map
+is said to **commute** if there is a [homotopy](foundation-core.homotopies.md)
+between the map on the left and the composite of the top and right maps:
 
 ```text
   left ~ right ∘ top.
@@ -71,46 +72,88 @@ module _
     H ∙h (K ·r i)
 ```
 
-### Any commuting triangle of maps induces a commuting triangle of function spaces
+### Coherences of commuting triangles of maps with fixed vertices
+
+This or its opposite should be the coherence in the characterization of
+identifications of commuting triangles of maps with fixed end vertices.
 
 ```agda
 module _
-  { l1 l2 l3 l4 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
-  ( left : A → X) (right : B → X) (top : A → B)
+  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
+  (left : A → X) (right : B → X) (top : A → B)
+  (left' : A → X) (right' : B → X) (top' : A → B)
+  (c : coherence-triangle-maps left right top)
+  (c' : coherence-triangle-maps left' right' top')
   where
 
-  precomp-coherence-triangle-maps :
-    coherence-triangle-maps left right top →
-    ( W : UU l4) →
-    coherence-triangle-maps
-      ( precomp left W)
-      ( precomp top W)
-      ( precomp right W)
-  precomp-coherence-triangle-maps H W = htpy-precomp H W
-
-  precomp-coherence-triangle-maps' :
-    coherence-triangle-maps' left right top →
-    ( W : UU l4) →
-    coherence-triangle-maps'
-      ( precomp left W)
-      ( precomp top W)
-      ( precomp right W)
-  precomp-coherence-triangle-maps' H W = htpy-precomp H W
+  coherence-htpy-triangle-maps :
+    left ~ left' → right ~ right' → top ~ top' → UU (l1 ⊔ l2)
+  coherence-htpy-triangle-maps L R T =
+    c ∙h htpy-comp-horizontal T R ~ L ∙h c'
 ```
 
-### Coherences of commuting triangles of maps with fixed vertices
+## Properties
 
-This or its opposite should be the coherence in the characterization of
-identifications of commuting triangles of maps with fixed end vertices.
+### If the top map has a section, then the reversed triangle with the section on top commutes
+
+If `t : B → A` is a [section](foundation-core.sections.md) of the top map `h`,
+then the triangle
+
+```text
+       t
+  B ------> A
+   \       /
+   g\     /f
+     \   /
+      V V
+       X,
+```
+
+commutes.
 
 ```agda
-coherence-htpy-triangle-maps :
-  {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3}
-  (left : A → X) (right : B → X) (top : A → B)
-  (left' : A → X) (right' : B → X) (top' : A → B) →
-  coherence-triangle-maps left right top →
-  coherence-triangle-maps left' right' top' →
-  left ~ left' → right ~ right' → top ~ top' → UU (l1 ⊔ l2)
-coherence-htpy-triangle-maps left right top left' right' top' c c' L R T =
-  c ∙h htpy-comp-horizontal T R ~ L ∙h c'
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) (h : A → B) (H : coherence-triangle-maps f g h)
+  (t : section h)
+  where
+
+  inv-triangle-section : coherence-triangle-maps' g f (map-section h t)
+  inv-triangle-section =
+    (H ·r map-section h t) ∙h (g ·l is-section-map-section h t)
+
+  triangle-section : coherence-triangle-maps g f (map-section h t)
+  triangle-section = inv-htpy inv-triangle-section
+```
+
+### If the right map has a retraction, then the reversed triangle with the retraction on the right commutes
+
+If `r : X → B` is a retraction of the right map `g` in a triangle `f ~ g ∘ h`,
+then the triangle
+
+```text
+       f
+  A ------> X
+   \       /
+   h\     /r
+     \   /
+      V V
+       B,
+```
+
+commutes.
+
+```agda
+module _
+  {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3}
+  (f : A → X) (g : B → X) (h : A → B) (H : coherence-triangle-maps f g h)
+  (r : retraction g)
+  where
+
+  inv-triangle-retraction : coherence-triangle-maps' h (map-retraction g r) f
+  inv-triangle-retraction =
+    (map-retraction g r ·l H) ∙h (is-retraction-map-retraction g r ·r h)
+
+  triangle-retraction : coherence-triangle-maps h (map-retraction g r) f
+  triangle-retraction = inv-htpy inv-triangle-retraction
 ```

src/foundation-core/contractible-types.lagda.md

@@ -12,6 +12,7 @@ open import foundation.dependent-pair-types
 open import foundation.equality-cartesian-product-types
 open import foundation.function-extensionality
 open import foundation.implicit-function-types
+open import foundation.retracts-of-types
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types