Merge branch 'main' into uniqueness-colimits

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)