diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index 55cc7383..52291225 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -421,8 +421,8 @@ retraction the first map is an equivalence, and dually.
   ( ( ( retr-gf, η-gf), (sec-gf, ε-gf)) : is-equiv A C (comp A B C g f))
   : is-equiv B C g
   :=
-    ( ( comp C A B f retr-gf ,
-        ind-has-section A B f has-section-f
+    ( ( comp C A B f retr-gf
+      , ind-has-section A B f has-section-f
           ( \ b → f (retr-gf (g b)) = b)
           ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a)))
     , ( comp C A B f sec-gf, ε-gf))
@@ -551,6 +551,181 @@ The retraction associated with an equivalence is an equivalence.
       ( is-equiv-section-is-equiv A B f is-equiv-f)
 ```
 
+## Section-retraction pairs
+
+A pair of maps `s : A → B` and `r : B → A'` is a **section-retraction pair** if
+the composite `A → A'` is an equivalence.
+
+```rzk
+#def is-section-retraction-pair
+  ( A B A' : U)
+  ( s : A → B)
+  ( r : B → A')
+  : U
+  := is-equiv A A' (comp A B A' r s)
+```
+
+When we have such a section-retraction pair `(s, r)`, we say that `r` is an
+**external retraction** of `s` and `s` is an **external section** of `r`.
+
+```rzk
+#def has-external-retraction
+  ( A B : U)
+  ( s : A → B)
+  : U
+  :=
+    Σ ((A', r) : ( Σ (A' : U) , B → A'))
+    , ( is-section-retraction-pair A B A' s r)
+
+#def has-external-section
+  ( B A' : U)
+  ( r : B → A')
+  : U
+  :=
+    Σ ((A, s) : ( Σ (A : U) , A → B))
+    , ( is-section-retraction-pair A B A' s r)
+```
+
+Note that exactly like `has-section` and `has-retraction` these are not
+_properties_ of `s` or `r`, but structure.
+
+Without univalence, we cannot yet show that the types `has-external-retraction`
+and `has-retraction` (and their section counterparts, respectively) are
+equivalent, so we content ourselves in showing that there is a logical
+biimplication between them.
+
+```rzk
+#def has-retraction-externalize
+  ( A B : U)
+  ( s : A → B)
+  ( (r , η) : has-retraction A B s)
+  : has-external-retraction A B s
+  :=
+    ( ( A , r)
+    , is-equiv-homotopy A A (\ a → r (s (a))) (identity A)
+      ( η) ( is-equiv-identity A))
+
+#def has-section-externalize
+  ( B A' : U)
+  ( r : B → A')
+  ( (s , ε) : has-section B A' r)
+  : has-external-section B A' r
+  :=
+    ( ( A' , s)
+    , is-equiv-homotopy A' A' (\ a' → r (s (a'))) (identity A')
+      ( ε) ( is-equiv-identity A'))
+
+#def has-retraction-internalize
+  ( A B : U)
+  ( s : A → B)
+  ( ((A' , r) , ( (rec-rs , η-rs) , _))
+    : has-external-retraction A B s)
+  : has-retraction A B s
+  := ( comp B A' A rec-rs r , η-rs)
+
+#def has-section-internalize
+  ( B A' : U)
+  ( r : B → A')
+  ( ((A , s) , (_ , (sec-rs , ε-rs)))
+    : has-external-section B A' r)
+  : has-section B A' r
+  := ( comp A' A B s sec-rs , ε-rs)
+```
+
+A consequence of the above is that in a section-retraction pair `(s, r)`, the
+map `s` is a section and the map `r` is a retraction. Note that not every
+composable pair `(s, r)` of such maps is a section-retraction pair; they have to
+(up to composition with an equivalence) be section and retraction _of each
+other_.
+
+In a section-retraction pair, if one of `s : A → B` and `r : B → A'` is an
+equivalence, then so is the other.
+
+This is just a rephrasing of `is-equiv-left-factor` and `is-equiv-right-factor`.
+
+```rzk
+#section is-equiv-is-section-retraction-pair
+
+#variables A B A' : U
+#variable s : A → B
+#variable r : B → A'
+
+#variable is-sec-rec-pair : is-section-retraction-pair A B A' s r
+
+#def is-equiv-section-is-equiv-retraction-is-section-retraction-pair
+  ( is-equiv-r : is-equiv B A' r)
+  : is-equiv A B s
+  :=
+    is-equiv-right-factor A B A' s r
+    ( is-equiv-r) ( is-sec-rec-pair)
+
+#def is-equiv-retraction-is-equiv-section-is-section-retraction-pair
+  ( is-equiv-s : is-equiv A B s)
+  : is-equiv B A' r
+  :=
+    is-equiv-left-factor A B A'
+    ( s) ( is-equiv-s)
+    ( r) ( is-sec-rec-pair)
+
+#end is-equiv-is-section-retraction-pair
+```
+
+## Retracts
+
+We say that a type `A` is a retract of a type `B` if we have a map `s : A → B`
+which has a retraction.
+
+```rzk title="The type of proofs that A is a retract of B"
+#def is-retract-of
+  ( A B : U)
+  : U
+  := Σ ( s : A → B) , has-retraction A B s
+
+#def section-is-retract-of
+  ( A B : U)
+  ( (s , (_ , _)) : is-retract-of A B)
+  : A → B
+  := s
+
+#def retraction-is-retract-of
+  ( A B : U)
+  ( (_ , (r , _)) : is-retract-of A B)
+  : B → A
+  := r
+
+#def homotopy-is-retract-of
+  ( A B : U)
+  ( (s , (r , η)) : is-retract-of A B)
+  : homotopy A A ( \ a → r ( s a)) ( identity A)
+  := η
+```
+
+Section-retraction pairs `A → B → A'` are a convenient way to exhibit both `A`
+and `A'` as retracts of `B`.
+
+```rzk
+#def is-retract-of-left-section-retraction-pair
+  ( A B A' : U)
+  ( s : A → B)
+  ( r : B → A')
+  ( is-sr-pair-sr : is-section-retraction-pair A B A' s r)
+  : is-retract-of A B
+  :=
+    ( ( s)
+    , ( has-retraction-internalize A B s ((A' , r) , is-sr-pair-sr)))
+
+#def is-retract-of-right-section-retraction-pair
+  ( A B A' : U)
+  ( s : A → B)
+  ( r : B → A')
+  ( is-sr-pair-sr : is-section-retraction-pair A B A' s r)
+  : is-retract-of A' B
+  :=
+    ( first ( has-section-internalize B A' r ((A , s) , is-sr-pair-sr))
+    , ( r
+      , second ( has-section-internalize B A' r ((A , s) , is-sr-pair-sr))))
+```
+
 ## Function extensionality
 
 By path induction, an identification between functions defines a homotopy.
