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].
 
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/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index e97987fe..46fbe032 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -834,3 +834,112 @@ We summarize the result as the following equivalence:
 
 #end fibers-comm-square
 ```
+
+## 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))
+```
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].
 
diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index fbd71d2b..02747f4a 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))
   := is-equiv-fiberwise-is-equiv-total
       ( (t : ψ ) → A t [ϕ t ↦ a t] )
       ( \ g → (f = g) )
@@ -689,79 +756,45 @@ 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
   : WeakExtExt → ExtExt
-  := \ weakextext I ψ ϕ A a f g →
-      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
+  := extext-weakextext'
 ```
 
-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 +802,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-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 +865,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 +875,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 +895,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 +903,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 +929,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 +968,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 +984,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 +992,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 +1032,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 +1069,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 +1083,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 +1143,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 +1180,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 +1199,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 +1237,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 +1303,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 +1311,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/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 12154ce0..ef17dc76 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -278,17 +278,57 @@ 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
 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)
@@ -343,6 +383,23 @@ naive form of) extension 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
@@ -370,6 +427,61 @@ 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-ψ-ϕ))
+
+#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-ψ-ϕ))
+```
+
 ## Stability properties of right orthogonal maps
 
 Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 6a0b1166..837da1e8 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
@@ -1490,7 +1512,7 @@ As a special case of the above:
   :=
     ( \ _ → unit ,
       \ k →
-      eq-ext-htpy extext
+      naiveextext-extext extext
         ( 2 × 2) Δ² (\ _ → BOT)
         ( \ _ → Unit) (\ _ → recBOT)
         ( \ _ → unit) k
@@ -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 uses (extext weakextext)
+  ( 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))
+```
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)
       ( Δ¹)
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 5647968d..d925c14d 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-α
 ```
 
diff --git a/src/simplicial-hott/09-yoneda.rzk.md b/src/simplicial-hott/09-yoneda.rzk.md
index 36f81b7e..f0d6c927 100644
--- a/src/simplicial-hott/09-yoneda.rzk.md
+++ b/src/simplicial-hott/09-yoneda.rzk.md
@@ -401,6 +401,176 @@ Naturality in `#!rzk C` is not automatic but can be proven easily:
           A is-segal-A a C D is-covariant-C is-covariant-D ψ u x)
 ```
 
+## 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
+  :=
+     yon
+     ( A)
+     ( is-segal-A)
+     ( a)
+     ( hom A a')
+     ( is-covariant-representable-is-segal A is-segal-A a')
+
+#def 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))
+  : ( yoneda-embedding A is-segal-A a a') ( ( evid A a ( hom A a')) φ) = φ
+  :=
+     yon-evid
+      ( A)
+      ( is-segal-A)
+      ( a)
+      ( hom A a')
+      ( is-covariant-representable-is-segal A is-segal-A a') φ
+
+#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')) φ ))
+      ( φ)
+      ( compute-yoneda-embedding-evid A is-segal-A a a' φ)
+
+#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
+      ( 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-compute-yoneda-embedding-evid A is-segal-A a a' φ x)
+
+#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
+  :=
+     rev
+      ( hom A a' x)
+      ( ( ( yoneda-embedding A is-segal-A a a')
+          ( ( evid A a ( hom A a')) φ )) x f)
+      ( φ x f)
+      ( htpy-yoneda-embedding-evid A is-segal-A a a' φ x f)
+```
+
+Define the action by precompostition.
+
+```rzk
+#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 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
+#def eq-yoneda-embedding-precomposition-evid
+  ( 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
+    = precomposition-evid-is-segal 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 )
+```
+
+Now we cocatenate the paths to prove the result as stated.
+
+```rzk
+#def eq-compute-precomposition-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 = (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)
+      ( precomposition-evid-is-segal 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-precomposition-evid
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( a a' : A)
+  ( φ : ( x : A) → ( hom A a x → hom A a' x))
+  ( 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-compute-precomposition-evid A is-segal-A a a' φ x f)
+
+#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
+      ( funext)
+      ( A)
+      ( \ x → ( hom A a x → hom A a' x))
+      ( φ)
+      ( precomposition-evid-is-segal A is-segal-A a a' φ)
+      ( \ x → eq-htpy-precomposition-evid A is-segal-A a a' φ x)
+```
+
 ## Yoneda for contravariant families
 
 Dually, the Yoneda lemma for contravariant type families characterizes natural
diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md
index 7b42b546..0af7298a 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,55 +46,53 @@ 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)
-  := \ α → 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 )
-              ( α)
+  : ( family-cone A B f x) →  ( family-cone A B f b)
+  :=
+  \ α
+  → 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.
@@ -99,38 +104,41 @@ 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)
-  := \ α → 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 )
+  : ( family-cocone A B f x) → ( family-cocone A B f b)
+  :=
+  \ α
+  → 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.
@@ -142,9 +150,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 +166,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 +216,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 +237,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)
+```