diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index a1f238ef..cb78073c 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -533,6 +533,50 @@ 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
+#section is-section-retraction-pair
+
+#variables A' B A : U
+#variable s : A' → B
+#variable r : B → A
+
+
+#def is-section-retraction-pair
+  : U
+  := is-equiv A' A (comp A' B A r s)
+```
+
+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
+#variable is-sec-rec-pair : is-section-retraction-pair
+
+#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-section-retraction-pair
+```
+
 ## Function extensionality
 
 By path induction, an identification between functions defines a homotopy.
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/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)))