diff --git a/src/hott/06-contractible.rzk.md b/src/hott/06-contractible.rzk.md
index 640c9eef..42f890a1 100644
--- a/src/hott/06-contractible.rzk.md
+++ b/src/hott/06-contractible.rzk.md
@@ -175,39 +175,22 @@ A type is contractible if and only if its terminal map is an equivalence.
 
 A retract of contractible types is contractible.
 
-```rzk title="The type of proofs that A is a retract of B"
-#def is-retract-of
-  ( A B : U)
-  : U
-  := Σ ( s : A → B) , has-retraction A B s
-
-#section retraction-data
+```rzk title="If A is a retract of a contractible type it has a term"
+#section is-contr-is-retract-of-is-contr
 
 #variables A B : U
-#variable is-retract-of-A-B : is-retract-of A B
-
-#def section-is-retract-of
-  : A → B
-  := first is-retract-of-A-B
-
-#def retraction-is-retract-of
-  : B → A
-  := first (second is-retract-of-A-B)
+#variable is-retr-of-A-B : is-retract-of A B
 
-#def homotopy-is-retract-of
-  : homotopy A A (comp A B A retraction-is-retract-of section-is-retract-of) (identity A)
-  := second (second is-retract-of-A-B)
-```
-
-```rzk title="If A is a retract of a contractible type it has a term"
-#def is-inhabited-is-contr-is-retract-of uses (is-retract-of-A-B)
+#def is-inhabited-is-contr-is-retract-of uses (is-retr-of-A-B)
   ( is-contr-B : is-contr B)
   : A
-  := retraction-is-retract-of (center-contraction B is-contr-B)
+  :=
+    retraction-is-retract-of A B is-retr-of-A-B
+    ( center-contraction B is-contr-B)
 ```
 
 ```rzk title="If A is a retract of a contractible type it has a contracting homotopy"
-#def has-homotopy-is-contr-is-retract-of uses (is-retract-of-A-B)
+#def has-homotopy-is-contr-is-retract-of uses (is-retr-of-A-B)
   ( is-contr-B : is-contr B)
   ( a : A)
   : ( is-inhabited-is-contr-is-retract-of is-contr-B) = a
@@ -215,25 +198,33 @@ A retract of contractible types is contractible.
     concat
       ( A)
       ( is-inhabited-is-contr-is-retract-of is-contr-B)
-      ( (comp A B A retraction-is-retract-of section-is-retract-of) a)
+      ( comp A B A
+        ( retraction-is-retract-of A B is-retr-of-A-B)
+        ( section-is-retract-of A B is-retr-of-A-B)
+        ( a))
       ( a)
-      ( ap B A (center-contraction B is-contr-B) (section-is-retract-of a)
-        ( retraction-is-retract-of)
-        ( homotopy-contraction B is-contr-B (section-is-retract-of a)))
-      ( homotopy-is-retract-of a)
+      ( ap B A
+        ( center-contraction B is-contr-B)
+        ( section-is-retract-of A B is-retr-of-A-B a)
+        ( retraction-is-retract-of A B is-retr-of-A-B)
+        ( homotopy-contraction B is-contr-B
+          ( section-is-retract-of A B is-retr-of-A-B a)))
+      ( homotopy-is-retract-of A B is-retr-of-A-B a)
 ```
 
 ```rzk title="If A is a retract of a contractible type it is contractible"
