diff --git a/src/hott/02-homotopies.rzk.md b/src/hott/02-homotopies.rzk.md
index 1881dde8..1e55da48 100644
--- a/src/hott/02-homotopies.rzk.md
+++ b/src/hott/02-homotopies.rzk.md
@@ -132,6 +132,27 @@ $K^{-1} \cdot H  \sim \text{refl-htpy}_{g}$
       g
 ```
 
+## Composition of equal maps
+
+```rzk
+
+#def comp-homotopic-maps
+  ( A B C : U)
+  ( f g : A → B)
+  ( h k : B → C)
+  ( p : f = g)
+  ( q : h = k)
+  : comp A B C h f = comp A B C k g
+  :=
+    ind-path (A → B) f (\ g' p' → comp A B C h f = comp A B C k g')
+    ( ind-path (B → C) h (\ k' q' → comp A B C h f = comp A B C k' f)
+      ( refl)
+      ( k)
+      ( q))
+    ( g)
+    ( p)
+```
+
 ## Naturality
 
 ```rzk title="The naturality square associated to a homotopy and a path"
diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index 05beb96b..c31a2198 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -813,6 +813,28 @@ identifications. This defines `#!rzk eq-htpy` to be the retraction to
   ( f g : (x : X) → A x)
   : ((x : X) → f x = g x) → (f = g)
   := first (first (funext X A f g))
+
+#def left-cancel-is-equiv uses (funext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  : (comp A B A (π₁ (π₁ is-equiv-f)) f) = (identity A)
+  :=
+    eq-htpy A (\ x' → A)
+    ( comp A B A (π₁ (π₁ is-equiv-f)) f)
+    ( identity A)
+    ( π₂ (π₁ is-equiv-f))
+
+#def right-cancel-is-equiv uses (funext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  : (comp B A B f (π₁ (π₂ is-equiv-f))) = (identity B)
+  :=
+    eq-htpy B (\ x' → B)
+    ( comp B A B f (π₁ (π₂ is-equiv-f)))
+    ( identity B)
+    ( π₂ (π₂ is-equiv-f))
 ```
 
 Using function extensionality, a fiberwise equivalence defines an equivalence of
diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index 82e04f45..d973037d 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -10,10 +10,8 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-- `hott/4-equivalences.rzk` — contains the definitions of `#!rzk Equiv` and
+- `hott/03-equivalences.rzk.md` — contains the definitions of `#!rzk Equiv` and
   `#!rzk comp-equiv`
-- the file `hott/4-equivalences.rzk` relies in turn on the previous files in
-  `hott/`
 
 ## Extension up to homotopy
 
@@ -356,6 +354,25 @@ For each of these we provide a corresponding functorial instance
       ( ( \ 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)))
+
+#def inv-equiv-axiom-choice
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( X : ψ → U)
+  ( Y : (t : ψ) → (x : X t) → U)
+  ( a : (t : ϕ) → X t)
+  ( b : (t : ϕ) → Y t (a t))
+  : Equiv
+    ( Σ ( f : ((t : ψ) → X t [ϕ t ↦ a t]))
+      , ( (t : ψ) → Y t (f t) [ϕ t ↦ b t]))
+    ( (t : ψ) → (Σ (x : X t) , Y t x) [ϕ t ↦ (a t , b t)])
+  :=
+    inv-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]))
+    ( axiom-choice I ψ ϕ X Y a b)
 ```
 
 ## Composites and unions of cofibrations
@@ -1185,39 +1202,70 @@ Given a map `α : A' → A`, there is also a notion of relative extension types.
 #variable I : CUBE
 #variable ψ : I → TOPE
 #variable ϕ : ψ → TOPE
-#variables A' A : ψ → U
-#variable α : (t : ψ) → A' t → A t
-#variable σ' : (t : ϕ) → A' t
-#variable τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]
+#variables A B : ψ → U
+#variable f : (t : ψ) → A t → B t
+#variable a : (t : ϕ) → A t
+#variable τ : (t : ψ) → B t [ϕ t ↦ f t (a t)]
 
 #def relative-extension-type
   : U
   :=
