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

@@ -331,6 +331,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

src/simplicial-hott/06-2cat-of-segal-types.rzk.md

@@ -10,17 +10,18 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
-  their subshapes.
-- `04-extension-types.rzk.md` — We use extension extensionality.
-- `05-segal-types.rzk.md` - We use the notion of hom types.
+- `3-simplicial-type-theory.md` — We rely on definitions of simplicies and their
+  subshapes.
+- `4-extension-types.md` — We use extension extensionality.
+- `5-segal-types.md` - We use the notion of hom types.
 
 Some of the definitions in this file rely on function extensionality and
 extension extensionality:
 
 ```rzk
 #assume funext : FunExt
 #assume extext : ExtExt
+#assume weakextext : WeakExtExt
 ```
 
 ## Functors
@@ -127,6 +128,58 @@ Preservation of composition requires the Segal hypothesis.
     ( functors-pres-comp A B is-segal-A is-segal-B F x y z f g)
 ```
 
+The action on morphisms commutes with transport.
+
+```rzk
+#def ap-hom-naturality
+  ( A B C : U)
+  ( f g : A → B)
+  ( h k : B → C)
+  ( p : f = g)
+  ( q : h = k)
+  ( x y : A)
+  : comp (hom B (f x) (f y)) (hom B (g x) (g y)) (hom C (k (g x)) (k (g y)))
+      ( ap-hom B C k (g x) (g y))
+      ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g p)
+    =
+    comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g x)) (k (g y)))
+      ( transport (A → C) (\ f' → hom C (f' x) (f' y))
+        ( comp A B C h f)
+        ( comp A B C k g)
+        ( comp-homotopic-maps A B C f g h k p q))
+      ( ap-hom B C h (f x) (f y))
+  :=
+    ind-path (A → B) f
+      ( \ g' p' →
+        comp (hom B (f x) (f y)) (hom B (g' x) (g' y)) (hom C (k (g' x)) (k (g' y)))
+          ( ap-hom B C k (g' x) (g' y))
+          ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g' p')
+        =
+        comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g' x)) (k (g' y)))
+          ( transport (A → C) (\ f' → hom C (f' x) (f' y))
+            ( comp A B C h f)
+            ( comp A B C k g')
+            ( comp-homotopic-maps A B C f g' h k p' q))
+          ( ap-hom B C h (f x) (f y)))
+      ( ind-path (B → C) h
+          ( \ k' q' →
+            comp (hom B (f x) (f y)) (hom B (f x) (f y)) (hom C (k' (f x)) (k' (f y)))
+              ( ap-hom B C k' (f x) (f y))
+              ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f f refl)
+            =
+            comp (hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k' (f x)) (k' (f y)))
+              ( transport (A → C) (\ f' → hom C (f' x) (f' y))
+                ( comp A B C h f)
+                ( comp A B C k' f)
+                ( comp-homotopic-maps A B C f f h k' refl q'))
+              ( ap-hom B C h (f x) (f y)))
+            ( refl)
+          ( k)
+          ( q))
+      ( g)
+      ( p)
+```
+
 ## Natural transformations
 
 Given two simplicial maps `#!rzk f g : (x : A) → B x` , a **natural
@@ -440,3 +493,212 @@ the "Gray interchanger" built from two commutative triangles.
     ( horizontal-comp-nat-trans A B C f g f' g' η η')
   := \ (t, s) a → η' t (η s a)
 ```
+
+## Equivalences are fully faithful
+
+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 postcomp-Π-ext
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → (A t → B t))
+  : ((t : ψ) → A t [ϕ t ↦ a t]) → ((t : ψ) → B t [ϕ t ↦ f t (a t)])
+  := ( \ α t → f t (α t))
+
+#def fiber-postcomp-Π-ext -- already defined as relative extension type in 03-extension-types
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → (A t → B t))
+  ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)])
+  : U
+  :=
+    fib
+      ( (t : ψ) → A t [ϕ t ↦ a t])
+      ( (t : ψ) → B t [ϕ t ↦ f t (a t)])
+      ( postcomp-Π-ext I ψ ϕ A B a f)
+      ( β)
+
+#def fiber-family-ext
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → (A t → B t))
+  ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)])
+  : U
+  :=
+    (t : ψ) → fib (A t) (B t) (f t) (β t) [ϕ t ↦ (a t, refl)]
+
+#def equiv-fiber-postcomp-Π-ext-fiber-family-ext
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → (A t → B t))
+  ( β : (t : ψ) → B t [ϕ t ↦ f t (a t)])
+  : Equiv
+    ( fiber-postcomp-Π-ext I ψ ϕ A B a f β)
+    ( fiber-family-ext I ψ ϕ A B a f β)
+  :=
+    equiv-comp
+      ( fiber-postcomp-Π-ext I ψ ϕ A B a f β)
+      ( relative-extension-type I ψ ϕ A B f a β)
+      ( fiber-family-ext I ψ ϕ A B a f β)
+      ( equiv-relative-extension-type-fib extext I ψ ϕ A B f a β)
+      ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = β t) a (\ t → refl))
+```
+
+In particular, 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-contr-fiber-family-ext-contr-fib
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → (A t → B 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 a f β)
+  :=
+    weakextext 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 is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (weakextext extext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → (A t → B 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 a f β)
+  :=
+    is-contr-equiv-is-contr'
+      ( fiber-postcomp-Π-ext I ψ ϕ A B a f β)
+      ( fiber-family-ext I ψ ϕ A B a f β)
+      ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B a f β)
+      ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B a f β family-equiv-f)
+
+#def is-equiv-postcomp-Π-ext-is-equiv uses (weakextext extext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( a : (t : ϕ) → A t)
+  ( f : (t : ψ) → (A t → B 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)])
+      ( postcomp-Π-ext I ψ ϕ A B a 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 a f)
+      ( \ β → is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B a f β family-equiv-f)
+```
+
+Using this result we can show that `#!rzk ap-hom` is an equivalence when f is an
+equivalence.
+
+```rzk
+#def is-equiv-ap-hom-is-equiv uses (weakextext extext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  ( x y : A)
+  : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y)
+  :=
+    is-equiv-postcomp-Π-ext-is-equiv 2 Δ¹ ∂Δ¹
+        ( \ t → A)
+        ( \ t → B)
+        ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y))
+        ( \ t → f)
+        ( \ t → is-equiv-f)
+```
+
+More precicely:
+
+```rzk
+#def fiber-ap-hom
+  ( A B : U)
+  ( x y : A)
+  ( f : A → B)
+  ( β : hom B (f x) (f y))
+  : U
+  :=
+    fib
+      ( hom A x y)
+      ( hom B (f x) (f y))
+      ( ap-hom A B f x y)
+      ( β)
+
+#def is-contr-fiber-ap-hom-is-equiv uses (weakextext extext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  ( x y : A)
+  ( β : hom B (f x) (f y))
+  : is-contr (fiber-ap-hom A B x y f β)
+  :=
+    is-contr-fiber-postcomp-Π-ext-is-equiv-fam 2 Δ¹ ∂Δ¹
+        ( \ t → A)
+        ( \ t → B)
+        ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y))
+        ( \ t → f)
+        ( β)
+        ( \ t → is-equiv-f)
+```
+
+We can also define a retraction of `#!rzk ap-hom` directly.
+
+```rzk
+#def retraction-ap-hom-retraction uses (funext)
+  ( A B : U)
+  ( f : A → B)
+  ( (r, ρ) : has-retraction A B f)
+  ( x y : A)
+  : (hom B (f x) (f y)) → (hom A x y)
+  :=
+    comp
+      ( hom B (f x) (f y))
+      ( hom A (r (f x)) (r (f y)))
+      ( hom A x y)
+      ( transport (A → A) (\ g' → (hom A (g' x) (g' y)))
+        ( comp A B A r f)
+        ( identity A)
+        ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ))
+      ( ap-hom B A r (f x) (f y))
+
+#def has-retraction-ap-hom-retraction uses (funext)
+  ( A B : U)
+  ( f : A → B)
+  ( (r, ρ) : has-retraction A B f)
+  ( x y : A)
+  : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y)
+  :=
+    ( retraction-ap-hom-retraction A B f (r, ρ) x y
+    , \ α →
+      apd (A → A) (\ g' → (hom A (g' x) (g' y)))
+        ( comp A B A r f)
+        ( identity A)
+        ( \ g' → ap-hom A A g' x y α)
+        ( eq-htpy funext A (\ x' → A) (comp A B A r f) (identity A) ρ))
+```