-#def is-contr-is-retract-of-is-contr uses (is-retract-of-A-B)
+#def is-contr-is-retract-of-is-contr uses (is-retr-of-A-B)
   ( is-contr-B : is-contr B)
   : is-contr A
   :=
     ( is-inhabited-is-contr-is-retract-of is-contr-B ,
       has-homotopy-is-contr-is-retract-of is-contr-B)
+
+#end is-contr-is-retract-of-is-contr
 ```
 
 ```rzk
-#end retraction-data
+
 ```
 
 ## Functions between contractible types
diff --git a/src/hott/08-families-of-maps.rzk.md b/src/hott/08-families-of-maps.rzk.md
index cee81ef3..ea235e80 100644
--- a/src/hott/08-families-of-maps.rzk.md
+++ b/src/hott/08-families-of-maps.rzk.md
@@ -287,7 +287,9 @@ equivalence.
   := (family-of-equiv-total-equiv A B C f , total-equiv-family-of-equiv A B C f)
 ```
 
-## Endpoint based path spaces
+## Path spaces
+
+### Based path spaces
 
 ```rzk title="An equivalence between the based path spaces"
 #def equiv-based-paths
@@ -308,6 +310,45 @@ equivalence.
       ( is-contr-based-paths A a)
 ```
 
+### Free path spaces
+
+The canonical map from a type to its the free path type is an equivalence.
+
+```rzk
+#def free-paths
+  ( A : U)
+  : U
+  := Σ ( (x , y) : product A A) , (x = y)
+
+#def constant-free-path
+  ( A : U)
+  ( a : A)
+  : free-paths A
+  := ((a , a) , refl)
+
+#def is-constant-free-path
+  ( A : U)
+  ( ((a , y) , p) : free-paths A)
+  : constant-free-path A a = ((a,y), p)
+  :=
+    ind-path A a
+    ( \ x p' →  constant-free-path A a = ((a , x) , p'))
+    ( refl)
+    ( y) ( p)
+
+#def start-free-path
+  ( A : U)
+  : free-paths A → A
+  := \ ((a , _) , _) → a
+
+#def is-equiv-constant-free-path
+  ( A : U)
+  : is-equiv A (free-paths A) (constant-free-path A)
+  :=
+    ( ( start-free-path A , \ _ → refl)
+    , ( start-free-path A , is-constant-free-path A))
+```
+
 ## Pullback of a type family
 
 A family of types over B pulls back along any function f : A → B to define a
diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 5783d68f..124ebda2 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -458,7 +458,7 @@ In fact, it suffices to assume that the left square has horizontal sections.
 
 ## Fiber products
 
-Given two type families `B C : A → U`, we can form their fiberwise product.
+Given two type families `B C : A → U`, we can form their **fiberwise product**.
 
 ```rzk
 #def fiberwise-product
@@ -483,7 +483,8 @@ Given two type families `B C : A → U`, we can form their fiberwise product.
   := \ (_,c) → c
 ```
 
-Given two maps `B → A` and `C → A`, we can form the relative product over `A`.
+Given two maps `B → A` and `C → A`, we can form the **relative product** over
+`A`.
 
 ```rzk
 #section relative-product
@@ -496,7 +497,7 @@ Given two maps `B → A` and `C → A`, we can form the relative product over `A
 
 #def relative-product
   : U
-  := Σ ( (b, c) : product B C) , β b = γ c
+  := Σ ( (b, c) : product B C) , (β b = γ c)
 
 #def first-relative-product uses (A B β C γ)
   : relative-product → B
@@ -520,7 +521,7 @@ product of all fibers.
   : U
   := total-type A (fiberwise-product A (fib B A β) (fib C A γ))
 
-#def fiber-product-unpacked
+#def unpack-fiber-product
   : fiber-product
   = ( Σ (a : A), (product (fib B A β a) (fib C A γ a)))
   := refl