-    Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
-    , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
+    Σ ( τ' : (t : ψ) → A t [ϕ t ↦ a t])
+    , ( ( t : ψ) → (f t (τ' t) = τ t) [ϕ t ↦ refl])
+```
 
-#def relative-extension-type'
+This is equivalently expressed as the fibers of postcomposition by $f$.
+
+```rzk
+#def postcomp-Π-ext
+  : ((t : ψ) → A t [ϕ t ↦ a t]) →
+    ((t : ψ) → B t [ϕ t ↦ f t (a t)])
+  := ( \ τ' t → f t (τ' t))
+
+#def fiber-postcomp-Π-ext
   : U
   :=
     fib
-    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
-    ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
-    ( \ τ' t → α t (τ' t))
+    ( (t : ψ) → A t [ϕ t ↦ a t])
+    ( (t : ψ) → B t [ϕ t ↦ f t (a t)])
+    ( postcomp-Π-ext)
     ( τ)
 
 #def equiv-relative-extension-type-fib uses (extext)
   : Equiv
-    ( relative-extension-type')
+    ( fiber-postcomp-Π-ext)
     ( relative-extension-type)
   :=
     total-equiv-family-of-equiv
-    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
-    ( \ τ' → (\ t → α t (τ' t)) =_{ (t : ψ) → A t [ϕ t ↦ α t (σ' t)]} τ)
-    ( \ τ' → (t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
+    ( (t : ψ) → A t [ϕ t ↦ a t])
+    ( \ τ' → (\ t → f t (τ' t)) =_{ (t : ψ) → B t [ϕ t ↦ f t (a t)]} τ)
+    ( \ τ' → (t : ψ) → (f t (τ' t) = τ t) [ϕ t ↦ refl])
     ( \ τ' →
-      equiv-ExtExt extext I ψ ϕ A
-      ( \ t → α t (σ' t))
-      ( \ t → α t (τ' t)) ( τ))
+      equiv-ExtExt extext I ψ ϕ B
+      ( \ t → f t (a t))
+      ( \ t → f t (τ' t)) ( τ))
+```
+
+The fiber of postcomposition by a map $f: \prod_{t : I|\psi} A (t) \to B (t)$ is
+equivalent to the family of fibers of $f\_t$.
+
+```rzk
+#def fiber-family-ext
+  : U
+  := (t : ψ) → fib (A t) (B t) (f t) (τ t) [ϕ t ↦ (a t, refl)]
+
+#def equiv-fiber-postcomp-Π-ext-fiber-family-ext uses (extext)
+  : Equiv
+    ( fiber-postcomp-Π-ext)
+    ( fiber-family-ext)
+  :=
+    equiv-comp
+    ( fiber-postcomp-Π-ext)
+    ( relative-extension-type)
+    ( fiber-family-ext)
+    ( equiv-relative-extension-type-fib)
+    ( inv-equiv-axiom-choice I ψ ϕ A (\ t x → f t x = τ t) a (\ t → refl))
+
 #end relative-extension-types
 ```
 
@@ -1345,9 +1393,7 @@ We can view it as a map of maps either vertically or horizontally.
     ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
     ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
   :=
-    ( ( ( \ a t → f t (a t))
-      , ( \ a t → f t (a t)))
-    , \ _ → refl)
+    ( ( (\ a t → f t (a t)), (\ a t → f t (a t))), \ _ → refl)
 
 #def map-of-map-extension-type
   ( I : CUBE)
@@ -1359,74 +1405,52 @@ We can view it as a map of maps either vertically or horizontally.
     ( (t : ψ) → A t) ( (t : ψ) → B t) (\ a t → f t (a t))
     ( (t : ϕ) → A t) ( (t : ϕ) → B t) (\ a t → f t (a t))
   :=
-    ( ( ( \ a t → a t)
-      , ( \ b t → b t))
-    , \ _ → refl)
+    ( ( (\ a t → a t), (\ b t → b t)), \ _ → refl)
 ```
 
 ### Equivalences induce equivalences of extension types
 
-We start by treating the case of extensions from the empty shape `BOT`.
-
-It follows from extension extensionality that if `f : A → B` is an equivalence,
-then so is the map of maps `map-of-restriction-maps`.
+If $f: \prod_{t : I|\psi} A (t) \to B (t)$ is a family of equivalence then the
+fibers of postcomposition by $f$ are contractible.
 
 ```rzk
-#def is-equiv-extensions-BOT-is-equiv uses (extext)
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( A B : ψ → U)
-  ( f : (t : ψ) → (A t) → (B t))
-  ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
-  : 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 →
-            naiveextext-extext extext I ψ ( \ t → BOT)
-              ( A)
-              ( \ u → recBOT)
-              ( \ t → first (first (is-equiv-f t)) (f t (a t)))
-              ( a)
-              ( \ t → second (first (is-equiv-f t)) (a t))))
-      , ( ( \ b t → first (second (is-equiv-f t)) (b t))
-        , ( \ b →
-            naiveextext-extext extext I ψ ( \ t → BOT)
-              ( B)
-              ( \ u → recBOT)
-              ( \ t → f t (first (second (is-equiv-f t)) (b t)))
-              ( b)
-              ( \ t → second (second (is-equiv-f t)) (b t)))))
-
-#def equiv-extensions-BOT-equiv uses (extext)
+
+#def is-contr-fiber-family-ext-contr-fib
   ( I : CUBE)
   ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
   ( A B : ψ → U)
-  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
-  : Equiv ((t : ψ) → A t) ((t : ψ) → B t)
+  ( f : (t : ψ) → A t → B t)
+  ( a : (t : ϕ) → A t)
+  ( τ : (t : ψ) → B t [ϕ t ↦ f t (a t)])
+  ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
+  : is-contr (fiber-family-ext I ψ ϕ A B f a τ)
   :=
-    ( ( \ a t → first ( famequiv t) (a t))
-    , is-equiv-extensions-BOT-is-equiv I ψ A B
-      ( \ t → first (famequiv t))
-      ( \ t → second (famequiv t)))
+    (weakextext-extext extext) I ψ ϕ
+    ( \ t → fib (A t) (B t) (f t) (τ t))
+    ( \ t → is-contr-map-is-equiv (A t) (B t) (f t) (family-equiv-f t) (τ t))
+    ( \ t → (a t, refl))
 
-#def equiv-of-restriction-maps-equiv uses (extext)
+#def is-contr-fiber-postcomp-Π-ext-is-equiv-fam uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
   ( A B : ψ → U)
-  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
-  : Equiv-of-maps
-    ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
-    ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
-  :=
-    ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t))
-    , ( second (equiv-extensions-BOT-equiv I ψ A B famequiv)
-      , second ( equiv-extensions-BOT-equiv I
-                 (\ t → ϕ t) (\ t → A t) (\ t → B t) (\ t → famequiv t))))
+  ( f : (t : ψ) → A t → B t)
+  ( a : (t : ϕ) → A t)
+  ( τ : (t : ψ) → B t [ϕ t ↦ f t (a t)])
+  ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
+  : is-contr (fiber-postcomp-Π-ext I ψ ϕ A B f a τ)
+  :=
+    is-contr-equiv-is-contr'
+    ( fiber-postcomp-Π-ext I ψ ϕ A B f a τ)
+    ( fiber-family-ext I ψ ϕ A B f a τ)
+    ( equiv-fiber-postcomp-Π-ext-fiber-family-ext I ψ ϕ A B f a τ)
+    ( is-contr-fiber-family-ext-contr-fib I ψ ϕ A B f a τ family-equiv-f)
 ```
 
-Now we use the result for extensions of `BOT` to bootstrap to arbitrary
-extensions. We show that an equivalence `f : A → B` induces an equivalence of
-all extension types, not just those extended from `BOT`.
+Hence, postcomposing with an equivalence induces an equivalence of extension
+types.
 
 ```rzk
 #def is-equiv-extensions-is-equiv uses (extext)
@@ -1435,31 +1459,19 @@ all extension types, not just those extended from `BOT`.
   ( ϕ : ψ → TOPE)
   ( A B : ψ → U)
   ( f : (t : ψ) → A t → B t)
-  ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
-  : ( a : (t : ϕ) → A t)
-  → is-equiv
+  ( a : (t : ϕ) → A t)
+  ( family-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
+  : is-equiv
     ( (t : ψ) → A t [ϕ t ↦ a t])
     ( (t : ψ) → B t [ϕ t ↦ f t (a t)])
-    ( \ a' t → f t (a' t))
+    ( postcomp-Π-ext I ψ ϕ A B f a)
   :=
-    is-homotopy-cartesian-is-horizontal-equiv
-    ( (t : ϕ) → A t)
-    ( \ a → (t : ψ) → A t [ϕ t ↦ a t])
-    ( (t : ϕ) → B t)
-    ( \ b → (t : ψ) → B t [ϕ t ↦ b t])
-    ( \ a t → f t (a t))
-    ( \ _ a' t → f t (a' t))
-    ( is-equiv-extensions-BOT-is-equiv
-      ( I) (\ t → ϕ t) (\ t → A t) (\ t → B t) ( \ t → f t)
-      ( \ (t : ϕ) → is-equiv-f t))
-    ( is-equiv-Equiv-is-equiv'
-        ( (t : ψ) → A t) ((t : ψ) → B t) (\ a' t → f t (a' t))
-        ( Σ (a : (t : ϕ) → A t) , ((t : ψ) → A t [ϕ t ↦ a t]))
-        ( Σ (b : (t : ϕ) → B t) , ((t : ψ) → B t [ϕ t ↦ b t]))
-        ( \ (a , a') → ( \ t → f t (a t) , \ t → f t (a' t)))
-      ( cofibration-composition-functorial
-        I ψ ϕ (\ _ → BOT) A B f (\ _ → recBOT))
-      ( is-equiv-extensions-BOT-is-equiv I ψ A B f is-equiv-f))
+    is-equiv-is-contr-map
+    ( (t : ψ) → A t [ϕ t ↦ a t])
+    ( (t : ψ) → B t [ϕ t ↦ f t (a t)])
+    ( postcomp-Π-ext I ψ ϕ A B f a)
+    ( \ τ →
+      is-contr-fiber-postcomp-Π-ext-is-equiv-fam I ψ ϕ A B f a τ family-equiv-f)
 
 #def equiv-extensions-equiv uses (extext)
   ( I : CUBE)
@@ -1472,11 +1484,31 @@ all extension types, not just those extended from `BOT`.
     ( (t : ψ) → A t [ϕ t ↦ a t])
     ( (t : ψ) → B t [ϕ t ↦ first (equivs-A-B t) (a t)])
   :=
-  ( ( \ a' t → first (equivs-A-B t) (a' t))
-  , ( is-equiv-extensions-is-equiv I ψ ϕ A B
+    ( postcomp-Π-ext I ψ ϕ A B (\ t → (first (equivs-A-B t))) a
+    , is-equiv-extensions-is-equiv I ψ ϕ A B
       ( \ t → first (equivs-A-B t))
-      ( \ t → second (equivs-A-B t))
-      ( a)))
+      ( a)
+      ( \ t → second (equivs-A-B t)))
+
+#def equiv-of-restriction-maps-equiv uses (extext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
+  : Equiv-of-maps
+    ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
+    ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
+  :=
+    ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t))
+    , ( second (equiv-extensions-equiv I ψ ( \ _ → BOT)
+      ( A) ( B)
+      ( famequiv)
+      ( \ _ → recBOT))
+      , second ( equiv-extensions-equiv I ( \ t → ϕ t) ( \ _ → BOT)
+        ( \ t → A t) ( \ t → B t)
+        ( \ t → famequiv t)
+        ( \ _ → recBOT))))
 ```
 
 ### Retracts induce retracts of extension types
@@ -1508,8 +1540,9 @@ working with external retractions.
   :=
     is-equiv-extensions-is-equiv I ψ ϕ A A
     ( \ t a₀ → r t (s t (a₀)))
-    ( \ t → is-equiv-retraction-section (A t) (B t) (s t) (r t) (η t))
     ( a)
+    ( \ t → is-equiv-retraction-section (A t) (B t) (s t) (r t) (η t))
+
 
 #def has-retraction-extensions-has-retraction' uses (extext η)
   ( a : (t : ϕ) → A t)
diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index ff1ed87d..4405a9d7 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -642,8 +642,8 @@ Every equivalence `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`.
   ( is-equiv-α : is-equiv A' A α)
   : is-right-orthogonal-to-shape I ψ ϕ A' A α
   :=
-    is-equiv-extensions-is-equiv extext I ψ ϕ
-    ( \ _ → A') ( \  _ → A) ( \ _ → α) ( \ _ → is-equiv-α)
+    ( \ a → is-equiv-extensions-is-equiv extext I ψ ϕ
+      ( \ _ → A') ( \  _ → A) ( \ _ → α) ( a) ( \ _ → is-equiv-α))
 ```
 
 Right orthogonality is closed under homotopy.
@@ -802,7 +802,7 @@ follows for the former.
     = τhB)
   :=
     ind-has-section-equiv
-    ( relative-extension-type' I ψ ϕ
+    ( fiber-postcomp-Π-ext I ψ ϕ
       ( \ _ → relative-product A A' α B f) ( \ _ → B)
       ( \ _ → second-relative-product A A' α B f)
       ( σB') ( τB))
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 904d40b2..b37537f1 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -676,10 +676,11 @@ then $(x : X) → A x$ is a Segal type.
           ( \ t s → A s)
           ( \ u → recBOT)))
       ( \ h s t → h s t) -- second equivalence
-      ( second (equiv-extensions-BOT-equiv extext I ψ
+      ( second (equiv-extensions-equiv extext I ψ (\ _ → BOT)
         ( \ s → Δ² → A s)
         ( \ s → Λ → A s)
-        ( \ s → (horn-restriction (A s) , fiberwise-is-segal-A s))))
+        ( \ s → (horn-restriction (A s) , fiberwise-is-segal-A s))
+        ( \ _ → recBOT)))
       ( \ h t s → (h s) t) -- third equivalence
       ( second
         ( fubini
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 ad097a0c..36301df0 100644
--- a/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
+++ b/src/simplicial-hott/06-2cat-of-segal-types.rzk.md
@@ -10,9 +10,9 @@ This is a literate `rzk` file:
 
 ## Prerequisites
 
-- `03-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
+- `02-simplicial-type-theory.rzk.md` — We rely on definitions of simplicies and
   their subshapes.
-- `04-extension-types.rzk.md` — We use extension extensionality.
+- `03-extension-types.rzk.md` — We use extension extensionality.
 - `05-segal-types.rzk.md` - We use the notion of hom types.
 
 Some of the definitions in this file rely on function extensionality and
@@ -127,6 +127,66 @@ Preservation of composition requires the Segal hypothesis.
     ( functors-pres-comp A B is-segal-A is-segal-B F x y z f g)
 ```
 
+The action on morphisms commutes with transport.
+
+```rzk
+#def ap-hom-naturality
+  ( A B C : U)
+  ( f g : A → B)
+  ( h k : B → C)
+  ( p : f = g)
+  ( q : h = k)
+  ( x y : A)
+  : comp
+    ( hom B (f x) (f y))
+    ( hom B (g x) (g y))
+    ( hom C (k (g x)) (k (g y)))
+    ( ap-hom B C k (g x) (g y))
+    ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g p)
+    =
+    comp
+    ( hom B (f x) (f y)) (hom C (h (f x)) (h (f y))) (hom C (k (g x)) (k (g y)))
+    ( transport (A → C) (\ f' → hom C (f' x) (f' y))
+      ( comp A B C h f)
+      ( comp A B C k g)
+      ( comp-homotopic-maps A B C f g h k p q))
+    ( ap-hom B C h (f x) (f y))
+  :=
+  ind-path (A → B) f
+  ( \ g' p' →
+    comp (hom B (f x) (f y)) (hom B (g' x) (g' y)) (hom C (k (g' x)) (k (g' y)))
+    ( ap-hom B C k (g' x) (g' y))
+    ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f g' p')
+    =
+    comp
+    ( hom B (f x) (f y))(hom C (h (f x)) (h (f y)))(hom C (k (g' x)) (k (g' y)))
+    ( transport (A → C) (\ f' → hom C (f' x) (f' y))
+      ( comp A B C h f)
+      ( comp A B C k g')
+      ( comp-homotopic-maps A B C f g' h k p' q))
+    ( ap-hom B C h (f x) (f y)))
+  ( ind-path (B → C) h
+    ( \ k' q' →
+      comp (hom B (f x) (f y)) (hom B (f x) (f y)) (hom C (k' (f x)) (k' (f y)))
+      ( ap-hom B C k' (f x) (f y))
+      ( transport (A → B) (\ f' → hom B (f' x) (f' y)) f f refl)
+      =
+      comp
+      ( hom B (f x) (f y))
+      ( hom C (h (f x)) (h (f y)))
+      ( hom C (k' (f x)) (k' (f y)))
+      ( transport (A → C) (\ f' → hom C (f' x) (f' y))
+        ( comp A B C h f)
+        ( comp A B C k' f)
+        ( comp-homotopic-maps A B C f f h k' refl q'))
+      ( ap-hom B C h (f x) (f y)))
+    ( refl)
+    ( k)
+    ( q))
+  ( g)
+  ( p)
+```
+
 ## Natural transformations
 
 Given two simplicial maps `#!rzk f g : (x : A) → B x` , a **natural
@@ -440,3 +500,69 @@ the "Gray interchanger" built from two commutative triangles.
     ( horizontal-comp-nat-trans A B C f g f' g' η η')
   := \ (t, s) a → η' t (η s a)
 ```
+
+## Equivalences are fully faithful
+
+Since `#!rzk hom` is defined as an extension type, `#!rzk ap-hom` correspond to
+postcomposition. Hence, we can use `#!rzk is-equiv-extensions-is-equiv` to show
+that `#!rzk ap-hom` is an equivalence when f is an equivalence.
+
+```rzk
+#def is-equiv-ap-hom-is-equiv uses (extext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  ( x y : A)
+  : is-equiv (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y)
+  :=
+    is-equiv-extensions-is-equiv extext 2 Δ¹ ∂Δ¹
+    ( \ _ → A) ( \ _ → B)
+    ( \ _ → f)
+    ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y))
+    ( \ _ → is-equiv-f)
+```
+
+More precicely:
+
+```rzk
+#def fiber-ap-hom
+  ( A B : U)
+  ( x y : A)
+  ( f : A → B)
+  ( β : hom B (f x) (f y))
+  : U
+  :=
+    fib (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y) (β)
+
+#def is-contr-fiber-ap-hom-is-equiv uses (extext)
+  ( A B : U)
+  ( f : A → B)
+  ( is-equiv-f : is-equiv A B f)
+  ( x y : A)
+  ( β : hom B (f x) (f y))
+  : is-contr (fiber-ap-hom A B x y f β)
+  :=
+    is-contr-fiber-postcomp-Π-ext-is-equiv-fam extext 2 Δ¹ ∂Δ¹
+    ( \ _ → A) ( \ _ → B)
+    ( \ _ → f)
+    ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y))
+    ( β)
+    ( \ _ → is-equiv-f)
+```
+
+We can also define a retraction of `#!rzk ap-hom` directly.
+
+```rzk
+#def has-retraction-ap-hom-retraction uses (extext)
+  ( A B : U)
+  ( f : A → B)
+  ( has-retraction-f : has-retraction A B f)
+  ( x y : A)
+  : has-retraction (hom A x y) (hom B (f x) (f y)) (ap-hom A B f x y)
+  :=
+    has-retraction-extensions-has-retraction extext 2 Δ¹ ∂Δ¹
+    ( \ _ → A) ( \ _ → B)
+    ( \ _ → f)
+    ( \ _ → has-retraction-f)
+    ( \ t → recOR (t ≡ 0₂ ↦ x , t ≡ 1₂ ↦ y))
+```
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index 2b419242..bfc7e8f9 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -252,8 +252,7 @@ of discrete types is discrete.
 ```
 
 By extension extensionality, an extension type into a family of discrete types
-is discrete. Since `#!rzk equiv-extensions-BOT-equiv` considers total extension
-types only, extending from `#!rzk BOT`, that's all we prove here for now.
+is discrete.
 
 ```rzk
 #def equiv-hom-eq-extension-type-is-discrete uses (extext)
@@ -270,13 +269,11 @@ types only, extending from `#!rzk BOT`, that's all we prove here for now.
       ( (t : ψ) → hom (A t) (f t) (g t))
       ( hom ((t : ψ) → A t) f g)
       ( equiv-ExtExt extext I ψ (\ _ → BOT) A (\ _ → recBOT) f g)
-      ( equiv-extensions-BOT-equiv
-        ( extext)
-        ( I)
-        ( ψ)
+      ( equiv-extensions-equiv extext I ψ (\ _ → BOT)
         ( \ t → f t = g t)
         ( \ t → hom (A t) (f t) (g t))
-        ( \ t → (hom-eq (A t) (f t) (g t) , (is-discrete-A t (f t) (g t)))))
+        ( \ t → (hom-eq (A t) (f t) (g t) , (is-discrete-A t (f t) (g t))))
+        ( \ _ → recBOT))
       ( fubini
         ( I)
         ( 2)
@@ -1141,3 +1138,40 @@ Finally, we conclude:
   : is-segal A
   := is-contr-hom2-is-discrete A is-discrete-A
 ```
+
+## Naturality for hom-eq
+
+`#!rzk hom-eq` commute with `#!rzk ap-hom`.
+
+```rzk
+#def hom-eq-naturality
+  ( A B : U)
+  ( f : A → B)
+  ( x y : A)
+  ( p : x = y)
+  :
+  comp (x = y) (hom A x y) (hom B (f x) (f y))
+    ( ap-hom A B f x y)
+    ( hom-eq A x y)
+    ( p)
+  =
+  comp (x = y) ((f x) = (f y)) (hom B (f x) (f y))
+    ( hom-eq B (f x) (f y))
+    ( ap A B x y f)
+    ( p)
+  :=
+    ind-path A x
+      ( \ y' p' →
+        comp (x = y') (hom A x y') (hom B (f x) (f y'))
+          ( ap-hom A B f x y')
+          ( hom-eq A x y')
+          ( p')
+        =
+        comp (x = y') ((f x) = (f y')) (hom B (f x) (f y'))
+          ( hom-eq B (f x) (f y'))
+          ( ap A B x y' f)
+          ( p'))
+      ( functors-pres-id extext A B f x)
+      ( y)
+      ( p)
+```
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 6e251ffe..eebaed7b 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -1308,13 +1308,11 @@ domain are equivalent:
 #def equiv-total-dhom-equiv uses (A x y)
   : Equiv ( (t : Δ¹) → B (f t)) ((t : Δ¹) → C (f t))
   :=
-    equiv-extensions-BOT-equiv
-      ( extext)
-      ( 2)
-      ( Δ¹)
+    equiv-extensions-equiv extext 2 Δ¹ (\ _ → BOT)
       ( \ t → B (f t))
       ( \ t → C (f t))
       ( \ t → equiv-BC (f t))
+      ( \ _ → recBOT)
 
 #def equiv-total-covariant-dhom-equiv uses (extext equiv-BC)
   : Equiv
@@ -2088,3 +2086,35 @@ are discrete.
       ( is-covariant-representable-is-segal A is-segal-A x)
       ( y)
 ```
+
+In particular, the identity types of discrete types are also discrete. First, we
+show that equivalences preserve discreteness, which is a special case of
+preservation of local types by equivalences.
+
+```rzk
+#def equiv-preserve-discreteness uses (extext)
+  ( A B : U)
+  ( A≅B : Equiv A B)
+  ( is-discrete-B : is-discrete B)
+  : is-discrete A
+  :=
+  is-discrete-is-Δ¹-local A
+    (is-Δ¹-local-is-left-local A
+      ( is-local-type-equiv-is-local-type extext 2 Δ¹ (\ t → t ≡ 0₂) A B A≅B
+        ( is-left-local-is-Δ¹-local B
+          (is-Δ¹-local-is-discrete B is-discrete-B))))
+```
+
+```rzk title="RS17, Corollary 8.20"
+#def is-discrete-id-path-is-discrete uses (extext)
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  ( x y : A)
+  : is-discrete (x = y)
+  :=
+  equiv-preserve-discreteness (x = y) (hom A x y)
+  ( hom-eq A x y , is-discrete-A x y)
+  ( is-discrete-hom-is-segal A
+    ( is-segal-is-discrete extext A is-discrete-A)
+    ( x) ( y))
+```