Merge branch 'main' into functoriality-extensions

README.md

@@ -17,7 +17,7 @@ results from the following papers:
 - "[Limits and colimits of synthetic ∞-categories](https://arxiv.org/abs/2202.12386)"
   [3]
 
-This formalization project follows the philosophy layed out in the article
+This formalization project follows the philosophy laid out in the article
 "[Could ∞-category theory be taught to undergraduates?](https://www.ams.org/journals/notices/202305/noti2692/noti2692.html)"
 [4].
 

src/hott/07-fibers.rzk.md

@@ -17,6 +17,13 @@ The homotopy fiber of a map is the following type:
   ( b : B)
   : U
   := Σ (a : A) , (f a) = b
+
+#def rev-fib
+  ( A B : U)
+  ( f : A → B)
+  ( b : B)
+  : U
+  := Σ (a : A) , b = (f a)
 ```
 
 We calculate the transport of `#!rzk (a , q) : fib b` along `#!rzk p : a = a'`:
@@ -63,6 +70,17 @@ of the form `#!rzk (a, refl : f a = f a) : fib A B f`.
   :=
     ind-path B (f a) (\ b p → C b (a, p)) (s a) b q
 
+#def ind-rev-fib
+  ( A B : U)
+  ( f : A → B)
+  ( C : (b : B) → rev-fib A B f b → U)
+  ( s : (a : A) → C (f a) (a, refl))
+  ( b : B)
+  ( (a, q) : rev-fib A B f b)
+  : C b (a, q)
+  :=
+    ind-path-end B (f a) (\ b p → C b (a, p)) (s a) b q
+
 #def ind-fib-computation
   ( A B : U)
   ( f : A → B)

src/hott/10-trivial-fibrations.rzk.md

@@ -268,6 +268,27 @@ the fibers.
     ( fubini-Σ A B (\ a b → f a = b))
 ```
 
+The inverse of this equivalence is given (definitionally!) by the projection
+`\ (_ , (a , _)) → a`.
+
+```rzk
+#def compute-left-inverse-equiv-domain-sum-of-fibers
+  ( A B : U)
+  ( f : A → B)
+  ( (b , (a , p)) : (Σ (b : B) , fib A B f b))
+  : ( first (first ( second (equiv-domain-sum-of-fibers A B f))) (b , (a , p))
+    = a)
+  := refl
+
+#def compute-right-inverse-equiv-domain-sum-of-fibers
+  ( A B : U)
+  ( f : A → B)
+  ( (b , (a , p)) : (Σ (b : B) , fib A B f b))
+  : ( first (second ( second (equiv-domain-sum-of-fibers A B f))) (b , (a , p))
+    = a)
+  := refl
+```
+
 ## Equivalence between fibers in equivalent domains
 
 As an application of the main theorem, we show that precomposing with an

src/hott/11-homotopy-pullbacks.rzk.md

@@ -638,3 +638,112 @@ The relative product of `f : B → A` with a map `Unit → A` corresponding to
       , is-equiv-identity Unit))
 
 ```