@@ -586,3 +587,29 @@ product of all fibers.
 
 #end relative-product
 ```
+
+### Fiber product with singleton type
+
+The relative product of `β : B → A` with a map `Unit → A` corresponding to
+`a : A` is nothing but the fiber `fib B A β a`.
+
+```rzk
+#def compute-relative-product-singleton
+  ( A B : U)
+  ( β : B → A)
+  ( a : A)
+  : Equiv-of-maps
+    ( fib B A β a) (Unit) (\ _ → unit)
+    ( relative-product A B β Unit (\ unit → a))
+    ( Unit) ( second-relative-product A B β Unit (\ unit → a))
+  :=
+    ( ( ( ( \ (b , p) → ((b , unit) , p))
+        , ( identity Unit))
+      , \ _ → refl)
+    , ( ( ( ( \ ((b , unit) , p) → (b, p))
+          , ( \ _ → refl))
+        , ( ( \ ((b , unit) , p) → (b, p))
+          , ( \ _ → refl)))
+      , is-equiv-identity Unit))
+
+```
diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index 1af91e74..0cfaf9ec 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -70,8 +70,8 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
   : has-section (extension-type σ) (homotopy-extension-type σ)
       (extension-type-weakening-map σ)
   :=
-    ( extension-strictification σ,
-      \ th → ( second (section-extension-type-weakening' σ th)))
+    ( extension-strictification σ
+    , \ th → ( second (section-extension-type-weakening' σ th)))
 
 
 #def is-equiv-extension-type-weakening
@@ -120,9 +120,7 @@ This equivalence is functorial in the following sense:
       , \ _ → refl
       )
     , ( is-equiv-extension-type-weakening I ψ ϕ A' σ'
-      , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t))
-      )
-    )
+      , is-equiv-extension-type-weakening I ψ ϕ A (\ t → α t (σ' t))))
 ```
 
 ## Commutation of arguments and currying
@@ -1120,7 +1118,7 @@ pointwise.
     ( \ τ → (t : ϕ) → (τ t = σ t))
     ( \ τ →
       equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t)
-      ( \ _ → recBOT) ( \ t → τ t) ( σ))
+      ( \ _ → recBOT) (\ t → τ t) σ)
 
 #def extension-type-pointwise-weakening uses (extext)
   ( σ : (t : ϕ) → A t)
@@ -1157,7 +1155,7 @@ Given a map `α : A' → A`, there is also a notion of relative extension types.
   : U
   :=
     Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
-    , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl]
+    , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
 
 #def relative-extension-type'
   : U
@@ -1207,24 +1205,24 @@ with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`.
     , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t]
 ```
 
-If all ordinary relative extension types are contractible, then also all
-generalized ones.
+If all ordinary relative extension types are contractible, then all generalized
+extension types are also contractible.
 
 ```rzk
 #def has-contr-relative-extension-types
   : U
   :=
-    ( σ' : (t : ϕ) → A' t)
+  ( ( σ' : (t : ϕ) → A' t)
   → ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
-  → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ))
+  → ( is-contr (relative-extension-type I ψ ϕ A' A α σ' τ)))
 
 #def has-contr-general-relative-extension-types
   : U
   :=
-    ( σ' : (t : ϕ) → A' t)
+  ( ( σ' : (t : ϕ) → A' t)
   → ( τ : (t : ψ) → A t)
   → ( h : (t : ϕ) → α t (σ' t) = τ t)
-  → ( is-contr ( general-relative-extension-type σ' τ h))
+  → ( is-contr ( general-relative-extension-type σ' τ h)))
 
 #def has-contr-relative-extension-types-generalize' uses (extext)
   ( has-contr-relext-α : has-contr-relative-extension-types)
diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 5f0ab1f3..0b25eace 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -15,6 +15,7 @@ function extensionality:
 #assume naiveextext : NaiveExtExt
 #assume extext : ExtExt
 #assume funext : FunExt
+#assume weakextext : WeakExtExt
 ```
 
 ## Right orthogonal maps with respect to shapes
