Discrete fibers Cor. 8.20 RS17

src/hott/02-homotopies.rzk.md

@@ -132,6 +132,27 @@ $K^{-1} \cdot H  \sim \text{refl-htpy}_{g}$
       g
 ```
 
+## Composition of equal maps
+
+```rzk
+
+#def comp-homotopic-maps
+  ( A B C : U)
+  ( f g : A → B)
+  ( h k : B → C)
+  ( p : f = g)
+  ( q : h = k)
+  : comp A B C h f = comp A B C k g
+  :=
+    ind-path (A → B) f (\ g' p' → comp A B C h f = comp A B C k g')
+    ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f)
+      ( refl)
+      ( k)
+      ( q))
+    ( g)
+    ( p)
+```
+
 ## Naturality
 
 ```rzk title="The naturality square associated to a homotopy and a path"

src/hott/03-equivalences.rzk.md

@@ -813,6 +813,28 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to
   ( f g : (x : X) → A x)
   : ((x : X) → f x = g x) → (f = g)
   := first (first (funext X A f g))
+
+#def left-cancel-is-equiv uses (funext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  : (comp A B A (π₁ (π₁ is-equiv-f)) f) = (identity A)
+  :=
+    eq-htpy A (\ x' → A)
+    ( comp A B A (π₁ (π₁ is-equiv-f)) f)
+    ( identity A)
+    ( π₂ (π₁ is-equiv-f))
+
+#def right-cancel-is-equiv uses (funext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  : (comp B A B f (π₁ (π₂ is-equiv-f))) = (identity B)
+  :=
+    eq-htpy B (\ x' → B)
+    ( comp B A B f (π₁ (π₂ is-equiv-f)))
+    ( identity B)
+    ( π₂ (π₂ is-equiv-f))
 ```
 
 Using function extensionality, a fiberwise equivalence defines an equivalence of

src/simplicial-hott/03-extension-types.rzk.md

@@ -10,10 +10,8 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-- `hott/4-equivalences.rzk` — contains the definitions of `#!rzk Equiv` and
+- `hott/03-equivalences.rzk.md` — contains the definitions of `#!rzk Equiv` and
   `#!rzk comp-equiv`
-- the file `hott/4-equivalences.rzk` relies in turn on the previous files in
-  `hott/`
 
 ## Extension up to homotopy
 
@@ -356,6 +354,25 @@ For each of these we provide a corresponding functorial instance
       ( ( \ g → (\ t → (first (g t)) , \ t → second (g t)))
       , ( ( \ (f , h) t → (f t , h t) , \ _ → refl)
         , ( \ (f , h) t → (f t , h t) , \ _ → refl)))
+
+#def inv-equiv-axiom-choice
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( X : ψ → U)
+  ( Y : (t : ψ) → (x : X t) → U)
+  ( a : (t : ϕ) → X t)
+  ( b : (t : ϕ) → Y t (a t))
+  : Equiv
+    ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t]))
+      , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t]))
+    ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)])
+  :=
+    inv-equiv
+    ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)])
+    ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t]))
+      , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t]))
+    ( axiom-choice I ψ ϕ X Y a b)
 ```
 
 ## Composites and unions of cofibrations
@@ -1185,39 +1202,70 @@ Given a map `α : A' → A`, there is also a notion of relative extension types.
 #variable I : CUBE
 #variable ψ : I → TOPE
 #variable ϕ : ψ → TOPE
-#variables A' A : ψ → U
-#variable α : (t : ψ) → A' t → A t
-#variable σ' : (t : ϕ) → A' t
-#variable τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]
+#variables A B : ψ → U
+#variable f : (t : ψ) → A t → B t
+#variable a : (t : ϕ) → A t
+#variable τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]
 
 #def relative-extension-type
   : U
   :=