+
+## Applications
+
+### Maps induced on fibers
+
+As an application of `#!rzk is-homotopy-cartesian-is-horizontal-equiv`, we show
+that an equivalence of maps induces an equivalence of fibers at each base point.
+
+```rzk
+#section is-equiv-map-of-fibers-is-equiv-map-of-maps
+#variables A' A : U
+#variable α : A' → A
+#variables B' B : U
+#variable β : B' → B
+#variable map-of-maps-α-β : map-of-maps A' A α B' B β
+
+-- To avoid polluting the global namespace, we add a random suffix to
+-- identifiers that are only supposed to be used in this section.
+#def s'-c4XT uses (A α B β) : A' → B' := first (first map-of-maps-α-β)
+#def s-c4XT uses (A' α B' β) : A → B := second (first map-of-maps-α-β)
+
+#def map-of-fibers-map-of-maps
+  ( a : A)
+  ( (a', p) : fib A' A α a)
+  : fib B' B β (s-c4XT a)
+  :=
+  ( s'-c4XT a'
+  , ( concat B (β (s'-c4XT a')) (s-c4XT (α a')) (s-c4XT a))
+    ( second  map-of-maps-α-β a')
+    ( ap A B (α a') a s-c4XT p))
+
+#def map-of-sums-of-fibers-map-of-maps uses (map-of-maps-α-β)
+  ( (a, u) : Σ (a : A), fib A' A α a)
+  : Σ (b : B), fib B' B β b
+  := (s-c4XT a, map-of-fibers-map-of-maps a u)
+
+#def sums-of-fibers-to-domains-map-of-maps uses (map-of-maps-α-β)
+  : map-of-maps
+    ( Σ (a : A), fib A' A α a)
+    ( Σ (b : B), fib B' B β b)
+    ( map-of-sums-of-fibers-map-of-maps)
+    ( A')
+    ( B')
+    ( s'-c4XT)
+  :=
+  ((( \ (_, (a', _)) → a'), ( \ (_, (b', _)) → b')), \ (a, u) → refl)
+
+#variable is-equiv-s' : is-equiv A' B' s'-c4XT
+
+#def is-equiv-map-of-sums-of-fibers-is-equiv-map-of-domains
+  uses (map-of-maps-α-β is-equiv-s')
+  : is-equiv
+    ( Σ (a : A), fib A' A α a)
+    ( Σ (b : B), fib B' B β b)
+    ( map-of-sums-of-fibers-map-of-maps)
+  :=
+  is-equiv-equiv-is-equiv
+  ( Σ (a : A), fib A' A α a)
+  ( Σ (b : B), fib B' B β b)
+  ( map-of-sums-of-fibers-map-of-maps)
+  ( A')
+  ( B')
+  ( s'-c4XT)
+  ( sums-of-fibers-to-domains-map-of-maps)
+  ( second
+    ( ( inv-equiv A' (Σ (a : A), fib A' A α a))
+      ( equiv-domain-sum-of-fibers A' A α)))
+  ( second
+    ( ( inv-equiv B' (Σ (b : B), fib B' B β b))
+      ( equiv-domain-sum-of-fibers B' B β)))
+  ( is-equiv-s')
+
+#variable is-equiv-s : is-equiv A B s-c4XT
+
+#def is-equiv-map-of-fibers-is-equiv-map-of-maps
+  uses (map-of-maps-α-β  is-equiv-s is-equiv-s')
+  : (a : A)
+  → is-equiv
+    ( fib A' A α a)
+    ( fib B' B β (s-c4XT a))
+    ( map-of-fibers-map-of-maps a)
+  :=
+  is-homotopy-cartesian-is-horizontal-equiv
+  ( A)
+  ( fib A' A α)
+  ( B)
+  ( fib B' B β)
+  ( s-c4XT)
+  ( map-of-fibers-map-of-maps)
+  ( is-equiv-s)
+  ( is-equiv-map-of-sums-of-fibers-is-equiv-map-of-domains)
+
+#end is-equiv-map-of-fibers-is-equiv-map-of-maps
+
+#def Equiv-of-fibers-Equiv-of-maps
+  ( A' A : U)
+  ( α : A' → A)
+  ( B' B : U)
+  ( β : B' → B)
+  ( (((s', s), η), (is-equiv-s, is-equiv-s')) : Equiv-of-maps A' A α B' B β)
+  (a : A)
+  : Equiv (fib A' A α a) (fib B' B β (s a))
+  :=
+  ( map-of-fibers-map-of-maps A' A α B' B β ((s', s), η) a
+  , ( is-equiv-map-of-fibers-is-equiv-map-of-maps A' A α B' B β ((s', s), η))
+    ( is-equiv-s)
+    ( is-equiv-s')
+    ( a))
+```

src/index.md

@@ -15,7 +15,7 @@ results from the following papers:
 - "[Limits and colimits of synthetic ∞-categories](https://arxiv.org/abs/2202.12386)"
   [^3]
 
-This formalization project follows the philosophy layed out in the article
+This formalization project follows the philosophy laid out in the article
 "[Could ∞-category theory be taught to undergraduates?](https://www.ams.org/journals/notices/202305/noti2692/noti2692.html)"
 [^4].