@@ -92,8 +93,7 @@ extension types.
         ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
       ( equiv-relative-extension-type-fib extext I ψ ϕ
         ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
-      ( are-contr-relext-α σ' τ)
-    )
+      ( are-contr-relext-α σ' τ))
 
 #def has-contr-relative-extension-types-is-right-orthogonal-to-shape uses (extext)
   ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
@@ -125,7 +125,7 @@ extension types.
   :=
     has-contr-relative-extension-types-generalize extext I ψ ϕ
       ( \ _ → A') (\ _ → A) (\ _ → α)
-    ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α)
+      ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α)
 
 #end has-contr-relative-extension-types-iff-is-right-orthogonal
 ```
@@ -705,59 +705,48 @@ We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`,
 for each `σ : ϕ → A` the type of `ψ`-extensions is contractible.
 
 ```rzk
+#section has-unique-extensions
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variable A : U
+
 #def has-unique-extensions
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A : U)
   : U
   := ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t])
 ```
 
-The property of having unique extension can be pulled back along any right
-orthogonal map.
+There are other equivalent characterizations which we shall prove below:
+
+We can ask that the canonical restriction map `(ψ → A) → (ϕ → A)` is an
+equivalence.
 
 ```rzk
-#def has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
-  ( A' A : U)
-  ( α : A' → A)
-  ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
-  : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A'
+#def is-local-type
+  : U
   :=
-    \ has-ue-A ( σ' : ϕ → A') →
-      is-contr-equiv-is-contr'
-        ( ( t : ψ) → A' [ϕ t ↦ σ' t])
-        ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
-        ( \ τ' t → α (τ' t) , is-orth-ψ-ϕ-α σ')
-        ( has-ue-A (\ t → α (σ' t)))
+    is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
 ```
 
-Alternatively, we can ask that the canonical restriction map `(ψ → A) → (ϕ → A)`
-is an equivalence.
+We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`
 
 ```rzk
-#section is-local-type
-#variable I : CUBE
-#variable ψ : I → TOPE
-#variable ϕ : ψ → TOPE
-#variable A : U
-
-#def is-local-type
+#def is-right-orthogonal-to-shape-terminal-map
   : U
   :=
-    is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
+    is-right-orthogonal-to-shape I ψ ϕ A Unit (terminal-map A)
 ```
 
-This follows straightforwardly from the fact that for every `σ : ϕ → A` we have
-an equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]` and the
-fiber of the restriction map `(ψ → A) → (ϕ → A)`.
+### Proof of first alternative characterization
+
+The equivalence between `is-local-type` and `has-unique-extensions` follows
+straightforwardly from the fact that for every `σ : ϕ → A` we have an
+equivalence between the extension type `(t : ψ) → A [ϕ t ↦ σ t]` and the fiber
+of the restriction map `(ψ → A) → (ϕ → A)`.
 
 ```rzk
 #def is-local-type-has-unique-extensions
-  ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
+  ( has-ue-ψ-ϕ-A : has-unique-extensions)
   : is-local-type
   :=
     is-equiv-is-contr-map (ψ → A) (ϕ → A) ( \ τ t → τ t)
@@ -770,7 +759,7 @@ fiber of the restriction map `(ψ → A) → (ϕ → A)`.
 
 #def has-unique-extensions-is-local-type
   ( is-lt-ψ-ϕ-A : is-local-type)
-  : has-unique-extensions I ψ ϕ A
+  : has-unique-extensions
   :=
     \ σ →
       is-contr-equiv-is-contr'
@@ -782,17 +771,69 @@ fiber of the restriction map `(ψ → A) → (ϕ → A)`.
             ( is-lt-ψ-ϕ-A)
             ( σ))
 
-#end is-local-type
+#end has-unique-extensions
+```
+
+### Properties of local types / unique extension types
+
+We fix a shape inclusion `ϕ ⊂ ψ`.
+
+```rzk
+#section stability-properties-local-types
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
 ```
 
-Since the property of having unique extensions passes from the codomain to the
-domain of a right orthogonal map, the same is true for locality of types.
+Every map between types with unique extensions / local types is right
+orthogonal.
 
 ```rzk
-#def is-local-type-domain-right-orthogonal-is-local-type-codomain
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( ϕ : ψ → TOPE)
+#def is-right-orthogonal-have-unique-extensions
+  ( A' A : U)
+  ( has-ue-ψ-ϕ-A' : has-unique-extensions I ψ ϕ A')
+  ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
+  ( α : A' → A)
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    \ σ →
+      is-equiv-are-contr
+      ( extension-type I ψ ϕ (\ _ → A') (σ))
+      ( extension-type I ψ ϕ (\ _ → A) (\ t → α (σ t)))
+      ( has-ue-ψ-ϕ-A' σ)
+      ( has-ue-ψ-ϕ-A (\ t → α (σ t)))
+      ( \ τ t → α (τ t))
+
+#def is-right-orthogonal-are-local-types
+  ( A' A : U)
+  ( is-lt-ψ-ϕ-A' : is-local-type I ψ ϕ A')
+  ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
+  : ( α : A' → A)
+  → is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    is-right-orthogonal-have-unique-extensions A' A
+    ( has-unique-extensions-is-local-type I ψ ϕ A' is-lt-ψ-ϕ-A')
+    ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
+```
+
+Conversely, the property of having unique extension can be pulled back along any
+right orthogonal map.
+
+```rzk
+#def has-unique-extensions-right-orthogonal-has-unique-extensions
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A'
+  :=
+    \ has-ue-A ( σ' : ϕ → A') →
+      is-contr-equiv-is-contr'
+        ( ( t : ψ) → A' [ϕ t ↦ σ' t])
+        ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
+        ( \ τ' t → α (τ' t) , is-orth-ψ-ϕ-α σ')
+        ( has-ue-A (\ t → α (σ' t)))
+
+#def is-local-type-right-orthogonal-is-local-type
   ( A' A : U)
   ( α : A' → A)
   ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
@@ -800,8 +841,78 @@ domain of a right orthogonal map, the same is true for locality of types.
   : is-local-type I ψ ϕ A'
   :=
     is-local-type-has-unique-extensions I ψ ϕ A'
-      ( has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
-          I ψ ϕ A' A α is-orth-α
+      ( has-unique-extensions-right-orthogonal-has-unique-extensions
+          ( A') ( A) ( α) ( is-orth-α)
           ( has-unique-extensions-is-local-type I ψ ϕ A is-local-A))
+```
+
+Weak extension extensionality says that every contractible type has unique
+extensions for every shape inclusion `ϕ ⊂ ψ`.
+
+```rzk
+#def has-unique-extensions-is-contr uses (weakextext)
+  ( C : U)
+  ( is-contr-C : is-contr C)
+  : has-unique-extensions I ψ ϕ C
+  :=
+    weakextext I ψ ϕ
+    ( \ _ → C) ( \ _ → is-contr-C)
+
+#def has-unique-extensions-Unit uses (weakextext)
+  : has-unique-extensions I ψ ϕ Unit
+  := has-unique-extensions-is-contr Unit is-contr-Unit
+
+#end stability-properties-local-types
+```
+
+### Proof of second alternative characterization
+
+Next we prove the logical equivalence between `has-unique-extensions` and
+`is-right-orthogonal-to-shape-terminal-map`. This follows directly from the fact
+that `Unit` has unique extensions (using `weakextext : WeakExtExt`).
+
+```rzk
+#section is-right-orthogonal-to-shape-terminal-map
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variable A : U
+
+#def has-unique-extensions-is-right-orthogonal-to-shape-terminal-map
+  uses (weakextext)
+  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A)
+  : has-unique-extensions I ψ ϕ A
+  :=
+    has-unique-extensions-right-orthogonal-has-unique-extensions
+      I ψ ϕ A Unit (terminal-map A)
+    ( is-orth-ψ-ϕ-tm-A)
+    ( has-unique-extensions-Unit I ψ ϕ)
+
+#def is-right-orthogonal-to-shape-terminal-map-has-unique-extensions
+  uses (weakextext)
+  ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
+  : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A
+  :=
+    is-right-orthogonal-have-unique-extensions I ψ ϕ A Unit
+    ( has-ue-ψ-ϕ-A) ( has-unique-extensions-Unit I ψ ϕ)
+    ( terminal-map A)
+
+#def is-right-orthogonal-to-shape-terminal-map-is-local-type
+  uses (weakextext)
+  ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
+  : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A
+  :=
+    is-right-orthogonal-to-shape-terminal-map-has-unique-extensions
+    ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
+
+#def is-local-type-is-right-orthogonal-to-shape-terminal-map
+  uses (weakextext)
+  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A)
+  : is-local-type I ψ ϕ A
+  :=
+    is-local-type-has-unique-extensions I ψ ϕ A
+    ( has-unique-extensions-is-right-orthogonal-to-shape-terminal-map
+      ( is-orth-ψ-ϕ-tm-A))
 
+#end is-right-orthogonal-to-shape-terminal-map
 ```
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index e343f965..ed74e32c 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -216,6 +216,66 @@ Extension types are also used to define the type of commutative triangles:
         t₂ ≡ t₁ ↦ h t₂]   -- the diagonal is exactly `h`
 ```
 
+## Arrow types
+
+We define the arrow type:
+
+```rzk
+#def arr
+  ( A : U)
+  : U
+  := Δ¹ → A
+```
+
+For later convenience we give an alternative characterizations of the arrow
+type.
+
+```rzk
+#def fibered-arr
+  ( A : U)
+  : U
+  := Σ (x : A) , (Σ (y : A) , hom A x y)
+
+#def fibered-arr-free-arr
+  ( A : U)
+  : arr A → fibered-arr A
+  := \ k → (k 0₂ , (k 1₂ , k))
+
+#def is-equiv-fibered-arr-free-arr
+  ( A : U)
+  : is-equiv (arr A) (fibered-arr A) (fibered-arr-free-arr A)
+  :=
+    ( ( (\ (_ , (_ , f)) → f) , (\ _ → refl))
+    , ( (\ (_ , (_ , f)) → f) , (\ _ → refl)))
+
+#def equiv-fibered-arr-free-arr
+  ( A : U)
+  : Equiv (arr A) (fibered-arr A)
+  := (fibered-arr-free-arr A , is-equiv-fibered-arr-free-arr A)
+```
+
+And the corresponding uncurried version.
+
+```rzk
+#def fibered-arr'
+  ( A : U)
+  : U
+  :=
+    Σ ((a,b) : product A A), hom A a b
+
+#def fibered-arr-free-arr'
+  ( A : U)
+  : arr A → fibered-arr' A
+  := \ σ → ((σ 0₂ , σ 1₂) , σ)
+
+#def is-equiv-fibered-arr-free-arr'
+  ( A : U)
+  : is-equiv (arr A) (fibered-arr' A) (fibered-arr-free-arr' A)
+  :=
+    ( ( (\ ((_ , _) , σ) → σ) , (\ _ → refl))
+    , ( (\ ((_ , _) , σ) → σ) , (\ _ → refl)))
+```
+
 ## The Segal condition
 
 A type is **Segal** if every composable pair of arrows has a unique composite.
@@ -624,36 +684,7 @@ then $(x : X) → A x$ is a Segal type.
         ( \ s → is-local-horn-inclusion-is-segal (A s)(fiberwise-is-segal-A s)))
 ```
 
