Retracts of maps (#900)

UniMath · Nov 5, 2023 · 5e15f6b · 5e15f6b
1 parent 52fdf4c
commit 5e15f6b
Show file tree

Hide file tree

Showing 17 changed files with 700 additions and 101 deletions.
diff --git a/src/foundation-core/commuting-squares-of-maps.lagda.md b/src/foundation-core/commuting-squares-of-maps.lagda.md
@@ -35,12 +35,16 @@ is said to commute if there is a homotopy between both composites.
 ## Definitions
 
 ```agda
-coherence-square-maps :
+module _
   {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4}
-  (top : C → B) (left : C → A) (right : B → X) (bottom : A → X) →
-  UU (l3 ⊔ l4)
-coherence-square-maps top left right bottom =
-  bottom ∘ left ~ right ∘ top
+  (top : C → B) (left : C → A) (right : B → X) (bottom : A → X)
+  where
+
+  coherence-square-maps : UU (l3 ⊔ l4)
+  coherence-square-maps = bottom ∘ left ~ right ∘ top
+
+  coherence-square-maps' : UU (l3 ⊔ l4)
+  coherence-square-maps' = right ∘ top ~ bottom ∘ left
 ```
 
 ## Properties

diff --git a/src/foundation-core/equality-dependent-pair-types.lagda.md b/src/foundation-core/equality-dependent-pair-types.lagda.md
@@ -72,9 +72,12 @@ module _
     {x : A} {s t : B x} → s ＝ t → (x , s) ＝ (x , t)
   eq-pair-eq-pr2 {x} = ap {B = Σ A B} (pair x)
 
+  ap-pr1-eq-pair-eq-pr2 :
+    {x : A} {s t : B x} (p : s ＝ t) → ap pr1 (eq-pair-eq-pr2 p) ＝ refl
+  ap-pr1-eq-pair-eq-pr2 refl = refl
+
   is-retraction-pair-eq-Σ :
-    (s t : Σ A B) →
-    ((pair-eq-Σ {s} {t}) ∘ (eq-pair-Σ' {s} {t})) ~ id {A = Eq-Σ s t}
+    (s t : Σ A B) → pair-eq-Σ {s} {t} ∘ eq-pair-Σ' {s} {t} ~ id {A = Eq-Σ s t}
   is-retraction-pair-eq-Σ (pair x y) (pair .x .y) (pair refl refl) = refl
 
   is-section-pair-eq-Σ :
@@ -104,7 +107,7 @@ module _
   equiv-pair-eq-Σ s t = pair pair-eq-Σ (is-equiv-pair-eq-Σ s t)
 
   η-pair : (t : Σ A B) → (pair (pr1 t) (pr2 t)) ＝ t
-  η-pair t = eq-pair-Σ refl refl
+  η-pair t = refl
 
   eq-base-eq-pair : {s t : Σ A B} → (s ＝ t) → (pr1 s ＝ pr1 t)
   eq-base-eq-pair p = pr1 (pair-eq-Σ p)

diff --git a/src/foundation-core/fibers-of-maps.lagda.md b/src/foundation-core/fibers-of-maps.lagda.md
@@ -53,7 +53,7 @@ module _
   where
 
   Eq-fiber : fiber f b → fiber f b → UU (l1 ⊔ l2)
-  Eq-fiber s t = Σ (pr1 s ＝ pr1 t) (λ α → ((ap f α) ∙ (pr2 t)) ＝ (pr2 s))
+  Eq-fiber s t = Σ (pr1 s ＝ pr1 t) (λ α → ap f α ∙ pr2 t ＝ pr2 s)
 
   refl-Eq-fiber : (s : fiber f b) → Eq-fiber s s
   pr1 (refl-Eq-fiber s) = refl
@@ -66,16 +66,15 @@ module _
   eq-Eq-fiber-uncurry (refl , refl) = refl
 
   eq-Eq-fiber :
-    {s t : fiber f b} (α : pr1 s ＝ pr1 t) →
-    ((ap f α) ∙ (pr2 t)) ＝ pr2 s → s ＝ t
+    {s t : fiber f b} (α : pr1 s ＝ pr1 t) → ap f α ∙ pr2 t ＝ pr2 s → s ＝ t
   eq-Eq-fiber α β = eq-Eq-fiber-uncurry (α , β)
 
   is-section-eq-Eq-fiber :
-    {s t : fiber f b} → (Eq-eq-fiber {s} {t} ∘ eq-Eq-fiber-uncurry {s} {t}) ~ id
+    {s t : fiber f b} → Eq-eq-fiber {s} {t} ∘ eq-Eq-fiber-uncurry {s} {t} ~ id
   is-section-eq-Eq-fiber (refl , refl) = refl
 
   is-retraction-eq-Eq-fiber :
-    {s t : fiber f b} → (eq-Eq-fiber-uncurry {s} {t} ∘ Eq-eq-fiber {s} {t}) ~ id
+    {s t : fiber f b} → eq-Eq-fiber-uncurry {s} {t} ∘ Eq-eq-fiber {s} {t} ~ id
   is-retraction-eq-Eq-fiber refl = refl
 
   abstract
@@ -112,7 +111,7 @@ module _
   where
 
   Eq-fiber' : fiber' f b → fiber' f b → UU (l1 ⊔ l2)
-  Eq-fiber' s t = Σ (pr1 s ＝ pr1 t) (λ α → (pr2 t ＝ ((pr2 s) ∙ (ap f α))))
+  Eq-fiber' s t = Σ (pr1 s ＝ pr1 t) (λ α → pr2 t ＝ pr2 s ∙ ap f α)
 
   refl-Eq-fiber' : (s : fiber' f b) → Eq-fiber' s s
   pr1 (refl-Eq-fiber' s) = refl
@@ -126,18 +125,17 @@ module _
     ap (pair x) (inv right-unit)
 
   eq-Eq-fiber' :
-    {s t : fiber' f b} (α : pr1 s ＝ pr1 t) →
-    (pr2 t) ＝ ((pr2 s) ∙ (ap f α)) → s ＝ t
+    {s t : fiber' f b} (α : pr1 s ＝ pr1 t) → pr2 t ＝ pr2 s ∙ ap f α → s ＝ t
   eq-Eq-fiber' α β = eq-Eq-fiber-uncurry' (α , β)
 
   is-section-eq-Eq-fiber' :
     {s t : fiber' f b} →
-    (Eq-eq-fiber' {s} {t} ∘ eq-Eq-fiber-uncurry' {s} {t}) ~ id
+    Eq-eq-fiber' {s} {t} ∘ eq-Eq-fiber-uncurry' {s} {t} ~ id
   is-section-eq-Eq-fiber' {x , refl} (refl , refl) = refl
 
   is-retraction-eq-Eq-fiber' :
     {s t : fiber' f b} →
-    (eq-Eq-fiber-uncurry' {s} {t} ∘ Eq-eq-fiber' {s} {t}) ~ id
+    eq-Eq-fiber-uncurry' {s} {t} ∘ Eq-eq-fiber' {s} {t} ~ id
   is-retraction-eq-Eq-fiber' {x , refl} refl = refl
 
   abstract
@@ -182,11 +180,10 @@ module _
   pr1 (map-inv-equiv-fiber (x , refl)) = x
   pr2 (map-inv-equiv-fiber (x , refl)) = refl
 
-  is-section-map-inv-equiv-fiber : (map-equiv-fiber ∘ map-inv-equiv-fiber) ~ id
+  is-section-map-inv-equiv-fiber : map-equiv-fiber ∘ map-inv-equiv-fiber ~ id
   is-section-map-inv-equiv-fiber (x , refl) = refl
 
-  is-retraction-map-inv-equiv-fiber :
-    (map-inv-equiv-fiber ∘ map-equiv-fiber) ~ id
+  is-retraction-map-inv-equiv-fiber : map-inv-equiv-fiber ∘ map-equiv-fiber ~ id
   is-retraction-map-inv-equiv-fiber (x , refl) = refl
 
   is-equiv-map-equiv-fiber : is-equiv map-equiv-fiber
@@ -315,13 +312,11 @@ module _
   inv-map-compute-fiber-comp :
     Σ (fiber g x) (λ t → fiber h (pr1 t)) → fiber (g ∘ h) x
   pr1 (inv-map-compute-fiber-comp t) = pr1 (pr2 t)
-  pr2 (inv-map-compute-fiber-comp t) =
-    ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
+  pr2 (inv-map-compute-fiber-comp t) = ap g (pr2 (pr2 t)) ∙ pr2 (pr1 t)
 
   is-section-inv-map-compute-fiber-comp :
     (map-compute-fiber-comp ∘ inv-map-compute-fiber-comp) ~ id
-  is-section-inv-map-compute-fiber-comp
-    ((.(h a) , refl) , (a , refl)) = refl
+  is-section-inv-map-compute-fiber-comp ((.(h a) , refl) , (a , refl)) = refl
 
   is-retraction-inv-map-compute-fiber-comp :
     (inv-map-compute-fiber-comp ∘ map-compute-fiber-comp) ~ id

diff --git a/src/foundation-core/identity-types.lagda.md b/src/foundation-core/identity-types.lagda.md
@@ -156,15 +156,19 @@ module _
 ### Transposing inverses
 
 ```agda
-left-transpose-eq-concat :
-  {l : Level} {A : UU l} {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z)
-  (r : x ＝ z) → ((p ∙ q) ＝ r) → q ＝ ((inv p) ∙ r)
-left-transpose-eq-concat refl q r s = s
-
-right-transpose-eq-concat :
-  {l : Level} {A : UU l} {x y : A} (p : x ＝ y) {z : A} (q : y ＝ z)
-  (r : x ＝ z) → ((p ∙ q) ＝ r) → p ＝ (r ∙ (inv q))
-right-transpose-eq-concat p refl r s = ((inv right-unit) ∙ s) ∙ (inv right-unit)
+module _
+  {l : Level} {A : UU l} {x y : A}
+  where
+
+  left-transpose-eq-concat :
+    (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
+    p ∙ q ＝ r → q ＝ inv p ∙ r
+  left-transpose-eq-concat refl q r s = s
+
+  right-transpose-eq-concat :
+    (p : x ＝ y) {z : A} (q : y ＝ z) (r : x ＝ z) →
+    p ∙ q ＝ r → p ＝ r ∙ inv q
+  right-transpose-eq-concat p refl r s = (inv right-unit ∙ s) ∙ inv right-unit
 ```
 
 The fact that `left-transpose-eq-concat` and `right-transpose-eq-concat` are

diff --git a/src/foundation-core/retractions.lagda.md b/src/foundation-core/retractions.lagda.md
@@ -26,7 +26,9 @@ A **retraction** is a map that has a right inverse, i.e. a section. Thus,
 homotopic to the identity at `A`. Moreover, in this case we say that `A` _is a
 retract of_ `B`.
 
-## Definition
+## Definitions
+
+### The type of retractions
 
 ```agda
 module _
@@ -40,11 +42,14 @@ module _
   map-retraction f = pr1
 
   is-retraction-map-retraction :
-    (f : A → B) (r : retraction f) → (map-retraction f r ∘ f) ~ id
+    (f : A → B) (r : retraction f) → map-retraction f r ∘ f ~ id
   is-retraction-map-retraction f = pr2
+```
 
-_retract-of_ :
-  {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
+### Retracts of a type
+
+```agda
+_retract-of_ : {l1 l2 : Level} → UU l1 → UU l2 → UU (l1 ⊔ l2)
 A retract-of B = Σ (A → B) retraction
 
 module _
@@ -58,13 +63,12 @@ module _
     (R : A retract-of B) → retraction (section-retract-of R)
   retraction-section-retract-of = pr2
 
-  retraction-retract-of : (A retract-of B) → B → A
+  retraction-retract-of : A retract-of B → B → A
   retraction-retract-of R = pr1 (retraction-section-retract-of R)
 
-  is-retraction-retraction-retract-of :
-    (R : A retract-of B) →
-    (retraction-retract-of R ∘ section-retract-of R) ~ id
-  is-retraction-retraction-retract-of R = pr2 (retraction-section-retract-of R)
+  is-retract-retract-of :
+    (R : A retract-of B) → retraction-retract-of R ∘ section-retract-of R ~ id
+  is-retract-retract-of R = pr2 (retraction-section-retract-of R)
 ```
 
 ## Properties

diff --git a/src/foundation/commuting-squares-of-homotopies.lagda.md b/src/foundation/commuting-squares-of-homotopies.lagda.md
@@ -24,11 +24,11 @@ A square of [homotopies](foundation-core.homotopies.md)
       |         |
  left |         | right
       v         v
-      z ------> i
+      h ------> i
         bottom
 ```
 
-is said to **commute** if there is a homotopy `left ∙h bottom ~ top ∙h right`.
+is said to **commute** if there is a homotopy `left ∙h bottom ~ top ∙h right `.
 Such a homotopy is called a **coherence** of the square.
 
 ## Definition
@@ -39,7 +39,7 @@ module _
   where
 
   coherence-square-homotopies :
-    (left : f ~ h) (bottom : h ~ i) (top : f ~ g) (right : g ~ i) → UU (l1 ⊔ l2)
-  coherence-square-homotopies left bottom top right =
+    (top : f ~ g) (left : f ~ h) (right : g ~ i) (bottom : h ~ i) → UU (l1 ⊔ l2)
+  coherence-square-homotopies top left right bottom =
     left ∙h bottom ~ top ∙h right
 ```
diff --git a/src/foundation/commuting-squares-of-identifications.lagda.md b/src/foundation/commuting-squares-of-identifications.lagda.md
@@ -45,7 +45,7 @@ module _
   coherence-square-identifications :
     (top : x ＝ y) (left : x ＝ z) (right : y ＝ w) (bottom : z ＝ w) → UU l
   coherence-square-identifications top left right bottom =
-    (left ∙ bottom) ＝ (top ∙ right)
+    left ∙ bottom ＝ top ∙ right
 ```
 
 ## Operations

diff --git a/src/foundation/equality-fibers-of-maps.lagda.md b/src/foundation/equality-fibers-of-maps.lagda.md
@@ -37,7 +37,7 @@ For any map `f : A → B` any `b : B` and any `x y : fiber f b`, there is an
 equivalence
 
 ```text
-(x ＝ y) ≃ fiber (ap f) ((pr2 x) ∙ (inv (pr2 y)))
+(x ＝ y) ≃ fiber (ap f) (pr2 x ∙ inv (pr2 y))
 ```
 
 ### Proof
@@ -48,19 +48,16 @@ module _
   where
 
   fiber-ap-eq-fiber-fiberwise :
-    (s t : fiber f b) (p : (pr1 s) ＝ (pr1 t)) →
-    ((tr (λ (a : A) → (f a) ＝ b) p (pr2 s)) ＝ (pr2 t)) →
-    (ap f p ＝ ((pr2 s) ∙ (inv (pr2 t))))
-  fiber-ap-eq-fiber-fiberwise (pair .x' p) (pair x' refl) refl =
-    inv ∘ (concat right-unit refl)
+    (s t : fiber f b) (p : pr1 s ＝ pr1 t) →
+    tr (λ (a : A) → f a ＝ b) p (pr2 s) ＝ pr2 t →
+    ap f p ＝ pr2 s ∙ inv (pr2 t)
+  fiber-ap-eq-fiber-fiberwise (.x' , p) (x' , refl) refl =
+    inv ∘ concat right-unit refl
 
   abstract
     is-fiberwise-equiv-fiber-ap-eq-fiber-fiberwise :
       (s t : fiber f b) → is-fiberwise-equiv (fiber-ap-eq-fiber-fiberwise s t)
-    is-fiberwise-equiv-fiber-ap-eq-fiber-fiberwise
-      ( pair x y)
-      ( pair .x refl)
-      ( refl) =
+    is-fiberwise-equiv-fiber-ap-eq-fiber-fiberwise (x , y) (.x , refl) refl =
       is-equiv-comp
         ( inv)
         ( concat right-unit refl)
@@ -69,15 +66,15 @@ module _
 
   fiber-ap-eq-fiber :
     (s t : fiber f b) → s ＝ t →
-    fiber (ap f {x = pr1 s} {y = pr1 t}) ((pr2 s) ∙ (inv (pr2 t)))
+    fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t))
   pr1 (fiber-ap-eq-fiber s .s refl) = refl
   pr2 (fiber-ap-eq-fiber s .s refl) = inv (right-inv (pr2 s))
 
   triangle-fiber-ap-eq-fiber :
     (s t : fiber f b) →
-    ( fiber-ap-eq-fiber s t) ~
-    ( (tot (fiber-ap-eq-fiber-fiberwise s t)) ∘ (pair-eq-Σ {s = s} {t}))
-  triangle-fiber-ap-eq-fiber (pair x refl) .(pair x refl) refl = refl
+    fiber-ap-eq-fiber s t ~
+    tot (fiber-ap-eq-fiber-fiberwise s t) ∘ pair-eq-Σ {s = s} {t}
+  triangle-fiber-ap-eq-fiber (x , refl) .(x , refl) refl = refl
 
   abstract
     is-equiv-fiber-ap-eq-fiber :
@@ -94,28 +91,41 @@ module _
 
   equiv-fiber-ap-eq-fiber :
     (s t : fiber f b) →
-    (s ＝ t) ≃ fiber (ap f {x = pr1 s} {y = pr1 t}) ((pr2 s) ∙ (inv (pr2 t)))
+    (s ＝ t) ≃ fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t))
   pr1 (equiv-fiber-ap-eq-fiber s t) = fiber-ap-eq-fiber s t
   pr2 (equiv-fiber-ap-eq-fiber s t) = is-equiv-fiber-ap-eq-fiber s t
 
+  map-inv-fiber-ap-eq-fiber :
+    (s t : fiber f b) →
+    fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t)) →
+    s ＝ t
+  map-inv-fiber-ap-eq-fiber (x , refl) (.x , p) (refl , u) =
+    eq-pair-eq-pr2 (ap inv u ∙ inv-inv p)
+
+  ap-pr1-map-inv-fiber-ap-eq-fiber :
+    (s t : fiber f b) →
+    (v : fiber (ap f {x = pr1 s} {y = pr1 t}) (pr2 s ∙ inv (pr2 t))) →
+    ap pr1 (map-inv-fiber-ap-eq-fiber s t v) ＝ pr1 v
+  ap-pr1-map-inv-fiber-ap-eq-fiber (x , refl) (.x , p) (refl , u) =
+    ap-pr1-eq-pair-eq-pr2 (ap inv u ∙ inv-inv p)
+
 module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (x y : A)
   where
 
   eq-fiber-fiber-ap :
-    (q : f x ＝ f y) → (pair x q) ＝ (pair y refl) → fiber (ap f {x} {y}) q
+    (q : f x ＝ f y) → (x , q) ＝ (y , refl) → fiber (ap f {x} {y}) q
   eq-fiber-fiber-ap q =
-    ( tr (fiber (ap f)) right-unit) ∘
-    ( fiber-ap-eq-fiber f (pair x q) (pair y refl))
+    tr (fiber (ap f)) right-unit ∘ fiber-ap-eq-fiber f (x , q) (y , refl)
 
   abstract
     is-equiv-eq-fiber-fiber-ap :
-      (q : (f x) ＝ (f y)) → is-equiv (eq-fiber-fiber-ap q)
+      (q : (f x) ＝ f y) → is-equiv (eq-fiber-fiber-ap q)
     is-equiv-eq-fiber-fiber-ap q =
       is-equiv-comp
         ( tr (fiber (ap f)) right-unit)
-        ( fiber-ap-eq-fiber f (pair x q) (pair y refl))
-        ( is-equiv-fiber-ap-eq-fiber f (pair x q) (pair y refl))
+        ( fiber-ap-eq-fiber f (x , q) (y , refl))
+        ( is-equiv-fiber-ap-eq-fiber f (x , q) (y , refl))
         ( is-equiv-tr (fiber (ap f)) right-unit)
 ```