-    Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
-    , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
+    Σ ( τ' : (t : ψ) → A t [ϕ t ↦ a t])
+    , ( ( t : ψ) → (f t (τ' t) = τ t) [ϕ t ↦ refl])
+```
 
-#def relative-extension-type'
+This is equivalently expressed as the fibers of postcomposition by $f$.
+
+```rzk
+#def postcomp-Π-ext
+  : ((t : ψ) → A t [ϕ t ↦ a t]) →
+    ((t : ψ) → B t [ϕ t ↦ f t (a t)])
+  := ( \ τ' t → f t (τ' t))
+
+#def fiber-postcomp-Π-ext
   : U
   :=
     fib
-    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
-    ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
-    ( \ τ' t → α t (τ' t))
+    ( (t : ψ) → A t [ϕ t ↦ a t])
+    ( (t : ψ) → B t [ϕ t ↦ f t (a t)])
+    ( postcomp-Π-ext)
     ( τ)
 
 #def equiv-relative-extension-type-fib uses (extext)
   : Equiv
-    ( relative-extension-type')
+    ( fiber-postcomp-Π-ext)
     ( relative-extension-type)
   :=
     total-equiv-family-of-equiv
-    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
-    ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ)
-    ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
+    ( (t : ψ) → A t [ϕ t ↦ a t])
+    ( \ τ' → (\ t → f t (τ' t)) =_{ (t : ψ) → B t [ϕ t ↦ f t (a t)]} τ)
+    ( \ τ' → (t : ψ) → (f t (τ' t) = τ t) [ϕ t ↦ refl])
     ( \ τ' →
-      equiv-ExtExt extext I ψ ϕ A
-      ( \ t → α t (σ' t))
-      ( \ t → α t (τ' t)) ( τ))
+      equiv-ExtExt extext I ψ ϕ B
+      ( \ t → f t (a t))
+      ( \ t → f t (τ' t)) ( τ))
+```
+
+The fiber of postcomposition by a map $f: \prod_{t : I|\psi} A (t) \to B (t)$ is
+equivalent to the family of fibers of $f\_t$.
+
+```rzk
+#def fiber-family-ext
+  : U
+  := (t : ψ) → fib (A t) (B t) (f t) (τ t) [ϕ t ↦ (a t, refl)]
+
+#def equiv-fiber-postcomp-Π-ext-fiber-family-ext uses (extext)
+  : Equiv
+    ( fiber-postcomp-Π-ext)
+    ( fiber-family-ext)
+  :=
+    equiv-comp
+    ( fiber-postcomp-Π-ext)
+    ( relative-extension-type)
+    ( fiber-family-ext)
+    ( equiv-relative-extension-type-fib)
+    ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = τ t) a (\ t → refl))
+
 #end relative-extension-types
 ```
 
@@ -1345,9 +1393,7 @@ We can view it as a map of maps either vertically or horizontally.
     ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
     ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
   :=
-    ( ( ( \ a t → f t (a t))
-      , ( \ a t → f t (a t)))
-    , \ _ → refl)
+    ( ( (\ a t → f t (a t)), (\ a t → f t (a t))), \ _ → refl)
 
 #def map-of-map-extension-type
   ( I : CUBE)
@@ -1359,74 +1405,52 @@ We can view it as a map of maps either vertically or horizontally.
     ( (t : ψ) → A t) ( (t : ψ) → B t) (\ a t → f t (a t))
     ( (t : ϕ) → A t) ( (t : ϕ) → B t) (\ a t → f t (a t))
   :=
-    ( ( ( \ a t → a t)
-      , ( \ b t → b t))
-    , \ _ → refl)
+    ( ( (\ a t → a t), (\ b t → b t)), \ _ → refl)
 ```
 
 ### Equivalences induce equivalences of extension types
 
-We start by treating the case of extensions from the empty shape `BOT`.
-
-It follows from extension extensionality that if `f : A → B` is an equivalence,
-then so is the map of maps `map-of-restriction-maps`.
+If $f: \prod_{t : I|\psi} A (t) \to B (t)$ is a family of equivalence then the
+fibers of postcomposition by $f$ are contractible.
 
 ```rzk
-#def is-equiv-extensions-BOT-is-equiv uses (extext)
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( A B : ψ → U)
-  ( f : (t : ψ) → (A t) → (B t))
-  ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
-  : is-equiv ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t))
-  :=  ( ( ( \ b t → (first (first (is-equiv-f t))) (b t))
-        , ( \ a →
-            naiveextext-extext extext I ψ ( \ t → BOT)
-              ( A)
-              ( \ u → recBOT)
-              ( \ t → first (first (is-equiv-f t)) (f t (a t)))
-              ( a)
-              ( \ t → second (first (is-equiv-f t)) (a t))))
-      , ( ( \ b t → first (second (is-equiv-f t)) (b t))
-        , ( \ b →
-            naiveextext-extext extext I ψ ( \ t → BOT)
-              ( B)
-              ( \ u → recBOT)
-              ( \ t → f t (first (second (is-equiv-f t)) (b t)))
-              ( b)
-              ( \ t → second (second (is-equiv-f t)) (b t)))))
-
-#def equiv-extensions-BOT-equiv uses (extext)
+
+#def is-contr-fiber-family-ext-contr-fib
   ( I : CUBE)
   ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
   ( A B : ψ → U)
-  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
-  : Equiv ((t : ψ) → A t) ((t : ψ) → B t)
+  ( f : (t : ψ) → A t → B t)
+  ( a : (t : ϕ) → A t)
+  ( τ : (t : ψ) → B t [ϕ t ↦ f t (a t)])
+  ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
+  : is-contr (fiber-family-ext I ψ ϕ A B f a τ)
   :=
-    ( ( \ a t → first ( famequiv t) (a t))
-    , is-equiv-extensions-BOT-is-equiv I ψ A B
-      ( \ t → first (famequiv t))
-      ( \ t → second (famequiv t)))
+    (weakextext-extext extext) I ψ ϕ
+    ( \ t → fib (A t) (B t) (f t) (τ t))
+    ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (τ t))
+    ( \ t → (a t, refl))
 
-#def equiv-of-restriction-maps-equiv uses (extext)
+#def is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
   ( A B : ψ → U)
-  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
-  : Equiv-of-maps
-    ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
-    ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
-  :=
-    ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t))
-    , ( second (equiv-extensions-BOT-equiv I ψ A B famequiv)
-      , second ( equiv-extensions-BOT-equiv I
-                 (\ t → ϕ t) (\ t → A t) (\ t → B t) (\ t → famequiv t))))
+  ( f : (t : ψ) → A t → B t)
+  ( a : (t : ϕ) → A t)
+  ( τ : (t : ψ) → B t [ϕ t ↦ f t (a t)])
+  ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
+  : is-contr (fiber-postcomp-Π-ext I ψ ϕ A B f a τ)
+  :=
+    is-contr-equiv-is-contr'
+    ( fiber-postcomp-Π-ext I ψ ϕ A B f a τ)
+    ( fiber-family-ext I ψ ϕ A B f a τ)
+    ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B f a τ)
+    ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B f a τ family-equiv-f)
 ```
 
-Now we use the result for extensions of `BOT` to bootstrap to arbitrary
-extensions. We show that an equivalence `f : A → B` induces an equivalence of
-all extension types, not just those extended from `BOT`.
+Hence, postcomposing with an equivalence induces an equivalence of extension
+types.
 
 ```rzk
 #def is-equiv-extensions-is-equiv uses (extext)
@@ -1435,31 +1459,19 @@ all extension types, not just those extended from `BOT`.
   ( ϕ : ψ → TOPE)
   ( A B : ψ → U)
   ( f : (t : ψ) → A t → B t)
-  ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
-  : ( a : (t : ϕ) → A t)
-  → is-equiv
+  ( a : (t : ϕ) → A t)
+  ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
+  : is-equiv
     ( (t : ψ) → A t [ϕ t ↦ a t])
     ( (t : ψ) → B t [ϕ t ↦ f t (a t)])
-    ( \ a' t → f t (a' t))
+    ( postcomp-Π-ext I ψ ϕ A B f a)
   :=
-    is-homotopy-cartesian-is-horizontal-equiv
-    ( (t : ϕ) → A t)
-    ( \ a → (t : ψ) → A t [ϕ t ↦ a t])
-    ( (t : ϕ) → B t)
-    ( \ b → (t : ψ) → B t [ϕ t ↦ b t])
-    ( \ a t → f t (a t))
-    ( \ _ a' t → f t (a' t))
-    ( is-equiv-extensions-BOT-is-equiv
-      ( I) (\ t → ϕ t) (\ t → A t) (\ t → B t) ( \ t → f t)
-      ( \ (t : ϕ) → is-equiv-f t))
-    ( is-equiv-Equiv-is-equiv'
-        ( (t : ψ) → A t) ((t : ψ) → B t) (\ a' t → f t (a' t))
-        ( Σ (a : (t : ϕ) → A t) , ((t : ψ) → A t [ϕ t ↦ a t]))
-        ( Σ (b : (t : ϕ) → B t) , ((t : ψ) → B t [ϕ t ↦ b t]))
-        ( \ (a , a') → ( \ t → f t (a t) , \ t → f t (a' t)))
-      ( cofibration-composition-functorial
-        I ψ ϕ (\ _ → BOT) A B f (\ _ → recBOT))
-      ( is-equiv-extensions-BOT-is-equiv I ψ A B f is-equiv-f))
+    is-equiv-is-contr-map
+    ( (t : ψ) → A t [ϕ t ↦ a t])
+    ( (t : ψ) → B t [ϕ t ↦ f t (a t)])
+    ( postcomp-Π-ext I ψ ϕ A B f a)
+    ( \ τ →
+      is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B f a τ family-equiv-f)
 
 #def equiv-extensions-equiv uses (extext)
   ( I : CUBE)
@@ -1472,11 +1484,31 @@ all extension types, not just those extended from `BOT`.
     ( (t : ψ) → A t [ϕ t ↦ a t])
     ( (t : ψ) → B t [ϕ t ↦ first (equivs-A-B t) (a t)])
   :=
-  ( ( \ a' t → first (equivs-A-B t) (a' t))
-  , ( is-equiv-extensions-is-equiv I ψ ϕ A B
+    ( postcomp-Π-ext I ψ ϕ A B (\ t → (first (equivs-A-B t))) a
+    , is-equiv-extensions-is-equiv I ψ ϕ A B
       ( \ t → first (equivs-A-B t))
-      ( \ t → second (equivs-A-B t))
-      ( a)))
+      ( a)
+      ( \ t → second (equivs-A-B t)))
+
+#def equiv-of-restriction-maps-equiv uses (extext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
+  : Equiv-of-maps
+    ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
+    ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
+  :=
+    ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t))
+    , ( second (equiv-extensions-equiv I ψ ( \ _ → BOT)
+      ( A) ( B)
+      ( famequiv)
+      ( \ _ → recBOT))
+      , second ( equiv-extensions-equiv I ( \ t → ϕ t) ( \ _ → BOT)
+        ( \ t → A t) ( \ t → B t)
+        ( \ t → famequiv t)
+        ( \ _ → recBOT))))
 ```
 
 ### Retracts induce retracts of extension types
@@ -1508,8 +1540,9 @@ working with external retractions.
   :=
     is-equiv-extensions-is-equiv I ψ ϕ A A
     ( \ t a₀ → r t (s t (a₀)))
-    ( \ t → is-equiv-retraction-section (A t) (B t) (s t) (r t) (η t))
     ( a)
+    ( \ t → is-equiv-retraction-section (A t) (B t) (s t) (r t) (η t))
+
 
 #def has-retraction-extensions-has-retraction' uses (extext η)
   ( a : (t : ϕ) → A t)