-In particular, the arrow type of a Segal type is Segal. First, we define the
-arrow type:
-
-```rzk
-#def arr
-  ( A : U)
-  : U
-  := Δ¹ → A
-```
-
-For later use, an equivalent characterization of the arrow type.
-
-```rzk
-#def arr-Σ-hom
-  ( A : U)
-  : ( arr A) → (Σ (x : A) , (Σ (y : A) , hom A x y))
-  := \ f → (f 0₂ , (f 1₂ , f))
-
-#def is-equiv-arr-Σ-hom
-  ( A : U)
-  : is-equiv (arr A) (Σ (x : A) , (Σ (y : A) , hom A x y)) (arr-Σ-hom A)
-  :=
-    ( ( \ (x , (y , f)) → f , \ f → refl) ,
-      ( \ (x , (y , f)) → f , \ xyf → refl))
-
-#def equiv-arr-Σ-hom
-  ( A : U)
-  : Equiv (arr A) (Σ (x : A) , (Σ (y : A) , hom A x y))
-  := ( arr-Σ-hom A , is-equiv-arr-Σ-hom A)
-```
+In particular, the arrow type of a Segal type is Segal.
 
 ```rzk title="RS17, Corollary 5.6(ii), special case for locality at the horn inclusion"
 #def is-local-horn-inclusion-arr uses (extext)
@@ -912,17 +943,16 @@ The `#!rzk witness-square-comp-is-segal` as an arrow in the arrow type:
   ( g : hom A x y)
   ( h : hom A y z)
   : hom2 (arr A) f g h
