From 2ef641fd279fb6782ed233b75d1357633bbdb2c8 Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Fri, 6 Oct 2023 15:18:02 -0400
Subject: [PATCH 01/20] yoneda embedding

---
 src/simplicial-hott/09-yoneda.rzk.md | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 605065f3..3e97a779 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -400,6 +400,24 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
         is-natural-in-family-yon-once-pointwise
           A is-segal-A a C D is-covariant-C is-covariant-D ψ u x)
 ```
+We prove the Yoneda embedding.
+
+```rzk tittle="Yoneda embedding "
+#def yoneda-embedding
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  :  hom A a' a → ( (z : A) → hom A a z → hom A a' z)
+  := yon
+      ( A )
+      ( is-segal-A)
+      ( a )
+      ( \ x → hom A a' x )
+      ( is-covariant-representable-is-segal
+          ( A)
+          ( is-segal-A)
+          ( a'))
+```
 
 ## Yoneda for contravariant families
 

From c6b07d84683acdd09fccb243a6fc8b78a47d4837 Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Mon, 9 Oct 2023 11:03:36 -0400
Subject: [PATCH 02/20] Yoneda embedding 9.3 and Remark 9.4

---
 src/simplicial-hott/09-yoneda.rzk.md | 71 ++++++++++++++++++++++++----
 1 file changed, 63 insertions(+), 8 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 3e97a779..729c797c 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -402,21 +402,76 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
 ```
 We prove the Yoneda embedding.
 
-```rzk tittle="Yoneda embedding "
+```rzk tittle="Yoneda embedding, Definition 9.3 RS17 "
 #def yoneda-embedding
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
   :  hom A a' a → ( (z : A) → hom A a z → hom A a' z)
-  := yon
-      ( A )
+  :=
+     yon
+     ( A )
+     ( is-segal-A)
+     ( a )
+     ( \ x → hom A a' x )
+     ( is-covariant-representable-is-segal
+        ( A)
+        ( is-segal-A)
+        ( a'))
+```
+```rzk
+#def yoneda-comp uses (funext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  : ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ)) = φ
+  :=
+     yon-evid
+      ( A)
       ( is-segal-A)
-      ( a )
-      ( \ x → hom A a' x )
+      ( a)
+      ( hom A a')
       ( is-covariant-representable-is-segal
-          ( A)
-          ( is-segal-A)
-          ( a'))
+        ( A)
+        ( is-segal-A)
+        ( a')) φ
+```
+```rzk
+#def is-composition
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  : ( x : A ) → ( hom A a x → hom A a' x)
+  := \ x f → comp-is-segal
+              ( A)
+              ( is-segal-A)
+              ( a')
+              ( a)
+              ( x)
+              ( ( evid A a ( hom A a')) φ)
+              ( f )
+```
+```rzk title="Remark 9.4, RS17"
+#def eq-yoneda-embedding-is-composition
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( x : A)
+  ( f : hom A a x)
+  : ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ))  x f =
+      is-composition A is-segal-A a a' φ x f
+  :=
+     compute-covariant-transport-of-hom-family-is-segal
+      ( A)
+      ( is-segal-A)
+      ( a')
+      ( a)
+      ( x)
+      ( (evid A a ( hom A a')) φ)
+      ( f )
 ```
 
 ## Yoneda for contravariant families

From b69fb58b266f8375884b379c419bfdeae15e6ffa Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Mon, 9 Oct 2023 18:00:21 -0400
Subject: [PATCH 03/20] Proof of Remark 9.4 as in RS17

---
 src/simplicial-hott/09-yoneda.rzk.md | 121 ++++++++++++++++++++++-----
 1 file changed, 102 insertions(+), 19 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 729c797c..72a18f32 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -414,13 +414,10 @@ We prove the Yoneda embedding.
      ( is-segal-A)
      ( a )
      ( \ x → hom A a' x )
-     ( is-covariant-representable-is-segal
-        ( A)
-        ( is-segal-A)
-        ( a'))
+     ( is-covariant-representable-is-segal A is-segal-A a')
 ```
 ```rzk
-#def yoneda-comp uses (funext)
+#def yoneda-phi uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
@@ -432,11 +429,52 @@ We prove the Yoneda embedding.
       ( is-segal-A)
       ( a)
       ( hom A a')
-      ( is-covariant-representable-is-segal
-        ( A)
-        ( is-segal-A)
-        ( a')) φ
+      ( is-covariant-representable-is-segal A is-segal-A a') φ
+
+#def htpy-yoneda-phi uses (funext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  : (x : A) → ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x = φ x
+  := htpy-eq
+    ( A )
+    ( \ x → ( hom A a x → hom A a' x) )
+    ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ ))
+    ( φ)
+    ( yoneda-phi A is-segal-A a a' φ )
+
+#def htpy-eq-yoneda-phi uses (funext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( x : A)
+  : ( f : hom A a x) → ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f = φ x f
+  := htpy-eq
+      ( hom A a x)
+      ( \ z → hom A a' x)
+      ( ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x)
+      ( φ x)
+      ( htpy-yoneda-phi A is-segal-A a a' φ x)
+
+#def eq-eq-phi-yoneda uses (funext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( x : A)
+  ( f : hom A a x)
+  : φ x f = ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f
+  :=
+     rev
+      ( hom A a' x)
+      ( ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f)
+      ( φ x f)
+      ( htpy-eq-yoneda-phi A is-segal-A a a' φ x f)
 ```
+Define the action by compostition
+
 ```rzk
 #def is-composition
   ( A : U)
@@ -444,17 +482,12 @@ We prove the Yoneda embedding.
   ( a a' : A)
   ( φ : ( x : A) → ( hom A a x → hom A a' x) )
   : ( x : A ) → ( hom A a x → hom A a' x)
-  := \ x f → comp-is-segal
-              ( A)
-              ( is-segal-A)
-              ( a')
-              ( a)
-              ( x)
-              ( ( evid A a ( hom A a')) φ)
-              ( f )
+  := \ x f → comp-is-segal A is-segal-A a' a x ( ( evid A a ( hom A a')) φ) f
 ```
-```rzk title="Remark 9.4, RS17"
-#def eq-yoneda-embedding-is-composition
+The Yoneda embedding coincides with ```#!rzk is-composition``` up to homotopy.
+
+```rzk
+#def eq-eq-yoneda-embedding-composition
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
@@ -473,6 +506,56 @@ We prove the Yoneda embedding.
       ( (evid A a ( hom A a')) φ)
       ( f )
 ```
+Now we glue the equalities to prove the result as stated in [RS17, Remark 9.4].
+
+```rzk
+#def eq-eq-phi-composition uses (funext)
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( x : A)
+  ( f : hom A a x)
+  : (φ x) f = (is-composition A is-segal-A a a' φ x) f
+  :=
+     concat
+      ( hom A a' x)
+      ( φ x f)
+      ( ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f)
+      ( is-composition A is-segal-A a a' φ x f)
+      ( eq-eq-phi-yoneda A is-segal-A a a' φ x f)
+      ( eq-eq-yoneda-embedding-composition A is-segal-A a a' φ x f )
+
+#def eq-htpy-phi-composition
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( x : A)
+  : φ x = is-composition A is-segal-A a a' φ x
+  :=
+      eq-htpy
+        ( funext)
+        ( hom A a x)
+        ( \ z → hom A a' x)
+        ( φ x)
+        ( is-composition A is-segal-A a a' φ x)
+        ( \ f → eq-eq-phi-composition A is-segal-A a a' φ x f)
+
+#def htpy-htpy-phi-composition
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  : φ = is-composition A is-segal-A a a' φ
+  := eq-htpy
+      ( funext)
+      ( A)
+      ( \ x → ( hom A a x → hom A a' x))
+      ( φ)
+      ( is-composition A is-segal-A a a' φ)
+      ( \ x → eq-htpy-phi-composition A is-segal-A a a' φ x )
+```
 
 ## Yoneda for contravariant families
 

From fd37ea86520a4e5e2bff63b9b027fae017f9e966 Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Mon, 9 Oct 2023 21:11:56 -0400
Subject: [PATCH 04/20] Changed titles and finish the proof

---
 src/simplicial-hott/09-yoneda.rzk.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 72a18f32..6c8fe4f3 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -400,7 +400,7 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
         is-natural-in-family-yon-once-pointwise
           A is-segal-A a C D is-covariant-C is-covariant-D ψ u x)
 ```
-We prove the Yoneda embedding.
+##  Yoneda embedding.
 
 ```rzk tittle="Yoneda embedding, Definition 9.3 RS17 "
 #def yoneda-embedding
@@ -484,7 +484,7 @@ Define the action by compostition
   : ( x : A ) → ( hom A a x → hom A a' x)
   := \ x f → comp-is-segal A is-segal-A a' a x ( ( evid A a ( hom A a')) φ) f
 ```
-The Yoneda embedding coincides with ```#!rzk is-composition``` up to homotopy.
+The Yoneda embedding coincides with ```#!rzk is-composition```.
 
 ```rzk
 #def eq-eq-yoneda-embedding-composition
@@ -506,7 +506,7 @@ The Yoneda embedding coincides with ```#!rzk is-composition``` up to homotopy.
       ( (evid A a ( hom A a')) φ)
       ( f )
 ```
-Now we glue the equalities to prove the result as stated in [RS17, Remark 9.4].
+Now we cocatenate the paths to prove the result as stated in [RS17, Remark 9.4].
 
 ```rzk
 #def eq-eq-phi-composition uses (funext)

From d359521969fbda87223cc9a09d3950c17acba7f3 Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Thu, 12 Oct 2023 12:36:36 -0400
Subject: [PATCH 05/20] Changes and parenthesis

---
 src/simplicial-hott/09-yoneda.rzk.md | 76 ++++++++++++++--------------
 1 file changed, 38 insertions(+), 38 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 4e9fe770..ac5ed324 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -402,7 +402,7 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
 ```
 ##  Yoneda embedding.
 
-```rzk tittle="Yoneda embedding, Definition 9.3 RS17 "
+```rzk title="Yoneda embedding, Definition 9.3 RS17 "
 #def yoneda-embedding
   ( A : U)
   ( is-segal-A : is-segal A)
@@ -410,19 +410,18 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
   :  hom A a' a → ( (z : A) → hom A a z → hom A a' z)
   :=
      yon
-     ( A )
+     ( A)
      ( is-segal-A)
-     ( a )
-     ( \ x → hom A a' x )
+     ( a)
+     ( hom A a')
      ( is-covariant-representable-is-segal A is-segal-A a')
-```
-```rzk
+
 #def yoneda-phi uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
-  : ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ)) = φ
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
+  : ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ) = φ
   :=
      yon-evid
       ( A)
@@ -435,26 +434,27 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
-  : (x : A) → ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x = φ x
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
+  : (x : A)
+    → ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x = φ x
   := htpy-eq
-    ( A )
-    ( \ x → ( hom A a x → hom A a' x) )
-    ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ ))
+    ( A)
+    ( \ x → ( hom A a x → hom A a' x))
+    ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ ))
     ( φ)
-    ( yoneda-phi A is-segal-A a a' φ )
+    ( yoneda-phi A is-segal-A a a' φ)
 
 #def htpy-eq-yoneda-phi uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
   ( x : A)
-  : ( f : hom A a x) → ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f = φ x f
+  : ( f : hom A a x) → ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x f = φ x f
   := htpy-eq
       ( hom A a x)
       ( \ z → hom A a' x)
-      ( ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x)
+      ( ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x)
       ( φ x)
       ( htpy-yoneda-phi A is-segal-A a a' φ x)
 
@@ -462,25 +462,25 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
   ( x : A)
   ( f : hom A a x)
-  : φ x f = ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f
+  : φ x f = ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x f
   :=
      rev
       ( hom A a' x)
-      ( ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f)
+      ( ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x f)
       ( φ x f)
       ( htpy-eq-yoneda-phi A is-segal-A a a' φ x f)
 ```
-Define the action by compostition
+Define the action by compostition.
 
 ```rzk
-#def is-composition
+#def precomposition-evid-is-segal
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
   : ( x : A ) → ( hom A a x → hom A a' x)
   := \ x f → comp-is-segal A is-segal-A a' a x ( ( evid A a ( hom A a')) φ) f
 ```
@@ -491,11 +491,11 @@ The Yoneda embedding coincides with ```#!rzk is-composition```.
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
   ( x : A)
   ( f : hom A a x)
-  : ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ))  x f =
-      is-composition A is-segal-A a a' φ x f
+  : ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x f
+    = precomposition-evid-is-segal A is-segal-A a a' φ x f
   :=
      compute-covariant-transport-of-hom-family-is-segal
       ( A)
@@ -513,48 +513,48 @@ Now we cocatenate the paths to prove the result as stated in [RS17, Remark 9.4].
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
   ( x : A)
   ( f : hom A a x)
-  : (φ x) f = (is-composition A is-segal-A a a' φ x) f
+  : (φ x) f = (precomposition-evid-is-segal A is-segal-A a a' φ x) f
   :=
      concat
       ( hom A a' x)
       ( φ x f)
-      ( ( ( yoneda-embedding A is-segal-A a a' ) ( ( evid A a ( hom A a')) φ )) x f)
-      ( is-composition A is-segal-A a a' φ x f)
+      ( ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x f)
+      ( precomposition-evid-is-segal A is-segal-A a a' φ x f)
       ( eq-eq-phi-yoneda A is-segal-A a a' φ x f)
-      ( eq-eq-yoneda-embedding-composition A is-segal-A a a' φ x f )
+      ( eq-eq-yoneda-embedding-composition A is-segal-A a a' φ x f)
 
 #def eq-htpy-phi-composition
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
   ( x : A)
-  : φ x = is-composition A is-segal-A a a' φ x
+  : φ x = precomposition-evid-is-segal A is-segal-A a a' φ x
   :=
       eq-htpy
         ( funext)
         ( hom A a x)
         ( \ z → hom A a' x)
         ( φ x)
-        ( is-composition A is-segal-A a a' φ x)
+        ( precomposition-evid-is-segal A is-segal-A a a' φ x)
         ( \ f → eq-eq-phi-composition A is-segal-A a a' φ x f)
 
 #def htpy-htpy-phi-composition
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  ( φ : ( x : A) → ( hom A a x → hom A a' x) )
-  : φ = is-composition A is-segal-A a a' φ
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
+  : φ = precomposition-evid-is-segal A is-segal-A a a' φ
   := eq-htpy
       ( funext)
       ( A)
       ( \ x → ( hom A a x → hom A a' x))
       ( φ)
-      ( is-composition A is-segal-A a a' φ)
-      ( \ x → eq-htpy-phi-composition A is-segal-A a a' φ x )
+      ( precomposition-evid-is-segal A is-segal-A a a' φ)
+      ( \ x → eq-htpy-phi-composition A is-segal-A a a' φ x)
 ```
 
 ## Yoneda for contravariant families

From 7782aa77239475ca5511e0ecd60be40fe80785cf Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Fri, 13 Oct 2023 16:47:35 -0400
Subject: [PATCH 06/20] fix names, parenthesis and spaces

---
 src/simplicial-hott/09-yoneda.rzk.md | 93 ++++++++++++++++------------
 1 file changed, 53 insertions(+), 40 deletions(-)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index ac5ed324..396a00b3 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -400,14 +400,15 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
         is-natural-in-family-yon-once-pointwise
           A is-segal-A a C D is-covariant-C is-covariant-D ψ u x)
 ```
-##  Yoneda embedding.
 
-```rzk title="Yoneda embedding, Definition 9.3 RS17 "
+## Yoneda embedding.
+
+```rzk title="Yoneda embedding. RS17, Definition 9.3"
 #def yoneda-embedding
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
-  :  hom A a' a → ( (z : A) → hom A a z → hom A a' z)
+  :  hom A a' a → (z : A) → hom A a z → hom A a' z
   :=
      yon
      ( A)
@@ -416,7 +417,7 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
      ( hom A a')
      ( is-covariant-representable-is-segal A is-segal-A a')
 
-#def yoneda-phi uses (funext)
+#def compute-yoneda-embedding-evid uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
@@ -430,50 +431,59 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
       ( hom A a')
       ( is-covariant-representable-is-segal A is-segal-A a') φ
 
-#def htpy-yoneda-phi uses (funext)
+#def htpy-compute-yoneda-embedding-evid uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
   ( φ : ( x : A) → ( hom A a x → hom A a' x))
   : (x : A)
-    → ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x = φ x
-  := htpy-eq
-    ( A)
-    ( \ x → ( hom A a x → hom A a' x))
-    ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ ))
-    ( φ)
-    ( yoneda-phi A is-segal-A a a' φ)
+    → ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x
+    = φ x
+  :=
+     htpy-eq
+      ( A)
+      ( \ x → ( hom A a x → hom A a' x))
+      ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ ))
+      ( φ)
+      ( compute-yoneda-embedding-evid A is-segal-A a a' φ)
 
-#def htpy-eq-yoneda-phi uses (funext)
+#def htpy-yoneda-embedding-evid uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
   ( φ : ( x : A) → ( hom A a x → hom A a' x))
   ( x : A)
-  : ( f : hom A a x) → ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x f = φ x f
-  := htpy-eq
+  : ( f : hom A a x)
+    → ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x f
+    = φ x f
+  :=
+     htpy-eq
       ( hom A a x)
       ( \ z → hom A a' x)
-      ( ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x)
+      ( ( ( yoneda-embedding A is-segal-A a a')
+          ( ( evid A a ( hom A a')) φ )) x)
       ( φ x)
-      ( htpy-yoneda-phi A is-segal-A a a' φ x)
+      ( htpy-compute-yoneda-embedding-evid A is-segal-A a a' φ x)
 
-#def eq-eq-phi-yoneda uses (funext)
+#def rev-compute-htpy-yoneda-embedding-evid uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
   ( φ : ( x : A) → ( hom A a x → hom A a' x))
   ( x : A)
   ( f : hom A a x)
-  : φ x f = ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x f
+  : φ x f
+    = ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ)) x f
   :=
      rev
       ( hom A a' x)
-      ( ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x f)
+      ( ( ( yoneda-embedding A is-segal-A a a')
+          ( ( evid A a ( hom A a')) φ )) x f)
       ( φ x f)
-      ( htpy-eq-yoneda-phi A is-segal-A a a' φ x f)
+      ( htpy-yoneda-embedding-evid A is-segal-A a a' φ x f)
 ```
-Define the action by compostition.
+
+Define the action by precompostition.
 
 ```rzk
 #def precomposition-evid-is-segal
@@ -484,10 +494,10 @@ Define the action by compostition.
   : ( x : A ) → ( hom A a x → hom A a' x)
   := \ x f → comp-is-segal A is-segal-A a' a x ( ( evid A a ( hom A a')) φ) f
 ```
-The Yoneda embedding coincides with ```#!rzk is-composition```.
+The Yoneda embedding coincides with `#!rzk precomposition-evid-is-segal`.
 
 ```rzk
-#def eq-eq-yoneda-embedding-composition
+#def eq-yoneda-embedding-precomposition-evid
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
@@ -506,10 +516,11 @@ The Yoneda embedding coincides with ```#!rzk is-composition```.
       ( (evid A a ( hom A a')) φ)
       ( f )
 ```
-Now we cocatenate the paths to prove the result as stated in [RS17, Remark 9.4].
+
+Now we cocatenate the paths to prove the result as stated.
 
 ```rzk
-#def eq-eq-phi-composition uses (funext)
+#def eq-compute-precomposition-evid uses (funext)
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
@@ -521,12 +532,13 @@ Now we cocatenate the paths to prove the result as stated in [RS17, Remark 9.4].
      concat
       ( hom A a' x)
       ( φ x f)
-      ( ( ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ )) x f)
+      ( ( ( yoneda-embedding A is-segal-A a a')
+          ( ( evid A a ( hom A a')) φ )) x f)
       ( precomposition-evid-is-segal A is-segal-A a a' φ x f)
-      ( eq-eq-phi-yoneda A is-segal-A a a' φ x f)
-      ( eq-eq-yoneda-embedding-composition A is-segal-A a a' φ x f)
+      ( rev-compute-htpy-yoneda-embedding-evid A is-segal-A a a' φ x f)
+      ( eq-yoneda-embedding-precomposition-evid A is-segal-A a a' φ x f)
 
-#def eq-htpy-phi-composition
+#def eq-htpy-precomposition-evid
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
@@ -534,27 +546,28 @@ Now we cocatenate the paths to prove the result as stated in [RS17, Remark 9.4].
   ( x : A)
   : φ x = precomposition-evid-is-segal A is-segal-A a a' φ x
   :=
-      eq-htpy
-        ( funext)
-        ( hom A a x)
-        ( \ z → hom A a' x)
-        ( φ x)
-        ( precomposition-evid-is-segal A is-segal-A a a' φ x)
-        ( \ f → eq-eq-phi-composition A is-segal-A a a' φ x f)
+     eq-htpy
+      ( funext)
+      ( hom A a x)
+      ( \ z → hom A a' x)
+      ( φ x)
+      ( precomposition-evid-is-segal A is-segal-A a a' φ x)
+      ( \ f → eq-compute-precomposition-evid A is-segal-A a a' φ x f)
 
-#def htpy-htpy-phi-composition
+#def eq-precomposition-evid-is-segal
   ( A : U)
   ( is-segal-A : is-segal A)
   ( a a' : A)
   ( φ : ( x : A) → ( hom A a x → hom A a' x))
   : φ = precomposition-evid-is-segal A is-segal-A a a' φ
-  := eq-htpy
+  :=
+     eq-htpy
       ( funext)
       ( A)
       ( \ x → ( hom A a x → hom A a' x))
       ( φ)
       ( precomposition-evid-is-segal A is-segal-A a a' φ)
-      ( \ x → eq-htpy-phi-composition A is-segal-A a a' φ x)
+      ( \ x → eq-htpy-precomposition-evid A is-segal-A a a' φ x)
 ```
 
 ## Yoneda for contravariant families

From 293d568af39b59df9c682321300fdafdafcf13f2 Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Fri, 13 Oct 2023 17:04:38 -0400
Subject: [PATCH 07/20] Formating

---
 src/simplicial-hott/09-yoneda.rzk.md | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 396a00b3..f0d6c927 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -494,6 +494,7 @@ Define the action by precompostition.
   : ( x : A ) → ( hom A a x → hom A a' x)
   := \ x f → comp-is-segal A is-segal-A a' a x ( ( evid A a ( hom A a')) φ) f
 ```
+
 The Yoneda embedding coincides with `#!rzk precomposition-evid-is-segal`.
 
 ```rzk

From 687e219819b8860f0946d354270850fc7e3134fc Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 19:42:51 +0200
Subject: [PATCH 08/20] formatting and functorial instances

---
 src/hott/07-fibers.rzk.md                     |  18 +
 src/simplicial-hott/03-extension-types.rzk.md | 705 +++++++++---------
 src/simplicial-hott/05-segal-types.rzk.md     |   2 +-
 .../06-2cat-of-segal-types.rzk.md             |   2 +-
 4 files changed, 387 insertions(+), 340 deletions(-)

diff --git a/src/hott/07-fibers.rzk.md b/src/hott/07-fibers.rzk.md
index c868a218..99ec1c40 100644
--- a/src/hott/07-fibers.rzk.md
+++ b/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)
diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index b96a608a..03814870 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -34,8 +34,7 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
 #def extension-type
   ( σ : (t : ϕ) → A t)
   : U
-  :=
-    ( t : ψ) → A t [ϕ t ↦ σ t]
+  := ( t : ψ) → A t [ϕ t ↦ σ t]
 
 #def homotopy-extension-type
   ( σ : (t : ϕ) → A t)
@@ -45,8 +44,7 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
 #def extension-type-weakening-map
   ( σ : (t : ϕ) → A t)
   : extension-type σ → homotopy-extension-type σ
-  :=
-    \ τ → ( τ, refl)
+  := \ τ → ( τ, refl)
 
 #def section-extension-type-weakening'
   : ( σ : (t : ϕ) → A t)
@@ -101,24 +99,24 @@ This equivalence is functorial in the following sense:
   ( α : (t : ψ) → A' t → A t)
   ( σ' : (t : ϕ) → A' t)
   : Equiv-of-maps
-      ( extension-type I ψ ϕ A' σ')
-      ( extension-type I ψ ϕ A (\ t → α t (σ' t)))
-      ( \ τ' t → α t (τ' t))
-      ( homotopy-extension-type I ψ ϕ A' σ')
-      ( homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t)))
-      ( \ (τ', p) →
-          ( \ t → α t (τ' t),
-            ap ((t : ϕ) → A' t) ((t : ϕ) → A t)
-               ( \ (t : ϕ) → τ' t)
-               ( \ (t : ϕ) → σ' t)
-               ( \ σ'' t → α t (σ'' t))
-               ( p)))
+    ( extension-type I ψ ϕ A' σ')
+    ( extension-type I ψ ϕ A (\ t → α t (σ' t)))
+    ( \ τ' t → α t (τ' t))
+    ( homotopy-extension-type I ψ ϕ A' σ')
+    ( homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t)))
+    ( \ (τ', p) →
+      ( \ t → α t (τ' t)
+      , ap
+        ( (t : ϕ) → A' t)
+        ( (t : ϕ) → A t)
+        ( \ (t : ϕ) → τ' t)
+        ( \ (t : ϕ) → σ' t)
+        ( \ σ'' t → α t (σ'' t))
+        ( p)))
   :=
     ( ( ( extension-type-weakening-map I ψ ϕ A' σ'
-        , extension-type-weakening-map I ψ ϕ A (\ t → α t (σ' t))
-        )
-      , \ _ → refl
-      )
+        , extension-type-weakening-map I ψ ϕ A (\ t → α t (σ' t)))
+      , ( \ _ → refl))
     , ( is-equiv-extension-type-weakening I ψ ϕ A' σ'
       , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t))))
 ```
@@ -137,11 +135,9 @@ This equivalence is functorial in the following sense:
       ( (t : ψ) → ((x : X) → Y t x) [ϕ t ↦ f t])
       ( (x : X) → (t : ψ) → Y t x [ϕ t ↦ f t x])
   :=
-    ( \ g x t → g t x ,
-      ( ( \ h t x → (h x) t ,
-          \ g → refl) ,
-        ( \ h t x → (h x) t ,
-          \ h → refl)))
+    ( ( \ g x t → g t x)
+    , ( ( \ h t x → (h x) t , \ g → refl)
+      , ( \ h t x → (h x) t , \ h → refl)))
 
 #def flip-ext-fun-inv
   ( I : CUBE)
@@ -154,11 +150,9 @@ This equivalence is functorial in the following sense:
     ( (x : X) → (t : ψ) → Y t x [ϕ t ↦ f t x])
     ( (t : ψ) → ((x : X) → Y t x) [ϕ t ↦ f t])
   :=
-    ( \ h t x → (h x) t ,
-      ( ( \ g x t → g t x ,
-          \ h → refl) ,
-        ( \ g x t → g t x ,
-          \ g → refl)))
+    ( ( \ h t x → (h x) t)
+    , ( ( \ g x t → g t x , \ h → refl)
+      , ( \ g x t → g t x , \ g → refl)))
 ```
 
 ```rzk title="RS17, Theorem 4.2"
@@ -171,16 +165,15 @@ This equivalence is functorial in the following sense:
   ( X : ψ → ζ → U)
   ( f : ((t , s) : I × J | (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s)) → X t s)
   : Equiv
-    ( (t : ψ) →
-      ( (s : ζ) → X t s [χ s ↦ f (t , s)]) [ϕ t ↦ \ s → f (t , s)])
-    ( ((t , s) : I × J | ψ t ∧ ζ s) →
-      X t s [(ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ f (t , s)])
+    ( ( t : ψ)
+    → ( (s : ζ) → X t s [χ s ↦ f (t , s)])
+      [ ϕ t ↦ \ s → f (t , s)])
+    ( ( (t , s) : I × J | ψ t ∧ ζ s)
+    → ( X t s [(ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ f (t , s)]))
   :=
-    ( \ g (t , s) → (g t) s ,
-      ( ( \ h t s → h (t , s) ,
-          \ g → refl) ,
-        ( \ h t s → h (t , s) ,
-          \ h → refl)))
+    ( ( \ g (t , s) → (g t) s)
+    , ( ( \ h t s → h (t , s) , \ g → refl)
+      , ( \ h t s → h (t , s) , \ h → refl)))
 
 #def uncurry-opcurry
   ( I J : CUBE)
@@ -191,16 +184,15 @@ This equivalence is functorial in the following sense:
   ( X : ψ → ζ → U)
   ( f : ((t , s) : I × J | (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s)) → X t s)
   : Equiv
-    ( ((t , s) : I × J | ψ t ∧ ζ s) →
-      X t s [(ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ f (t , s)])
-    ( ( s : ζ) →
-      ( (t : ψ) → X t s [ϕ t ↦ f (t , s)]) [χ s ↦ \ t → f (t , s)])
+    ( ( (t , s) : I × J | ψ t ∧ ζ s)
+    → ( X t s [(ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ f (t , s)]))
+    ( ( s : ζ)
+    → ( (t : ψ) → X t s [ϕ t ↦ f (t , s)])
+      [ χ s ↦ \ t → f (t , s)])
   :=
-    ( \ h s t → h (t , s) ,
-      ( ( \ g (t , s) → (g s) t ,
-          \ h → refl) ,
-        ( \ g (t , s) → (g s) t ,
-          \ g → refl)))
+    ( ( \ h s t → h (t , s))
+    , ( ( \ g (t , s) → (g s) t , \ h → refl)
+      , ( \ g (t , s) → (g s) t , \ g → refl)))
 
 #def fubini
   ( I J : CUBE)
@@ -211,22 +203,115 @@ This equivalence is functorial in the following sense:
   ( X : ψ → ζ → U)
   ( f : ((t , s) : I × J | (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s)) → X t s)
   : Equiv
-    ( ( t : ψ) →
-      ( (s : ζ) → X t s [χ s ↦ f (t , s)]) [ϕ t ↦ \ s → f (t , s)])
-    ( ( s : ζ) →
-      ( (t : ψ) → X t s [ϕ t ↦ f (t , s)]) [χ s ↦ \ t → f (t , s)])
+    ( ( t : ψ)
+    → ( (s : ζ) → X t s [χ s ↦ f (t , s)]) [ϕ t ↦ \ s → f (t , s)])
+    ( ( s : ζ)
+    → ( (t : ψ) → X t s [ϕ t ↦ f (t , s)]) [χ s ↦ \ t → f (t , s)])
   :=
     equiv-comp
-      ( ( t : ψ) →
-        ( (s : ζ) → X t s [χ s ↦ f (t , s)]) [ϕ t ↦ \ s → f (t , s)])
-      ( ( (t , s) : I × J | ψ t ∧ ζ s) →
-        X t s [(ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ f (t , s)])
-      ( ( s : ζ) →
-        ( (t : ψ) → X t s [ϕ t ↦ f (t , s)]) [χ s ↦ \ t → f (t , s)])
+      ( ( t : ψ)
+      → ( (s : ζ) → X t s [χ s ↦ f (t , s)]) [ϕ t ↦ \ s → f (t , s)])
+      ( ( (t , s) : I × J | ψ t ∧ ζ s)
+      → X t s [(ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ f (t , s)])
+      ( ( s : ζ)
+      → ( (t : ψ) → X t s [ϕ t ↦ f (t , s)]) [χ s ↦ \ t → f (t , s)])
       ( curry-uncurry I J ψ ϕ ζ χ X f)
       ( uncurry-opcurry I J ψ ϕ ζ χ X f)
 ```
 
+For each of these we provide a corresponding functorial instance
+
+```rzk
+#def curry-uncurry-functorial
+  ( I J : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( ζ : J → TOPE)
+  ( χ : ζ → TOPE)
+  ( A' A : ψ → ζ → U)
+  ( α : (t : ψ) → (s : ζ) → A' t s → A t s)
+  ( σ' : ((t , s) : I × J | (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s)) → A' t s)
+  : Equiv-of-maps
+    ( ( t : ψ)
+    → ( (s : ζ) → A' t s [χ s ↦ σ' (t , s)])
+      [ ϕ t ↦ \ s → σ' (t , s)])
+    ( ( t : ψ)
+    → ( (s : ζ) → A t s [χ s ↦ α t s (σ' (t , s))])
+      [ ϕ t ↦ \ s → α t s (σ' (t , s))])
+    ( \ τ' t s → α t s (τ' t s))
+    ( ( (t , s) : I × J | ψ t ∧ ζ s)
+    → ( A' t s) [ (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ σ' (t , s)])
+    ( ( (t , s) : I × J | ψ t ∧ ζ s)
+    → ( A t s) [ (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ α t s (σ' (t , s))])
+    ( \ uτ' (t , s) → α t s (uτ' (t , s)))
+  :=
+  ( ( ( first (curry-uncurry I J ψ ϕ ζ χ A' σ')
+      , first (curry-uncurry I J ψ ϕ ζ χ A ( \ (t , s) → α t s (σ' (t , s)))))
+    , ( \ _ → refl))
+  , ( second (curry-uncurry I J ψ ϕ ζ χ A' σ')
+    , second (curry-uncurry I J ψ ϕ ζ χ A ( \ (t , s) → α t s (σ' (t , s))))))
+
+#def uncurry-opcurry-functorial
+  ( I J : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( ζ : J → TOPE)
+  ( χ : ζ → TOPE)
+  ( A' A : ψ → ζ → U)
+  ( α : (t : ψ) → (s : ζ) → A' t s → A t s)
+  ( σ' : ((t , s) : I × J | (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s)) → A' t s)
+  : Equiv-of-maps
+    ( ( (t , s) : I × J | ψ t ∧ ζ s)
+    → ( A' t s) [ (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ σ' (t , s)])
+    ( ( (t , s) : I × J | ψ t ∧ ζ s)
+    →  ( A t s) [ (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s) ↦ α t s (σ' (t , s))])
+    ( \ uτ' (t , s) → α t s (uτ' (t , s)))
+    ( ( s : ζ)
+    → ( (t : ψ) → A' t s [ϕ t ↦ σ' (t , s)])
+      [ χ s ↦ \ t → σ' (t , s)])
+    ( ( s : ζ)
+    → ( (t : ψ) → A t s [ϕ t ↦ α t s ( σ' (t , s))])
+      [ χ s ↦ \ t → α t s (σ' (t , s))])
+    ( \ τ' s t → α t s (τ' s t))
+  :=
+  ( ( ( first (uncurry-opcurry I J ψ ϕ ζ χ A' σ')
+      , first (uncurry-opcurry I J ψ ϕ ζ χ A ( \ (t , s) → α t s (σ' (t , s)))))
+    , ( \ _ → refl))
+  , ( second (uncurry-opcurry I J ψ ϕ ζ χ A' σ')
+    , second (uncurry-opcurry I J ψ ϕ ζ χ A ( \ (t , s) → α t s (σ' (t , s))))))
+
+#def fubini-functorial
+  ( I J : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( ζ : J → TOPE)
+  ( χ : ζ → TOPE)
+  ( A' A : ψ → ζ → U)
+  ( α : (t : ψ) → (s : ζ) → A' t s → A t s)
+  ( σ' : ((t , s) : I × J | (ϕ t ∧ ζ s) ∨ (ψ t ∧ χ s)) → A' t s)
+  : Equiv-of-maps
+    ( ( t : ψ)
+    → ( (s : ζ) → A' t s [χ s ↦ σ' (t , s)])
+      [ ϕ t ↦ \ s → σ' (t , s)])
+    ( ( t : ψ)
+    → ( (s : ζ) → A t s [χ s ↦ α t s (σ' (t , s))])
+      [ ϕ t ↦ \ s → α t s (σ' (t , s))])
+    ( \ τ' t s → α t s (τ' t s))
+    ( ( s : ζ)
+    → ( (t : ψ) → A' t s [ϕ t ↦ σ' (t , s)])
+      [ χ s ↦ \ t → σ' (t , s)])
+    ( ( s : ζ)
+    → ( (t : ψ) → A t s [ϕ t ↦ α t s( σ' (t , s))])
+      [ χ s ↦ \ t → α t s (σ' (t , s))])
+    ( \ τ' s t → α t s (τ' s t))
+  :=
+  ( ( ( first (fubini I J ψ ϕ ζ χ A' σ')
+      , first (fubini I J ψ ϕ ζ χ A ( \ (t , s) → α t s (σ' (t , s)))))
+    , ( \ _ → refl))
+  , ( second (fubini I J ψ ϕ ζ χ A' σ')
+    , second (fubini I J ψ ϕ ζ χ A ( \ (t , s) → α t s (σ' (t , s))))))
+```
+
 ## Extending into Σ-types (the non-axiom of choice)
 
 ```rzk title="RS17, Theorem 4.3"
@@ -240,14 +325,12 @@ This equivalence is functorial in the following sense:
   ( b : (t : ϕ) → Y t (a t))
   : 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]))
+    ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t]))
+      , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t]))
     :=
-      ( \ 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)))
+      ( ( \ 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)))
 ```
 
 ## Composites and unions of cofibrations
@@ -267,9 +350,9 @@ The original form.
     ( Σ ( f : (t : ψ) → X t [ϕ t ↦ a t]) ,
         ( (t : χ) → X t [ψ t ↦ f t]))
   :=
-    ( \ h → (\ t → h t , \ t → h t) ,
-      ( ( \ (_f , g) t → g t , \ h → refl) ,
-        ( ( \ (_f , g) t → g t , \ h → refl))))
+    ( ( \ h → (\ t → h t , \ t → h t))
+    , ( ( \ (_f , g) t → g t , \ h → refl)
+      , ( ( \ (_f , g) t → g t , \ h → refl))))
 
 #def cofibration-composition-functorial
   ( I : CUBE)
@@ -280,21 +363,21 @@ The original form.
   ( α : (t : χ) → A' t → A t)
   ( σ' : (t : ϕ) → A' t)
   : Equiv-of-maps
-     ( (t : χ) → A' t [ϕ t ↦ σ' t])
-     ( (t : χ) → A t [ϕ t ↦ α t (σ' t)])
-     ( \ τ' t → α t (τ' t))
-     ( Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) ,
-        ( (t : χ) → A' t [ψ t ↦ τ' t]))
-     ( Σ ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) ,
-        ( (t : χ) → A t [ψ t ↦ τ t]))
-     ( \ (τ', υ') → ( \ t → α t (τ' t), \t → α t (υ' t)))
+    ( (t : χ) → A' t [ϕ t ↦ σ' t])
+    ( (t : χ) → A t [ϕ t ↦ α t (σ' t)])
+    ( \ τ' t → α t (τ' t))
+    ( Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
+      , ( (t : χ) → A' t [ψ t ↦ τ' t]))
+    ( Σ ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
+      , ( (t : χ) → A t [ψ t ↦ τ t]))
+    ( \ (τ', υ') → ( \ t → α t (τ' t), \t → α t (υ' t)))
   :=
-    ( ( ( \ h → (\ t → h t , \ t → h t) , \ h → (\ t → h t , \ t → h t)),
-        \ _ → refl),
-      ( ( ( \ (_f , g) t → g t , \ h → refl) ,
-          ( ( \ (_f , g) t → g t , \ h → refl))),
-        ( ( \ (_f , g) t → g t , \ h → refl) ,
-          ( ( \ (_f , g) t → g t , \ h → refl)))))
+    ( ( ( \ h → (\ t → h t , \ t → h t) , \ h → (\ t → h t , \ t → h t))
+      , ( \ _ → refl))
+    , ( ( ( \ (_f , g) t → g t , \ h → refl)
+        , ( ( \ (_f , g) t → g t , \ h → refl)))
+      , ( ( \ (_f , g) t → g t , \ h → refl)
+        , ( ( \ (_f , g) t → g t , \ h → refl)))))
 ```
 
 A reformulated version via tope disjunction instead of inclusion (see
@@ -308,12 +391,12 @@ A reformulated version via tope disjunction instead of inclusion (see
   ( a : (t : I | χ t ∧ ψ t ∧ ϕ t) → X t)
   : Equiv
       ( (t : χ) → X t [χ t ∧ ψ t ∧ ϕ t ↦ a t])
-      ( Σ ( f : (t : I | χ t ∧ ψ t) → X t [χ t ∧ ψ t ∧ ϕ t ↦ a t]) ,
-          ( (t : χ) → X t [χ t ∧ ψ t ↦ f t]))
+      ( Σ ( f : (t : I | χ t ∧ ψ t) → X t [χ t ∧ ψ t ∧ ϕ t ↦ a t])
+        , ( (t : χ) → X t [χ t ∧ ψ t ↦ f t]))
   :=
-    ( \ h → (\ t → h t , \ t → h t) ,
-      ( ( \ (_f , g) t → g t , \ h → refl) ,
-        ( \ (_f , g) t → g t , \ h → refl)))
+    ( ( \ h → (\ t → h t , \ t → h t))
+    , ( ( \ (_f , g) t → g t , \ h → refl)
+      , ( \ (_f , g) t → g t , \ h → refl)))
 ```
 
 ```rzk title="RS17, Theorem 4.5"
@@ -326,9 +409,9 @@ A reformulated version via tope disjunction instead of inclusion (see
       ( (t : I | ϕ t ∨ ψ t) → X t [ψ t ↦ a t])
       ( (t : ϕ) → X t [ϕ t ∧ ψ t ↦ a t])
   :=
-    (\ h t → h t ,
-      ( ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl) ,
-        ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl)))
+    ( \ h t → h t
+    , ( ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl)
+      , ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl)))
 
 #def cofibration-union-functorial
   ( I : CUBE)
@@ -344,16 +427,10 @@ A reformulated version via tope disjunction instead of inclusion (see
       ( (t : ϕ) → A t [ϕ t ∧ ψ t ↦ α t (τ' t)])
       ( \ ν' t → α t (ν' t))
   :=
-     ( ( ( \ υ' t → υ' t
-         , \ υ t → υ t
-         )
-       , \ _ → refl
-       )
-     , ( second (cofibration-union I ϕ ψ A' τ')
-       ,
-         second (cofibration-union I ϕ ψ A ( \ t → α t (τ' t)))
-       )
-     )
+     ( ( ( \ υ' t → υ' t , \ υ t → υ t)
+       , ( \ _ → refl))
+     , ( ( second (cofibration-union I ϕ ψ A' τ'))
+       , ( second (cofibration-union I ϕ ψ A ( \ t → α t (τ' t))))))
 ```
 
 ## Extension extensionality
@@ -388,7 +465,7 @@ We refer to another form as an "extension extensionality" axiom.
       ( (t : ψ) → A t [ϕ t ↦ a t])
       ( f)
       ( \ g' p' → (t : ψ) → (f t = g' t) [ϕ t ↦ refl])
-      ( \ t → refl)
+      ( \ _ → refl)
       ( g)
       ( p)
 ```
@@ -397,17 +474,17 @@ We refer to another form as an "extension extensionality" axiom.
 #def ExtExt
   : U
   :=
-    ( I : CUBE) →
-    ( ψ : I → TOPE) →
-    ( ϕ : ψ → TOPE) →
-    ( A : ψ → U) →
-    ( a : (t : ϕ) → A t) →
-    ( f  : (t : ψ) → A t [ϕ t ↦ a t]) →
-    ( g : (t : ψ ) → A t [ϕ t ↦ a t]) →
-    is-equiv
+    ( ( I : CUBE)
+    → ( ψ : I → TOPE)
+    → ( ϕ : ψ → TOPE)
+    → ( A : ψ → U)
+    → ( a : (t : ϕ) → A t)
+    → ( f : (t : ψ) → A t [ϕ t ↦ a t])
+    → ( g : (t : ψ ) → A t [ϕ t ↦ a t])
+    → is-equiv
       ( f = g)
       ( (t : ψ) → (f t = g t) [ϕ t ↦ refl])
-      ( ext-htpy-eq I ψ ϕ A a f g)
+      ( ext-htpy-eq I ψ ϕ A a f g))
 ```
 
 ```rzk title="The equivalence provided by extension extensionality"
@@ -433,7 +510,7 @@ fact, sometimes only this weaker form of the axiom is needed.
 #def NaiveExtExt
   : U
   :=
-    ( I : CUBE)
+  ( ( I : CUBE)
   → ( ψ : I → TOPE)
   → ( ϕ : ψ → TOPE)
   → ( A : ψ → U)
@@ -441,14 +518,12 @@ fact, sometimes only this weaker form of the axiom is needed.
   → ( f : (t : ψ) → A t [ϕ t ↦ a t])
   → ( g : (t : ψ) → A t [ϕ t ↦ a t])
   → ( (t : ψ) → (f t = g t) [ϕ t ↦ refl])
-  → ( f = g)
+  → ( f = g))
 
 #def naiveextext-extext
   ( extext : ExtExt)
   : NaiveExtExt
-  :=
-    \ I ψ ϕ A a f g →
-      ( first (first (extext I ψ ϕ A a f g)))
+  := \ I ψ ϕ A a f g → ( first (first (extext I ψ ϕ A a f g)))
 ```
 
 We show that naive extension extensionality implies weak extension
@@ -541,7 +616,7 @@ extensionality to weak extension extensionality:
   : ExtExt → WeakExtExt
   :=
     comp ExtExt NaiveExtExt WeakExtExt
-    ( weakextext-naiveextext) ( naiveextext-extext)
+    ( weakextext-naiveextext) (naiveextext-extext)
 ```
 
 ### Weak extension extensionality implies extension extensionality
@@ -567,45 +642,38 @@ cases an extension type to a function type.
   := f
 
 #define is-contr-ext-based-paths uses (weakextext f)
-  : is-contr ((t : ψ ) → (Σ (y : A t) ,
-              ((ext-projection-temp) t = y))[ϕ t ↦ (a t , refl)])
+  : is-contr
+    ( ( t : ψ )
+    → ( Σ (y : A t) , ((ext-projection-temp) t = y))
+      [ ϕ t ↦ (a t , refl)])
   :=
-    weakextext
-    ( I )
-    ( ψ )
-    ( ϕ )
+    weakextext I ψ ϕ
     ( \ t → (Σ (y : A t) , ((ext-projection-temp) t = y)))
-    ( \ t →
-      is-contr-based-paths (A t ) ((ext-projection-temp) t))
+    ( \ t → is-contr-based-paths (A t ) ((ext-projection-temp) t))
     ( \ t → (a t , refl) )
 
 #define is-contr-ext-endpoint-based-paths uses (weakextext f)
   : is-contr
-    ( ( t : ψ) →
-      ( Σ (y : A t) , (y = ext-projection-temp t)) [ ϕ t ↦ (a t , refl)])
+    ( ( t : ψ)
+    → ( Σ (y : A t) , (y = ext-projection-temp t))
+      [ ϕ t ↦ (a t , refl)])
   :=
-    weakextext
-    ( I)
-    ( ψ)
-    ( ϕ)
+    weakextext I ψ ϕ
     ( \ t → (Σ (y : A t) , y = ext-projection-temp t))
     ( \ t → is-contr-endpoint-based-paths (A t) (ext-projection-temp t))
     ( \ t → (a t , refl))
 
 #define is-contr-based-paths-ext uses (weakextext)
-  : is-contr (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
-              (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
+  : is-contr
+    ( Σ ( g : (t : ψ ) → A t [ϕ t ↦ a t])
+      , ( (t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
   :=
     is-contr-equiv-is-contr
     ( (t : ψ ) → (Σ (y : A t),
                      ((ext-projection-temp ) t = y)) [ϕ t ↦ (a t , refl)] )
     ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
                 (t : ψ ) → (f t = g t) [ϕ t ↦ refl] )
-    ( axiom-choice
-      ( I )
-      ( ψ )
-      ( ϕ )
-      ( A )
+    ( axiom-choice I ψ ϕ A
       ( \ t y → (ext-projection-temp) t = y)
       ( a )
       ( \t → refl ))
@@ -624,9 +692,9 @@ The map that defines extension extensionality
   ( A : ψ → U)
   ( a : (t : ϕ ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
-  : ((Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)) →
-      Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
-        ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
+  : ( ( Σ ( g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g))
+    → ( Σ ( g : (t : ψ ) → A t [ϕ t ↦ a t])
+      , ( ( t : ψ) → (f t = g t) [ϕ t ↦ refl])))
   :=
     total-map
     ( (t : ψ ) → A t [ϕ t ↦ a t])
@@ -646,18 +714,17 @@ The total bundle version of extension extensionality
   ( A : ψ → U)
   ( a : (t : ϕ ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
-  : is-equiv ((Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)))
-               (Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
-                  ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
-               (extext-weakextext-map I ψ ϕ A a f)
+  : is-equiv
+    ( ( Σ ( g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)))
+    ( Σ ( g : (t : ψ ) → A t [ϕ t ↦ a t])
+      , ( ( t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
+    ( extext-weakextext-map I ψ ϕ A a f)
   :=
     is-equiv-are-contr
-    ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]), (f = g)  )
-    ( Σ (g : (t : ψ ) → A t [ϕ t ↦ a t]) ,
-      ((t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
-    ( is-contr-based-paths
-      ( (t : ψ ) → A t [ϕ t ↦ a t])
-      ( f ))
+    ( Σ ( g : (t : ψ) → A t [ϕ t ↦ a t]), (f = g))
+    ( Σ ( g : (t : ψ) → A t [ϕ t ↦ a t])
+    , ( ( t : ψ ) → (f t = g t) [ϕ t ↦ refl]))
+    ( is-contr-based-paths ((t : ψ) → A t [ϕ t ↦ a t]) (f))
     ( is-contr-based-paths-ext weakextext I ψ ϕ A a f)
     ( extext-weakextext-map I ψ ϕ A a f)
 ```
@@ -675,11 +742,11 @@ extensionality. The following is statement the as proved in RS17.
   ( A : ψ → U)
   ( a : (t : ϕ ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
-  : (g : (t : ψ ) → A t [ϕ t ↦ a t]) →
-      is-equiv
+  : ( ( g : (t : ψ ) → A t [ϕ t ↦ a t])
+    → is-equiv
         ( f = g)
         ( (t : ψ ) → (f t = g t) [ϕ t ↦ refl])
-        ( ext-htpy-eq I ψ ϕ A a f g)
+        ( ext-htpy-eq I ψ ϕ A a f g))
   := total-equiv-family-of-equiv
       ( (t : ψ ) → A t [ϕ t ↦ a t] )
       ( \ g → (f = g) )
@@ -689,7 +756,7 @@ extensionality. The following is statement the as proved in RS17.
 ```
 
 The following is the literal statement of weak extension extensionality implying
-extension extensionality that we get by extraccting the fiberwise equivalence.
+extension extensionality that we get by extracting the fiberwise equivalence.
 
 ```rzk title="RS17 Proposition 4.8(i)"
 #define extext-weakextext
@@ -698,70 +765,37 @@ extension extensionality that we get by extraccting the fiberwise equivalence.
       extext-weakextext' weakextext I ψ ϕ A a f g
 ```
 
-## Applications of extension extensionality
-
-We now assume extension extensionality and derive a few consequences.
-
-```rzk
-#assume extext : ExtExt
-#assume naiveextext : NaiveExtExt
-```
-
-In particular, extension extensionality implies that homotopies give rise to
-identifications. This definition defines `#!rzk eq-ext-htpy` to be the
-retraction to `#!rzk ext-htpy-eq`.
+## Homotopy extension property
 
-```rzk
-#def eq-ext-htpy uses (extext)
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A : ψ → U)
-  ( a : (t : ϕ) → A t)
-  ( f g : (t : ψ) → A t [ϕ t ↦ a t])
-  : ((t : ψ) → (f t = g t) [ϕ t ↦ refl]) → (f = g)
-  := first (first (extext I ψ ϕ A a f g))
-```
-
-### Homotopy extension property
-
-We have a homotopy extension property.
-
-The following code is another instantiation of casting, necessary for some
-arguments below.
+The homotopy extension property has the following signature. We state this
+separately since below we will will show that this follows from extension
+extensionality.
 
 ```rzk
-#define restrict
+#def instance-HtpyExtProperty
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
   ( A : ψ → U)
+  ( b : (t : ψ) → A t)
   ( a : (t : ϕ) → A t)
-  ( f : (t : ψ) → A t [ϕ t ↦ a t])
-  : (t : ψ ) → A t
-  := f
-
-```
-
-The homotopy extension property has the following signature. We state this
-separately since below we will will both show that this follows from extension
-extensionality, but we will also show that extension extensionality follows from
-the homotopy extension property together with extra hypotheses.
-
-```rzk
-#define HtpyExtProperty
+  ( e : (t : ϕ) → a t = b t)
   : U
   :=
-    ( I : CUBE) →
-    ( ψ : I → TOPE) →
-    ( ϕ : ψ → TOPE) →
-    ( A : ψ → U) →
-    ( b : (t : ψ) → A t) →
-    ( a : (t : ϕ) → A t) →
-    ( e : (t : ϕ) → a t = b t) →
-      Σ (a' : (t : ψ) → A t [ϕ t ↦ a t]) ,
-      ((t : ψ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
+    Σ (a' : (t : ψ) → A t [ϕ t ↦ a t])
+    , ((t : ψ) → (a' t =_{ A t} b t) [ϕ t ↦ e t])
 
+#def HtpyExtProperty
+  : U
+  :=
+    ( ( I : CUBE)
+    → ( ψ : I → TOPE)
+    → ( ϕ : ψ → TOPE)
+    → ( A : ψ → U)
+    → ( b : (t : ψ) → A t)
+    → ( a : (t : ϕ) → A t)
+    → ( e : (t : ϕ) → a t = b t)
+    → ( instance-HtpyExtProperty I ψ ϕ A b a e ))
 ```
 
 If we assume weak extension extensionality, then then homotopy extension
@@ -769,74 +803,61 @@ property follows from a straightforward application of the axiom of choice to
 the point of contraction for weak extension extensionality.
 
 ```rzk title="RS17 Proposition 4.10"
-#define htpy-ext-property-weakextext
+#define htpy-ext-prop-weakextext
   ( weakextext : WeakExtExt)
   : HtpyExtProperty
   :=
-    \ I ψ ϕ A b a e →
+  \ I ψ ϕ A b a e →
     first
-    ( axiom-choice
-      ( I)
-      ( ψ)
-      ( ϕ)
-      ( A)
+    ( axiom-choice I ψ ϕ A
       ( \ t y → y = b t)
       ( a)
       ( e))
     ( first
-      ( weakextext
-        ( I)
-        ( ψ)
-        ( ϕ)
+      ( weakextext I ψ ϕ
         ( \ t → (Σ (y : A t) , y = b t))
-        ( \ t → is-contr-endpoint-based-paths
-                ( A t)
-                ( b t))
+        ( \ t → is-contr-endpoint-based-paths ( A t) ( b t))
         ( \ t → ( a t , e t) )))
-
 ```
 
-```rzk title="RS17 Proposition 4.10"
-#define htpy-ext-prop-weakextext
-  ( weakextext : WeakExtExt)
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A : ψ → U)
-  ( b : (t : ψ) → A t)
-  ( a : (t : ϕ) → A t)
-  ( e : (t : ϕ) → a t = b t)
-  : Σ (a' : (t : ψ) → A t [ϕ t ↦ a t]) ,
-      ((t : ψ) → (restrict I ψ ϕ A a a' t = b t) [ϕ t ↦ e t])
+For completeness, we give a short direct proof that
+extension extensionality also implies the homotopy extension property
+without passing through weak extension extensionality.
+
+```rzk
+#def htpy-ext-prop-naive-extext
+  ( extext : ExtExt)
+  : HtpyExtProperty
   :=
-    first
-    ( axiom-choice
-      ( I)
-      ( ψ)
-      ( ϕ)
-      ( A)
-      ( \ t y → y = b t)
-      ( a)
-      ( e))
-    ( first
-      ( weakextext
-        ( I)
-        ( ψ)
-        ( ϕ)
-        ( \ t → (Σ (y : A t) , y = b t))
-        ( \ t → is-contr-endpoint-based-paths
-                ( A t)
-                ( b t))
-        ( \ t → ( a t , e t) )))
+  \ I ψ ϕ A b a →
+  ind-has-section-equiv (a = (\ (t : ϕ) → b t)) ((t : ϕ) → a t = b t)
+  ( equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t) (\ _ → recBOT)
+    ( a) (\ (t : ϕ) → b t))
+  ( instance-HtpyExtProperty I ψ ϕ A b a)
+  ( \ e' →
+    ind-rev-fib
+    ( (t : ψ) → A t) ((t : ϕ) → A t) (\ b' t → b' t)
+    ( \ a' (b', p) →
+      instance-HtpyExtProperty I ψ ϕ A b' a'
+      ( ext-htpy-eq I (\ t → ϕ t) (\ _ → BOT) (\ t → A t) (\ _ → recBOT)
+        ( a') (\ (t : ϕ) → b' t) ( p)))
+    ( \ b' → ( b' , \ _ → refl))
+    ( a) (b , e'))
 ```
 
+### Homotopy extension property and NaiveExtExt imply WeakExtExt
+
+This section contains the original proof of RS17, Proposition 4.11
+stating that NaiveExtExt and HptyExtProperty jointly imply WeakExtExt.
+In light of `weakextext-naiveextext`, this is now redundant.
+We keep it around since some intermediate statements might still be useful.
+
 In an extension type of a dependent type that is pointwise contractible, then we
 have an inhabitant of the extension type witnessing the contraction, at every
 inhabitant of the base, of each point in the fiber to the center of the fiber.
 Both directions of this statement will be needed.
 
 ```rzk
-
 #def eq-ext-is-contr
   ( I : CUBE)
   ( ψ : I → TOPE)
@@ -845,7 +866,7 @@ Both directions of this statement will be needed.
   ( a : (t : ϕ ) → A t)
   ( is-contr-fiberwise-A : (t : ψ ) → is-contr ( A t))
   : (t : ϕ ) → ((first (is-contr-fiberwise-A t)) = a t)
-  :=  \ t → ( second (is-contr-fiberwise-A t) (a t))
+  := \ t → ( second (is-contr-fiberwise-A t) (a t))
 
 #def codomain-eq-ext-is-contr
   ( I : CUBE)
@@ -855,17 +876,19 @@ Both directions of this statement will be needed.
   ( a : (t : ϕ ) → A t)
   ( is-contr-fiberwise-A : (t : ψ ) → is-contr ( A t))
   : (t : ϕ ) → (a t = first (is-contr-fiberwise-A t))
-  :=  \ t →
-          rev
-            ( A t )
-            ( first (is-contr-fiberwise-A t) )
-            ( a t)
-            ( second (is-contr-fiberwise-A t) (a t))
-
+  :=
+    \ t →
+      rev
+      ( A t )
+      ( first (is-contr-fiberwise-A t) )
+      ( a t)
+      ( second (is-contr-fiberwise-A t) (a t))
 ```
 
 The below gives us the inhabitant
-$(a', e') : \sum_{\left\langle\prod_{t : I|\psi} A (t) \biggr|^\phi_a\right\rangle} \left\langle \prod_{t: I |\psi} a'(t) = b(t)\biggr|^\phi_e \right\rangle$
+$(a', e')
+: \sum_{\left\langle\prod_{t : I|\psi} A (t) \biggr|^\phi_a\right\rangle}
+\left\langle \prod_{t: I |\psi} a'(t) = b(t)\biggr|^\phi_e \right\rangle$
 from the first part of the proof of RS Prop 4.11. It amounts to the fact that
 parameterized contractibility, i.e. `#!rzk A : ψ → U` such that each `A t` is
 contractible, implies the hypotheses of the homotopy extension property are
@@ -873,7 +896,6 @@ satisfied, and so assuming homotopy extension property, we are entitled to the
 conclusion.
 
 ```rzk
-
 #define htpy-ext-prop-is-fiberwise-contr
   (htpy-ext-property : HtpyExtProperty)
   ( I : CUBE)
@@ -882,17 +904,12 @@ conclusion.
   ( A : ψ → U)
   ( a : (t : ϕ ) → A t)
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
-  : Σ (a' : (t : ψ ) → A t [ϕ t ↦ a t]),
-           ((t : ψ ) →
-            (restrict I ψ ϕ A a a' t =
-              first (is-contr-fiberwise-A t))
-              [ϕ t ↦ codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A t] )
+  : Σ ( a' : (t : ψ ) → A t [ϕ t ↦ a t])
+    , ( ( t : ψ )
+      → ( ( a' t) =_{ A t} first (is-contr-fiberwise-A t))
+        [ ϕ t ↦ codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A t] )
   :=
-    htpy-ext-property
-    ( I )
-    ( ψ )
-    ( ϕ )
-    ( A )
+    htpy-ext-property I ψ ϕ A
     (\ t →  first (is-contr-fiberwise-A t))
     ( a)
     ( codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A)
@@ -913,12 +930,26 @@ generality is needed.
   ( a : (t : ϕ ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
-  : (t : ψ ) → f t = (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t
-  := \ t → all-elements-equal-is-contr
-              ( A t)
-              ( is-contr-fiberwise-A t)
-              ( f t )
-              ( restrict I ψ ϕ A a (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)
+  : ( t : ψ )
+  → ( f t
+    = first
+      ( htpy-ext-prop-is-fiberwise-contr
+        htpy-ext-prop
+        I ψ ϕ A a
+        is-contr-fiberwise-A)
+      ( t))
+  :=
+    \ t →
+    all-elements-equal-is-contr
+    ( A t)
+    ( is-contr-fiberwise-A t)
+    ( f t )
+    ( ( first
+        ( htpy-ext-prop-is-fiberwise-contr
+          htpy-ext-prop
+          I ψ ϕ A a
+          is-contr-fiberwise-A))
+      ( t))
 ```
 
 And below proves that `#!rzk c(t) = refl`. Again, this is a consequence of a
@@ -938,16 +969,13 @@ slightly more general statement.
   : (t : ϕ ) → (refl =_{f t = a' t} c t)
   :=  \ t →
     all-paths-equal-is-contr
-    ( A t)
-    ( is-fiberwise-contr t)
-    ( f t)
-    ( a' t)
-    ( refl )
-    ( c t )
+    (A t) ( is-fiberwise-contr t)
+    ( f t) ( a' t) ( refl ) ( c t )
 ```
 
 Given the `#!rzk a'` produced above, the following gives an inhabitant of
-$\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\rangle$
+$\left \langle_{t : I |\psi}
+f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\rangle$
 
 ```rzk
 #define is-fiberwise-contr-ext-is-fiberwise-contr
@@ -957,7 +985,6 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r
   ( ϕ : ψ → TOPE)
   ( A : ψ → U)
   ( is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
- -- ( b : (t : ψ) → A t)
   ( a : (t : ϕ) → A t)
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   : (t : ψ ) →
@@ -966,38 +993,37 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r
                 htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A)) t)[ϕ t ↦ refl]
   :=
   first(
-    htpy-ext-prop
-    ( I )
-    ( ψ )
-    ( ϕ )
-    ( \ t → f t = first
-                  (htpy-ext-prop-is-fiberwise-contr
-                    htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A) t)
+    htpy-ext-prop I ψ ϕ
+    ( \ t →
+      ( ( f t)
+      = first
+        ( htpy-ext-prop-is-fiberwise-contr
+          htpy-ext-prop
+          I ψ ϕ A a
+          is-contr-fiberwise-A)
+        ( t)))
     ( RS-4-11-c
       htpy-ext-prop I ψ ϕ A a f is-contr-fiberwise-A)
     ( \ t → refl )
-    ( RS-4-11-c-is-refl
-      ( I)
-      ( ψ)
-      ( ϕ)
-      ( A)
+    ( RS-4-11-c-is-refl I ψ ϕ A
       ( is-contr-fiberwise-A)
       ( a )
       ( f )
-      ( first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
+      ( first
+        ( htpy-ext-prop-is-fiberwise-contr
+          htpy-ext-prop
+          I ψ ϕ A a
+          is-contr-fiberwise-A))
       ( RS-4-11-c
         ( htpy-ext-prop)
-        ( I)
-        ( ψ)
-        ( ϕ)
-        ( A)
-        ( a)
-        ( f)
+        ( I) ( ψ) ( ϕ) ( A) ( a) ( f)
         ( is-contr-fiberwise-A ))))
+```
 
-#define weak-ext-ext-from-eq-ext-htpy-htpy-ext-property
- (naiveextext : NaiveExtExt)
- (htpy-ext-prop : HtpyExtProperty)
+```rzk  title="RS17, Proposition 4.11"
+#define weak-extext-naiveextext-htpy-ext-property
+ ( naiveextext : NaiveExtExt)
+ ( htpy-ext-prop : HtpyExtProperty)
  : WeakExtExt
   := \ I ψ ϕ A is-contr-fiberwise-A a →
     (first (htpy-ext-prop-is-fiberwise-contr htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A),
@@ -1007,26 +1033,26 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r
       ( f )
       ( first (htpy-ext-prop-is-fiberwise-contr
                 htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
-      (naiveextext
-      ( I)
-      ( ψ )
-      ( ϕ )
-      ( A)
-      ( a)
-      ( f)
+      ( naiveextext I ψ ϕ A a f
       ( first (htpy-ext-prop-is-fiberwise-contr
                 htpy-ext-prop I ψ ϕ A a is-contr-fiberwise-A))
       ( is-fiberwise-contr-ext-is-fiberwise-contr
         ( htpy-ext-prop)
-        ( I)
-        ( ψ )
-        ( ϕ )
-        ( A)
+        ( I) ( ψ ) ( ϕ ) ( A)
         ( is-contr-fiberwise-A)
         ( a)
         ( f))))
 ```
 
+## Applications of extension extensionality
+
+We now assume extension extensionality and derive a few consequences.
+
+```rzk
+#assume extext : ExtExt
+#assume naiveextext : NaiveExtExt
+```
+
 ### Pointwise homotopy extension types
 
 Using `ExtExt` we can write the homotopy in the homotopy extension type
@@ -1044,7 +1070,8 @@ pointwise.
   ( σ : (t : ϕ) → A t)
   : U
   :=
-    Σ ( τ : (t : ψ) → A t) , ( (t : ϕ) → (τ t =_{ A t} σ t))
+    Σ ( τ : (t : ψ) → A t)
+    , ( (t : ϕ) → (τ t =_{ A t} σ t))
 
 #def equiv-pointwise-homotopy-extension-type uses (extext)
   ( σ : (t : ϕ) → A t)
@@ -1057,7 +1084,8 @@ pointwise.
     ( \ τ → (\ t → τ t) =_{ (t : ϕ) → A t} σ)
     ( \ τ → (t : ϕ) → (τ t = σ t))
     ( \ τ →
-      equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t)
+      equiv-ExtExt extext
+      ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → A t)
       ( \ _ → recBOT) (\ t → τ t) σ)
 
 #def extension-type-pointwise-weakening uses (extext)
@@ -1116,8 +1144,9 @@ Given a map `α : A' → A`, there is also a notion of relative extension types.
     ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ)
     ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
     ( \ τ' →
-      equiv-ExtExt extext I ψ ϕ A (\ t → α t (σ' t))
-        ( \ t → α t (τ' t)) ( τ))
+      equiv-ExtExt extext I ψ ϕ A
+      ( \ t → α t (σ' t))
+      ( \ t → α t (τ' t)) ( τ))
 #end relative-extension-types
 ```
 
@@ -1152,17 +1181,17 @@ extension types are also contractible.
 #def has-contr-relative-extension-types
   : U
   :=
-  ( ( σ' : (t : ϕ) → A' t)
-  → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
-  → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ)))
+    ( ( σ' : (t : ϕ) → A' t)
+    → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
+    → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ)))
 
 #def has-contr-general-relative-extension-types
   : U
   :=
-  ( ( σ' : (t : ϕ) → A' t)
-  → ( τ : (t : ψ) → A t)
-  → ( h : (t : ϕ) → α t (σ' t) = τ t)
-  → ( is-contr ( general-relative-extension-type σ' τ h)))
+    ( ( σ' : (t : ϕ) → A' t)
+    → ( τ : (t : ψ) → A t)
+    → ( h : (t : ϕ) → α t (σ' t) = τ t)
+    → ( is-contr ( general-relative-extension-type σ' τ h)))
 
 #def has-contr-relative-extension-types-generalize' uses (extext)
   ( has-contr-relext-α : has-contr-relative-extension-types)
@@ -1171,7 +1200,8 @@ extension types are also contractible.
   ( h : (t : ϕ) → α t (σ' t) = τ t)
   : is-contr
     ( general-relative-extension-type σ' τ
-      ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))))
+      ( \ t →
+        rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t))))
   :=
     ind-has-section-equiv
     ( extension-type I ψ ϕ A (\ t → α t (σ' t)))
@@ -1208,9 +1238,8 @@ The converse is of course trivial.
 ```rzk
 #def has-contr-relative-extension-types-specialize
   ( has-contr-gen-relext-α : has-contr-general-relative-extension-types)
-  :  has-contr-relative-extension-types
-  :=
-    \ σ' τ → has-contr-gen-relext-α σ' τ (\ _ → refl)
+  : has-contr-relative-extension-types
+  := \ σ' τ → has-contr-gen-relext-α σ' τ (\ _ → refl)
 
 #end general-extension-types
 ```
@@ -1275,7 +1304,7 @@ then so is the map of maps `map-of-restriction-maps`.
   : 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 →
-            eq-ext-htpy I ψ ( \ t → BOT)
+            naiveextext-extext extext I ψ ( \ t → BOT)
               ( A)
               ( \ u → recBOT)
               ( \ t → first (first (is-equiv-f t)) (f t (a t)))
@@ -1283,7 +1312,7 @@ then so is the map of maps `map-of-restriction-maps`.
               ( \ t → second (first (is-equiv-f t)) (a t))))
       , ( ( \ b t → first (second (is-equiv-f t)) (b t))
         , ( \ b →
-            eq-ext-htpy I ψ ( \ t → BOT)
+            naiveextext-extext extext I ψ ( \ t → BOT)
               ( B)
               ( \ u → recBOT)
               ( \ t → f t (first (second (is-equiv-f t)) (b t)))
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index ed74e32c..289861b0 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -1490,7 +1490,7 @@ As a special case of the above:
   :=
     ( \ _ → unit ,
       \ k →
-      eq-ext-htpy extext
+      naiveextext-extext extext
         ( 2 × 2) Δ² (\ _ → BOT)
         ( \ _ → Unit) (\ _ → recBOT)
         ( \ _ → unit) k
diff --git a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
index 85ddd775..5075d86b 100644
--- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
+++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
@@ -62,7 +62,7 @@ pointwise equal.
   ( x : A)
   : ( ap-hom A B F x x (id-hom A x)) = (id-hom B (F x))
   :=
-    eq-ext-htpy
+    naiveextext-extext
       ( extext)
       ( 2)
       ( Δ¹)

From 590ef7093a4890521dc497eb3ba8516f7e9acc32 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 19:53:04 +0200
Subject: [PATCH 09/20] autoformat

---
 src/simplicial-hott/03-extension-types.rzk.md | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index 03814870..fe148fa2 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -820,12 +820,12 @@ the point of contraction for weak extension extensionality.
         ( \ t → ( a t , e t) )))
 ```
 
-For completeness, we give a short direct proof that
-extension extensionality also implies the homotopy extension property
-without passing through weak extension extensionality.
+For completeness, we give a short direct proof that extension extensionality
+also implies the homotopy extension property without passing through weak
+extension extensionality.
 
 ```rzk
-#def htpy-ext-prop-naive-extext
+#def htpy-ext-prop-extext
   ( extext : ExtExt)
   : HtpyExtProperty
   :=
@@ -847,10 +847,10 @@ without passing through weak extension extensionality.
 
 ### Homotopy extension property and NaiveExtExt imply WeakExtExt
 
-This section contains the original proof of RS17, Proposition 4.11
-stating that NaiveExtExt and HptyExtProperty jointly imply WeakExtExt.
-In light of `weakextext-naiveextext`, this is now redundant.
-We keep it around since some intermediate statements might still be useful.
+This section contains the original proof of RS17, Proposition 4.11 stating that
+NaiveExtExt and HptyExtProperty jointly imply WeakExtExt. In light of
+`weakextext-naiveextext`, this is now redundant. We keep it around since some
+intermediate statements might still be useful.
 
 In an extension type of a dependent type that is pointwise contractible, then we
 have an inhabitant of the extension type witnessing the contraction, at every
@@ -1020,7 +1020,7 @@ f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\rangle$
         ( is-contr-fiberwise-A ))))
 ```
 
-```rzk  title="RS17, Proposition 4.11"
+```rzk title="RS17, Proposition 4.11"
 #define weak-extext-naiveextext-htpy-ext-property
  ( naiveextext : NaiveExtExt)
  ( htpy-ext-prop : HtpyExtProperty)

From 3098910b634e195879af8d04c39d274df97c552c Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 21:17:49 +0200
Subject: [PATCH 10/20] fibers between segal types

---
 src/simplicial-hott/05-segal-types.rzk.md | 48 ++++++++++++++++++++++-
 1 file changed, 47 insertions(+), 1 deletion(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index ed74e32c..b8019dc9 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -417,7 +417,7 @@ for the inclusion `Λ ⊂ Δ¹`.
   : U → U
   := is-local-type (2 × 2) Δ² (\ t → Λ t)
 
-#def is-local-horn-inclusion-unpacked
+#def unpack-is-local-horn-inclusion
   ( A : U)
   : is-local-horn-inclusion A = is-equiv (Δ² → A) (Λ → A) (horn-restriction A)
   := refl
@@ -570,6 +570,28 @@ We have now proven that both notions of Segal types are logically equivalent.
   := (is-local-horn-inclusion-is-segal A , is-segal-is-local-horn-inclusion A)
 ```
 
+Similarly, Segal types are characterized by having unique extensions along
+`Λ ⊂ Δ²`.
+
+```rzk
+#def is-segal-has-unique-inner-extensions
+  ( A : U)
+  ( has-inner-ue-A : has-unique-extensions (2 × 2) (Δ²) (\ t → Λ t) A)
+  : is-segal A
+  :=
+    is-segal-is-local-horn-inclusion A
+    ( is-local-type-has-unique-extensions (2 × 2) (Δ²) (\ t → Λ t) A
+      has-inner-ue-A)
+
+#def has-unique-inner-extensions-is-segal
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  : has-unique-extensions (2 × 2) (Δ²) (\ t → Λ t) A
+  :=
+    has-unique-extensions-is-local-type (2 × 2) (Δ²) (\ t → Λ t) A
+    ( is-local-horn-inclusion-is-segal A is-segal-A)
+```
+
 ## Segal function and extension types
 
 Using the new characterization of Segal types, we can show that the type of
@@ -1866,3 +1888,27 @@ products of morphisms. It is implicitly stated in Proposition 8.21.
 
 #end morphisms-of-products-is-products-of-morphisms
 ```
+
+## Fibers of maps between Segal types
+
+For any map `f : A → B` between Segal types, each fiber `fib A B f b` is again a
+Segal type. This is an instance of a general statement about types with unique
+extensions for the shape inclusion `Λ ⊂ Δ²`.
+
+```rzk
+#def is-fiberwise-segal-are-segal
+  ( A B : U)
+  ( f : A → B)
+  ( is-segal-A : is-segal A)
+  ( is-segal-B : is-segal B)
+  ( b : B)
+  : is-segal (fib A B f b)
+  :=
+    is-segal-has-unique-inner-extensions (fib A B f b)
+    ( has-fiberwise-unique-extensions-have-unique-extensions
+      extext weakextext
+      ( 2 × 2) (Δ²) (\ t → Λ t) A B f
+      ( has-unique-inner-extensions-is-segal A is-segal-A)
+      ( has-unique-inner-extensions-is-segal B is-segal-B)
+      ( b))
+```

From b84295ef3cce02adf13e837ecf908e355ff40113 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 21:20:26 +0200
Subject: [PATCH 11/20] make usage of extext explicit

---
 src/simplicial-hott/05-segal-types.rzk.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index b8019dc9..0ad043a6 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -1896,7 +1896,7 @@ Segal type. This is an instance of a general statement about types with unique
 extensions for the shape inclusion `Λ ⊂ Δ²`.
 
 ```rzk
-#def is-fiberwise-segal-are-segal
+#def is-fiberwise-segal-are-segal uses (extext weakextext)
   ( A B : U)
   ( f : A → B)
   ( is-segal-A : is-segal A)

From 5623be8c5a689b5c287ee90ac08ba26f34b20688 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Sun, 15 Oct 2023 18:44:43 +0200
Subject: [PATCH 12/20] pushout products

---
 .../04-right-orthogonal.rzk.md                | 45 +++++++++++++++++--
 src/simplicial-hott/08-covariant.rzk.md       |  2 +-
 2 files changed, 42 insertions(+), 5 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 12154ce0..7322d21e 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -283,12 +283,11 @@ shape retract, then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` then so is `χ × ϕ ⊂ χ × ψ` for
 every other shape `χ`.
 
-The following proof uses a lot of currying and uncurrying and relies on (the
-naive form of) extension extensionality.
+The following proof uses a lot of currying and uncurrying and relies extension
+extensionality.
 
 ```rzk
-#def is-right-orthogonal-to-shape-× uses (naiveextext)
--- this should be refactored by introducing cofibration-product-functorial
+#def is-right-orthogonal-to-shape-product uses (naiveextext)
   ( A' A : U)
   ( α : A' → A)
   ( J : CUBE)
@@ -370,6 +369,44 @@ For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to
          ( is-orth-ϕ-ψ∧ϕ ( \ t → τ' t))
 ```
 
+### Pushout products
+
+Combining the stability under pushouts and crossing with a shape, we get
+stability under pushout products.
+
+```rzk
+#def is-right-orthogonal-to-shape-pushout-product uses (naiveextext)
+  ( A' A : U)
+  ( α : A' → A)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : is-right-orthogonal-to-shape (J × I)
+    ( \ (t,s) → χ t ∧ ψ s)
+    ( \ (t,s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+    ( A') ( A) ( α)
+  :=
+    is-right-orthogonal-to-shape-left-cancel A' A α (J × I)
+    ( \ (t,s) → χ t ∧ ψ s)
+    ( \ (t,s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+    ( \ (t,s) → χ t ∧ ϕ s)
+    ( is-right-orthogonal-to-shape-pushout A' A α (J × I)
+      ( \ (t,s) → ζ t ∧ ψ s)
+      ( \ (t,s) → χ t ∧ ϕ s)
+      ( is-right-orthogonal-to-shape-product A' A α
+        ( J) ( \ t → ζ t)
+        ( I) ( ψ) ( ϕ)
+        (is-orth-ψ-ϕ)))
+    ( is-right-orthogonal-to-shape-product A' A α
+      ( J) ( χ)
+      ( I) ( ψ) ( ϕ)
+      ( is-orth-ψ-ϕ))
+```
+
 ## Stability properties of right orthogonal maps
 
 Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index ad6c8bc4..e89ba422 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -368,7 +368,7 @@ Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the pro
   : is-right-orthogonal-to-shape
       ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts) A' A α
   :=
-    is-right-orthogonal-to-shape-× naiveextext A' A α
+    is-right-orthogonal-to-shape-product naiveextext A' A α
       2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) is-left-fib-α
 ```
 

From 936c211b1d94b26052c7308994541e7dd591559e Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Sun, 15 Oct 2023 20:32:32 +0200
Subject: [PATCH 13/20] add transposition

---
 .../04-right-orthogonal.rzk.md                | 87 +++++++++++++++++--
 1 file changed, 81 insertions(+), 6 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 7322d21e..ef17dc76 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -278,6 +278,47 @@ shape retract, then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
 #end left-orthogonal-calculus-1
 ```
 
+### Transposition
+
+Inside a product of cube `I × J`, we can interchange the two factors without
+affecting left orthogonality.
+
+```rzk
+#def is-right-orthogonal-to-shape-transpose
+  ( A' A : U)
+  ( α : A' → A)
+  ( I J : CUBE)
+  ( ψ : (I × J) → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape (I × J)
+    ( \ (s , t) → ψ (s , t))
+    ( \ (s , t) → ϕ (s , t))
+    ( A') ( A) ( α))
+  : is-right-orthogonal-to-shape (J × I)
+    ( \ (t , s) → ψ (s , t))
+    ( \ (t , s) → ϕ (s , t))
+    ( A') (A) (α)
+  :=
+    \ σ' →
+    is-equiv-Equiv-is-equiv
+    ( ( (t , s) : J × I | ψ (s , t)) → A' [ϕ (s , t) ↦ σ' (t , s)])
+    ( ( (t , s) : J × I | ψ (s , t)) → A [ϕ (s , t) ↦ α (σ' (t , s))])
+    ( \ τ' ts → α (τ' ts))
+    ( ((s , t) : I × J | ψ (s , t)) → A' [ϕ (s , t) ↦ σ' (t , s)])
+    ( ((s , t) : I × J | ψ (s , t)) → A [ϕ (s , t) ↦ α (σ' (t , s))])
+    ( \ τ' st → α (τ' st))
+    ( ( ( ( \ v (x , y) → v (y , x))
+        , ( \ v (x , y) → v (y , x))
+        )
+      , ( \ _ → refl)
+      )
+    , ( ( ( ( \ v (x , y) → v (y , x)) , ( \ _ → refl))
+        , ( ( \ v (x , y) → v (y , x)) , ( \ _ → refl)))
+      , ( ( ( \ v (x , y) → v (y , x)) , ( \ _ → refl))
+        , ( ( \ v (x , y) → v (y , x)) , ( \ _ → refl)))))
+    ( is-orth-ψ-ϕ (\ (s , t) → σ' (t , s)))
+```
+
 ### Stability under exponentiation
 
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` then so is `χ × ϕ ⊂ χ × ψ` for
@@ -342,6 +383,23 @@ extensionality.
                   ( ( second ( second (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                     ( \ s' → τ (t, s')))
                   ( s))))
+
+#def is-right-orthogonal-to-shape-product' uses (naiveextext)
+  ( A' A : U)
+  ( α : A' → A)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : is-right-orthogonal-to-shape
+      ( I × J) ( \ (s , t) → ψ s ∧ χ t) ( \ (s , t) → ϕ s ∧ χ t) A' A α
+  :=
+    is-right-orthogonal-to-shape-transpose A' A α J I
+    ( \ (t , s) → χ t ∧ ψ s)
+    ( \ (t , s) → χ t ∧ ϕ s)
+    ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ is-orth-ψ-ϕ)
 ```
 
 ### Stability under exact pushouts
@@ -397,13 +455,30 @@ stability under pushout products.
     ( is-right-orthogonal-to-shape-pushout A' A α (J × I)
       ( \ (t,s) → ζ t ∧ ψ s)
       ( \ (t,s) → χ t ∧ ϕ s)
-      ( is-right-orthogonal-to-shape-product A' A α
-        ( J) ( \ t → ζ t)
-        ( I) ( ψ) ( ϕ)
+      ( is-right-orthogonal-to-shape-product A' A α J ( \ t → ζ t) I ψ ϕ
         (is-orth-ψ-ϕ)))
-    ( is-right-orthogonal-to-shape-product A' A α
-      ( J) ( χ)
-      ( I) ( ψ) ( ϕ)
+    ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ
+      ( is-orth-ψ-ϕ))
+
+#def is-right-orthogonal-to-shape-pushout-product' uses (naiveextext)
+  ( A' A : U)
+  ( α : A' → A)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : is-right-orthogonal-to-shape (I × J)
+    ( \ (s , t) → ψ s ∧ χ t)
+    ( \ (s , t) → (ϕ s ∧ χ t) ∨ (ψ s ∧ ζ t))
+    ( A') ( A) ( α)
+  :=
+    is-right-orthogonal-to-shape-transpose A' A α J I
+    ( \ (t,s) → χ t ∧ ψ s)
+    ( \ (t,s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+    ( is-right-orthogonal-to-shape-pushout-product A' A α J χ ζ I ψ ϕ
       ( is-orth-ψ-ϕ))
 ```
 

From b892f591145be60b36196646a5e51dd9becc7eb6 Mon Sep 17 00:00:00 2001
From: cesarbm03 <cbard035@uottawa.ca>
Date: Mon, 16 Oct 2023 13:14:55 -0400
Subject: [PATCH 14/20] colimits are unique up to isomorphism

---
 src/simplicial-hott/13-limits.rzk.md | 138 ++++++++++++++++++++-------
 1 file changed, 103 insertions(+), 35 deletions(-)

diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md
index 7b42b546..2442b580 100644
--- a/src/simplicial-hott/13-limits.rzk.md
+++ b/src/simplicial-hott/13-limits.rzk.md
@@ -8,6 +8,13 @@ This is a literate `rzk` file:
 #lang rzk-1
 ```
 
+Some definitions make use of function extentionality.
+
+```rzk
+#assume funext : FunExt
+#assume naiveextext : NaiveExtExt
+```
+
 ## Definition limits and colimits
 
 Given a function `#!rzk f : A → B` and `#!rzk b:B` we define the type of cones
@@ -15,8 +22,8 @@ over `#!rzk f`.
 
 ```rzk
 #def cone
-  ( A B : U )
-  ( f : A → B )
+  ( A B : U)
+  ( f : A → B)
   : U
   := Σ (b : B), hom (A → B) (constant A B b) f
 ```
@@ -26,8 +33,8 @@ under `#!rzk f`.
 
 ```rzk
 #def cocone
-  ( A B : U )
-  ( f : A → B )
+  ( A B : U)
+  ( f : A → B)
   : U
   := Σ (b : B), hom ( A → B) f (constant A B b)
 ```
@@ -39,54 +46,50 @@ We define a colimit for `#!rzk f : A → B` as an initial cocone under `#!rzk f`
   ( A B : U )
   ( f : A → B )
   : U
-  := Σ ( x : cocone A B f ) , is-initial (cocone A B f) x
+  := Σ ( x : cocone A B f) , is-initial ( cocone A B f) x
 ```
 
-We define a limit of `#!rzk f : A → B` as a terminal cone over `#!rzk f`.
+We define a limit of `#!rzk f : A → B` as a final cone over `#!rzk f`.
 
 ```rzk
 #def limit
   ( A B : U )
   ( f : A → B )
   : U
-  :=  Σ ( x : cone A B f ) , is-final (cone A B f) x
+  :=  Σ ( x : cone A B f) , is-final ( cone A B f) x
 ```
 
 We give a second definition of limits, we eventually want to prove both
 definitions coincide. Define cone as a family.
 
 ```rzk
-#def cone2
+#def family-cone
   (A B : U)
   : (A → B) → (B) → U
   := \ f → \ b → (hom (A → B) (constant A B b) f)
-```
 
-```rzk
 #def constant-nat-trans
   (A B : U)
   ( x y : B )
   ( k : hom B x y)
   : hom (A → B) (constant A B x) (constant A B y)
   := \ t a → ( constant A ( hom B x y ) k ) a t
-```
 
-```rzk
 #def cone-precomposition
   ( A B : U)
   ( is-segal-B : is-segal B)
   ( f : A → B )
   ( b x : B )
   ( k : hom B b x)
-  : (cone2 A B f x) →  (cone2 A B f b)
+  : ( family-cone A B f x) →  ( family-cone A B f b)
   := \ α → vertical-comp-nat-trans
               ( A)
               ( \ a → B)
               ( \ a → is-segal-B)
               ( constant A B b)
               ( constant A B x)
-              (f)
-              ( constant-nat-trans A B b x k )
+              ( f)
+              ( constant-nat-trans A B b x k)
               ( α)
 ```
 
@@ -99,34 +102,35 @@ Another definition of limit.
   ( f : A → B)
   : U
   := Σ (b : B),
-     Σ ( c : cone2 A B f b ),
-     ( x : B) → ( k : hom B b x)
-      → is-equiv (cone2 A B f x) (cone2 A B f b) (cone-precomposition A B is-segal-B f b x k )
+     Σ ( c : family-cone A B f b)
+     , ( x : B) → ( k : hom B b x)
+     → is-equiv
+        ( family-cone A B f x)
+        ( family-cone A B f b)
+        ( cone-precomposition A B is-segal-B f b x k)
 ```
 
 We give a second definition of colimits, we eventually want to prove both
 definitions coincide. Define cocone as a family.
 
 ```rzk
-#def cocone2
+#def family-cocone
   (A B : U)
-  : (A → B) → (B) → U
+  : ( A → B) → ( B) → U
   := \ f → \ b → (hom (A → B) f (constant A B b))
-```
 
-```rzk
 #def cocone-postcomposition
   ( A B : U)
   ( is-segal-B : is-segal B)
-  ( f : A → B )
-  ( x b : B )
+  ( f : A → B)
+  ( x b : B)
   ( k : hom B x b)
-  : (cocone2 A B f x) → (cocone2 A B f b)
+  : ( family-cocone A B f x) → ( family-cocone A B f b)
   := \ α → vertical-comp-nat-trans
               ( A)
               ( \ a → B)
               ( \ a → is-segal-B)
-              (f)
+              ( f)
               ( constant A B x)
               ( constant A B b)
               ( α)
@@ -142,9 +146,12 @@ Another definition of colimit.
   ( f : A → B)
   : U
   := Σ (b : B),
-     Σ ( c : cocone2 A B f b ),
-     ( x : B) → ( k : hom B x b)
-      → is-equiv (cocone2 A B f x) (cocone2 A B f b) (cocone-postcomposition A B is-segal-B f x b k )
+     Σ ( c : family-cocone A B f b)
+     , ( x : B) → ( k : hom B x b)
+     → is-equiv
+        ( family-cocone A B f x)
+        ( family-cocone A B f b)
+        ( cocone-postcomposition A B is-segal-B f x b k)
 ```
 
 The following alternative definition does not require a Segalness condition.
@@ -155,15 +162,13 @@ When `#!rzk is-segal B` then definitions 1 and 3 coincide.
   ( A B : U)
   ( f : A → B)
   : U
-  := Σ ( b : B),(x : B) → Equiv (hom B b x ) (cone2 A B f x)
-```
+  := Σ ( b : B),( x : B) → Equiv ( hom B b x) ( family-cone A B f x)
 
-```rzk
 #def colimit3
   ( A B : U)
   ( f : A → B)
   : U
-  := Σ ( b : B),(x : B) → Equiv (hom B x b ) (cocone2 A B f x)
+  := Σ ( b : B), ( x : B) → Equiv ( hom B x b) ( family-cocone A B f x)
 ```
 
 ## Uniqueness of initial and final objects.
@@ -207,7 +212,6 @@ In a Segal type, final objects are isomorphic.
   ( a b : A)
   ( is-final-a : is-final A a)
   ( is-final-b : is-final A b)
-  ( iso : Iso A is-segal-A a b)
   : Iso A is-segal-A a b
   :=
     ( first (is-final-b a) ,
@@ -229,4 +233,68 @@ In a Segal type, final objects are isomorphic.
             ( id-hom A b))))
 ```
 
-## Uniqueness up to isomophism of (co)limits
+## Uniqueness up to isomophism of (co)limits.
+
+The type of cocones of a function with codomain a Segal type is a Segal type.
+
+```rzk title="BM22, Remark 4 (i)"
+#def is-covariant-family-cone-is-segal
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  : is-covariant B ( \ b → family-cocone A B f b)
+  :=
+    is-covariant-substitution-is-covariant
+      ( A → B)
+      ( B)
+      ( hom ( A → B) f)
+      ( is-covariant-representable-is-segal
+          ( A → B)
+          ( is-segal-function-type
+            ( funext)
+            ( A)
+            ( \ _ → B)
+            ( \ _ → is-segal-B))
+          ( f))
+      ( \ b → constant A B b)
+
+#def is-segal-cocone-is-segal uses (funext)
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  : is-segal ( cocone A B f)
+  :=
+    is-segal-total-type-covariant-family-is-segal-base
+      ( naiveextext)
+      ( B)
+      ( family-cocone A B f)
+      ( is-covariant-family-cone-is-segal
+          ( A)
+          ( B)
+          ( is-segal-B)
+          ( f))
+      ( is-segal-B)
+```
+
+Colimits are unique up to isomorphism.
+
+```rzk title="BM, Corollary 1 (i)"
+#def iso-colimit-is-segal uses ( naiveextext funext)
+  ( A B : U)
+  ( is-segal-B : is-segal B)
+  ( f : A → B)
+  ( x y : colimit A B f)
+  : Iso
+      ( cocone A B f)
+      ( is-segal-cocone-is-segal A B is-segal-B f)
+      ( first x)
+      ( first y)
+  :=
+    iso-initial
+      ( cocone A B f)
+      ( is-segal-cocone-is-segal A B is-segal-B f)
+      ( first x)
+      ( first y)
+      ( second x)
+      ( second y)
+```

From f60e80a9e0f9c4e576c9d9d21a18454a7ef7011e Mon Sep 17 00:00:00 2001
From: Tashi Walde <tashi.walde@ma.tum.de>
Date: Mon, 16 Oct 2023 23:55:22 +0200
Subject: [PATCH 15/20] Update README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 6352fe2d..dca683fc 100644
--- a/README.md
+++ b/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].
 

From f32e79267d3a9237b9f4e1b8f835966e86326919 Mon Sep 17 00:00:00 2001
From: Aras Ergus <arasergus@posteo.net>
Date: Wed, 18 Oct 2023 08:40:09 +0200
Subject: [PATCH 16/20] Equivalences of maps induce equivalences of fibers

An argument by @TashiWalde.
---
 src/hott/11-homotopy-pullbacks.rzk.md | 109 ++++++++++++++++++++++++++
 1 file changed, 109 insertions(+)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 3a2839af..85ab806e 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -617,3 +617,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))
+```

From c48fc7a3c8d0b4fbcf6b379584787cefa7ebc9ed Mon Sep 17 00:00:00 2001
From: Aras Ergus <arasergus@posteo.net>
Date: Wed, 18 Oct 2023 17:46:13 +0200
Subject: [PATCH 17/20] Add a remark about `equiv-domain-sum-of-fibers`

This should make its occurrence in
`is-equiv-map-of-sums-of-fibers-is-equiv-map-of-domains`
clearer.
---
 src/hott/10-trivial-fibrations.rzk.md | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/hott/10-trivial-fibrations.rzk.md b/src/hott/10-trivial-fibrations.rzk.md
index 38cee14a..15e46507 100644
--- a/src/hott/10-trivial-fibrations.rzk.md
+++ 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

From 117f54c082bf4d83a0c94a9d2863cf3c1df4a0e8 Mon Sep 17 00:00:00 2001
From: Aras Ergus <arasergus@posteo.net>
Date: Wed, 18 Oct 2023 17:51:06 +0200
Subject: [PATCH 18/20] Fix a few formatting issues

---
 src/hott/11-homotopy-pullbacks.rzk.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 85ab806e..af765aab 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -683,10 +683,10 @@ that an equivalence of maps induces an equivalence of fibers at each base point.
   ( 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 α)))
+      ( equiv-domain-sum-of-fibers A' A α)))
   ( second
-   ( ( inv-equiv B' (Σ (b : B), fib B' B β b))
-     (equiv-domain-sum-of-fibers B' B β)))
+    ( ( 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

From 38f3b420da1dce9ced797f164ebee948e36a072a Mon Sep 17 00:00:00 2001
From: Emily Riehl <eriehl@math.jhu.edu>
Date: Sat, 21 Oct 2023 20:04:39 -0400
Subject: [PATCH 19/20] Update index.md

---
 src/index.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/index.md b/src/index.md
index 3a94a1bb..efbf6449 100644
--- a/src/index.md
+++ b/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].
 

From 00ef47eeae61992ca43be1cbdd5be7359c5d7d01 Mon Sep 17 00:00:00 2001
From: emilyriehl <emilyriehl@math.jhu.edu>
Date: Sun, 22 Oct 2023 10:56:27 -0400
Subject: [PATCH 20/20] removed some unnecessary space

---
 src/simplicial-hott/13-limits.rzk.md | 116 ++++++++++++++-------------
 1 file changed, 60 insertions(+), 56 deletions(-)

diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md
index 2442b580..0af7298a 100644
--- a/src/simplicial-hott/13-limits.rzk.md
+++ b/src/simplicial-hott/13-limits.rzk.md
@@ -82,15 +82,17 @@ definitions coincide. Define cone as a family.
   ( b x : B )
   ( k : hom B b x)
   : ( family-cone A B f x) →  ( family-cone A B f b)
-  := \ α → vertical-comp-nat-trans
-              ( A)
-              ( \ a → B)
-              ( \ a → is-segal-B)
-              ( constant A B b)
-              ( constant A B x)
-              ( f)
-              ( constant-nat-trans A B b x k)
-              ( α)
+  :=
+  \ α
+  → vertical-comp-nat-trans
+    ( A)
+    ( \ _ → B)
+    ( \ _ → is-segal-B)
+    ( constant A B b)
+    ( constant A B x)
+    ( f)
+    ( constant-nat-trans A B b x k)
+    ( α)
 ```
 
 Another definition of limit.
@@ -102,9 +104,9 @@ Another definition of limit.
   ( f : A → B)
   : U
   := Σ (b : B),
-     Σ ( c : family-cone A B f b)
-     , ( x : B) → ( k : hom B b x)
-     → is-equiv
+  Σ ( c : family-cone A B f b)
+    , ( x : B) → ( k : hom B b x)
+      → is-equiv
         ( family-cone A B f x)
         ( family-cone A B f b)
         ( cone-precomposition A B is-segal-B f b x k)
@@ -126,15 +128,17 @@ definitions coincide. Define cocone as a family.
   ( x b : B)
   ( k : hom B x b)
   : ( family-cocone A B f x) → ( family-cocone A B f b)
-  := \ α → vertical-comp-nat-trans
-              ( A)
-              ( \ a → B)
-              ( \ a → is-segal-B)
-              ( f)
-              ( constant A B x)
-              ( constant A B b)
-              ( α)
-              ( constant-nat-trans A B x b k )
+  :=
+  \ α
+  → vertical-comp-nat-trans
+    ( A)
+    ( \ _ → B)
+    ( \ _ → is-segal-B)
+    ( f)
+    ( constant A B x)
+    ( constant A B b)
+    ( α)
+    ( constant-nat-trans A B x b k )
 ```
 
 Another definition of colimit.
@@ -146,12 +150,12 @@ Another definition of colimit.
   ( f : A → B)
   : U
   := Σ (b : B),
-     Σ ( c : family-cocone A B f b)
-     , ( x : B) → ( k : hom B x b)
-     → is-equiv
-        ( family-cocone A B f x)
-        ( family-cocone A B f b)
-        ( cocone-postcomposition A B is-segal-B f x b k)
+  Σ ( c : family-cocone A B f b)
+    , ( x : B) → ( k : hom B x b)
+    → is-equiv
+      ( family-cocone A B f x)
+      ( family-cocone A B f b)
+      ( cocone-postcomposition A B is-segal-B f x b k)
 ```
 
 The following alternative definition does not require a Segalness condition.
@@ -245,18 +249,18 @@ The type of cocones of a function with codomain a Segal type is a Segal type.
   : is-covariant B ( \ b → family-cocone A B f b)
   :=
     is-covariant-substitution-is-covariant
-      ( A → B)
-      ( B)
-      ( hom ( A → B) f)
-      ( is-covariant-representable-is-segal
-          ( A → B)
-          ( is-segal-function-type
-            ( funext)
-            ( A)
-            ( \ _ → B)
-            ( \ _ → is-segal-B))
-          ( f))
-      ( \ b → constant A B b)
+    ( A → B)
+    ( B)
+    ( hom ( A → B) f)
+    ( is-covariant-representable-is-segal
+        ( A → B)
+        ( is-segal-function-type
+          ( funext)
+          ( A)
+          ( \ _ → B)
+          ( \ _ → is-segal-B))
+        ( f))
+    ( \ b → constant A B b)
 
 #def is-segal-cocone-is-segal uses (funext)
   ( A B : U)
@@ -265,15 +269,15 @@ The type of cocones of a function with codomain a Segal type is a Segal type.
   : is-segal ( cocone A B f)
   :=
     is-segal-total-type-covariant-family-is-segal-base
-      ( naiveextext)
+    ( naiveextext)
+    ( B)
+    ( family-cocone A B f)
+    ( is-covariant-family-cone-is-segal
+      ( A)
       ( B)
-      ( family-cocone A B f)
-      ( is-covariant-family-cone-is-segal
-          ( A)
-          ( B)
-          ( is-segal-B)
-          ( f))
       ( is-segal-B)
+      ( f))
+    ( is-segal-B)
 ```
 
 Colimits are unique up to isomorphism.
@@ -285,16 +289,16 @@ Colimits are unique up to isomorphism.
   ( f : A → B)
   ( x y : colimit A B f)
   : Iso
-      ( cocone A B f)
-      ( is-segal-cocone-is-segal A B is-segal-B f)
-      ( first x)
-      ( first y)
+    ( cocone A B f)
+    ( is-segal-cocone-is-segal A B is-segal-B f)
+    ( first x)
+    ( first y)
   :=
     iso-initial
-      ( cocone A B f)
-      ( is-segal-cocone-is-segal A B is-segal-B f)
-      ( first x)
-      ( first y)
-      ( second x)
-      ( second y)
+    ( cocone A B f)
+    ( is-segal-cocone-is-segal A B is-segal-B f)
+    ( first x)
+    ( first y)
+    ( second x)
+    ( second y)
 ```