-      (arr-in-arr-is-segal A is-segal-A w x y f g)
-      (arr-in-arr-is-segal A is-segal-A x y z g h)
-      (comp-is-segal (arr A) (is-segal-arr A is-segal-A)
-      f g h
-      (arr-in-arr-is-segal A is-segal-A w x y f g)
-      (arr-in-arr-is-segal A is-segal-A x y z g h))
+      ( arr-in-arr-is-segal A is-segal-A w x y f g)
+      ( arr-in-arr-is-segal A is-segal-A x y z g h)
+      ( comp-is-segal (arr A) (is-segal-arr A is-segal-A) f g h
+        ( arr-in-arr-is-segal A is-segal-A w x y f g)
+        ( arr-in-arr-is-segal A is-segal-A x y z g h))
   :=
     witness-comp-is-segal
       ( arr A)
       ( is-segal-arr A is-segal-A)
-      f g h
+      ( f) ( g) ( h)
       ( arr-in-arr-is-segal A is-segal-A w x y f g)
       ( arr-in-arr-is-segal A is-segal-A x y z g h)
 ```
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index 89aee5d3..b6ad3789 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -237,50 +237,40 @@ Discrete types are automatically Segal types.
         ( ( \ σ t s → (second (second σ)) (t , s)) , (\ σ → refl))))
 ```
 
-The equivalence underlying `#!rzk equiv-arr-Σ-hom`:
-
 ```rzk
-#def fibered-arr-free-arr
-  : (arr A) → (Σ (u : A) , (Σ (v : A) , hom A u v))
-  := \ k → (k 0₂ , (k 1₂ , k))
-
-#def is-equiv-fibered-arr-free-arr
-  : is-equiv (arr A) (Σ (u : A) , (Σ (v : A) , hom A u v)) (fibered-arr-free-arr)
-  := is-equiv-arr-Σ-hom A
-
 #def is-equiv-ap-fibered-arr-free-arr uses (w x y z)
   : is-equiv
       ( f =_{Δ¹ → A} g)
-      ( fibered-arr-free-arr f = fibered-arr-free-arr g)
+      ( fibered-arr-free-arr A f = fibered-arr-free-arr A g)
       ( ap
         ( arr A)
         ( Σ (u : A) , (Σ (v : A) , (hom A u v)))
         ( f)
         ( g)
-        ( fibered-arr-free-arr))
+        ( fibered-arr-free-arr A))
   :=
     is-emb-is-equiv
       ( arr A)
       ( Σ (u : A) , (Σ (v : A) , (hom A u v)))
-      ( fibered-arr-free-arr)
-      ( is-equiv-fibered-arr-free-arr)
+      ( fibered-arr-free-arr A)
+      ( is-equiv-fibered-arr-free-arr A)
       ( f)
       ( g)
 
 #def equiv-eq-fibered-arr-eq-free-arr uses (w x y z)
-  : Equiv (f =_{Δ¹ → A} g) (fibered-arr-free-arr f = fibered-arr-free-arr g)
+  : Equiv (f =_{Δ¹ → A} g) (fibered-arr-free-arr A f = fibered-arr-free-arr A g)
   :=
     equiv-ap-is-equiv
       ( arr A)
       ( Σ (u : A) , (Σ (v : A) , (hom A u v)))
-      ( fibered-arr-free-arr)
-      ( is-equiv-fibered-arr-free-arr)
+      ( fibered-arr-free-arr A)
+      ( is-equiv-fibered-arr-free-arr A)
       ( f)
       ( g)
 
 #def equiv-sigma-over-product-hom-eq
   : Equiv
-      ( fibered-arr-free-arr f = fibered-arr-free-arr g)
+      ( fibered-arr-free-arr A f = fibered-arr-free-arr A g)
       ( Σ ( p : x = z) ,
           ( Σ ( q : y = w) ,
               ( product-transport A A (hom A) x z y w p q f = g)))
@@ -288,8 +278,8 @@ The equivalence underlying `#!rzk equiv-arr-Σ-hom`:
     extensionality-Σ-over-product
       ( A) (A)
       ( hom A)
-      ( fibered-arr-free-arr f)
-      ( fibered-arr-free-arr g)
+      ( fibered-arr-free-arr A f)
+      ( fibered-arr-free-arr A g)
 
 #def equiv-square-sigma-over-product uses (extext is-discrete-A)
   : Equiv
@@ -318,7 +308,7 @@ The equivalence underlying `#!rzk equiv-arr-Σ-hom`:
                     (Δ¹ t) ∧ (s ≡ 1₂) ↦ k t])))
       ( equiv-comp
         ( f =_{Δ¹ → A} g)
-        ( fibered-arr-free-arr f = fibered-arr-free-arr g)
+        ( fibered-arr-free-arr A f = fibered-arr-free-arr A g)
         ( Σ ( p : x = z) ,
             ( Σ ( q : y = w) ,
                 ( product-transport A A (hom A) x z y w p q f = g)))
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 3366ba3a..ad6c8bc4 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -415,7 +415,7 @@ type, then so is `A'`.
   : is-segal A'
   :=
     is-segal-is-local-horn-inclusion A'
-      ( is-local-type-domain-right-orthogonal-is-local-type-codomain
+      ( is-local-type-right-orthogonal-is-local-type
         ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α
         ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α)
         ( is-local-horn-inclusion-is-segal A is-segal-A))
@@ -593,12 +593,6 @@ Finally, we deduce the theorem by some straightforward logical bookkeeping.
 
 ## Total type of a covariant family over a Segal type
 
-We prove that the total type of a covariant family over a Segal type is a Segal
-type. We split the proof into intermediate steps. Let `A` be a type and a type
-family `#!rzk C : A → U`.
-
-### Category theoretic proof
-
 For every covariant family `C : A → U`, the projection `Σ A, C → A` is an left
 fibration, hence an inner fibration. It immediately follows that if `A` is
 Segal, then so is `Σ A, C`.
@@ -617,63 +611,6 @@ Segal, then so is `Σ A, C`.
             ( is-naive-left-fibration-is-covariant A C is-covariant-C))
 ```
 
-### Type theoretic proof
-
-We examine the fibers of the horn restriction on the total type of `C`. First
-note we have the equivalences:
-
-```rzk
-#def apply-4-3
-  ( A : U )
-  ( C : A → U )
-  : Equiv
-    ( Λ → (Σ ( a : A ), C a ) )
-    ( Σ ( f : Λ → A ), ( t : Λ ) → ( C ( f t ) ) )
-  :=
-    axiom-choice ( 2 × 2 ) Λ ( \ t → BOT ) ( \ t → A )
-    ( \ t a → C a ) ( \ t → recBOT ) ( \ t → recBOT )
-
-#def apply-4-3-again
-  ( A : U )
-  ( C : A → U )
-  : Equiv
-    ( Δ² → (Σ ( a : A ), C a ) )
-    ( Σ ( f : Δ² → A ), ( t : Δ² ) → ( C ( f t ) ) )
-  :=
-    axiom-choice ( 2 × 2 ) Δ² ( \ t → BOT ) ( \ t → A )
-    ( \ t a → C a ) ( \ t → recBOT ) ( \ t → recBOT )
-```
-
-We show that the induced map between this types is an equivalence. First we
-exhibit the map:
-
-```rzk
-#def total-inner-horn-restriction
-  ( A : U )
-  ( C : A → U )
-  : ( Σ ( f : Δ² → A ), ( t : Δ² ) → ( C ( f t ) ) ) →
-    ( Σ ( g : Λ → A ), ( t : Λ ) → ( C ( g t ) ) )
-  := \ ( f, μ ) → ( \ t → f t , \ t → μ t)
-```
-
-Next we compute the fibers of this map by showing the equivalence as claimed in
-the proof of Theorem 8.8 in RS17. The following maps will be packed into some
-`#!rzk Equiv`.
-
-```rzk
-#def map-to-total-inner-horn-restriction-fiber
-  ( A : U )
-  ( C : A → U )
-  ( (g , φ) : ( Σ ( k : Λ → A ), ( t : Λ ) → C ( k t ) ) )
-  : ( Σ (h : (t : Δ²) → A [ Λ t ↦ g t ] ) ,
-      (( t : Δ² ) → C (h t) [ Λ t ↦ φ t])) →
-    ( fib ( Σ ( l : Δ² → A ), ( t : Δ² ) → ( C ( l t ) ))
-          ( Σ ( k : Λ → A ), ( t : Λ ) → ( C ( k t ) ))
-          ( total-inner-horn-restriction A C )
-          ( g,  φ) )
-  := \ ( f,μ ) → ( ( \ t → f t, \ t → μ t  ), refl )
-```
-
 ## Representable covariant families
 
 If `A` is a Segal type and `a : A` is any term, then `hom A a` defines a