diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index cadb5c65..52291225 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -24,18 +24,6 @@ This is a literate `rzk` file:
   := Σ (r : B → A) , (homotopy A A (comp A B A r f) (identity A))
 ```
 
-```rzk
-#def ind-has-section
-  ( f : A → B)
-  ( ( sec-f , ε-f) : has-section f)
-  ( C : B → U)
-  ( s : ( a : A) → C ( f a))
-  ( b : B)
-  : C b
-  :=
-    transport B C ( f (sec-f b)) b ( ε-f b) ( s (sec-f b))
-```
-
 We define equivalences to be bi-invertible maps.
 
 ```rzk
@@ -70,9 +58,17 @@ We define equivalences to be bi-invertible maps.
   : B → A
   := first (second is-equiv-f)
 
+#def has-section-is-equiv
+  : has-section A B f
+  := second is-equiv-f
+
 #def retraction-is-equiv uses (f)
   : B → A
   := first (first is-equiv-f)
+
+#def has-retraction-is-equiv
+  : has-retraction A B f
+  := first is-equiv-f
 ```
 
 ```rzk title="The homotopy between the section and retraction of an equivalence"
@@ -214,7 +210,7 @@ The inverse of an invertible map has an inverse.
         first ( second has-inverse-f)))
 ```
 
-## Composing equivalences
+## The type of equivalences
 
 The type of equivalences between types uses `#!rzk is-equiv` rather than
 `#!rzk has-inverse`.
@@ -226,6 +222,32 @@ The type of equivalences between types uses `#!rzk is-equiv` rather than
   := Σ (f : A → B) , (is-equiv A B f)
 ```
 
+## Induction with section
+
+```rzk
+#def ind-has-section
+  ( A B : U)
+  ( f : A → B)
+  ( ( sec-f , ε-f) : has-section A B f)
+  ( C : B → U)
+  ( s : (a : A) → C (f a))
+  ( b : B)
+  : C b
+  := transport B C (f (sec-f b)) b (ε-f b) (s (sec-f b))
+```
+
+It is convenient to have available the special case where `f` is an equivalence.
+
+```rzk
+#def ind-has-section-equiv
+  ( A B : U)
+  ( (f, is-equiv-f) : Equiv A B)
+  : ( C : B → U) → ((a : A) → C (f a)) → (b : B) → C b
+  := ind-has-section A B f (second is-equiv-f)
+```
+
+## Composing equivalences
+
 The data of an equivalence is not symmetric so we promote an equivalence to an
 invertible map to prove symmetry:
 
@@ -382,14 +404,12 @@ 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 A B f
   :=
-    ( ( comp B C A retr-gf g, η-gf) ,
-      ( comp B C A sec-gf g ,
-        \ b →
+    ( ( comp B C A retr-gf g, η-gf)
+    , ( comp B C A sec-gf g
+      , \ b →
             ap-cancel-has-retraction B C g
             has-retraction-g (f (sec-gf (g b))) b
-            ( ε-gf (g b))
-      )
-    )
+            ( ε-gf (g b))))
 ```
 
 ```rzk title="Left cancellation of equivalence property in diagrammatic order"
@@ -401,13 +421,11 @@ 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)
-    )
+          ( \ a → ap A B (retr-gf (g (f a))) a f (η-gf a)))
+    , ( comp C A B f sec-gf, ε-gf))
 ```
 
 We typically apply the cancelation property in a setting where the composite and
@@ -474,16 +492,16 @@ If a map is homotopic to an equivalence it is an equivalence.
   ( is-equiv-g : is-equiv A B g)
   : is-equiv A B f
   :=
-    ( ( ( first (first is-equiv-g)) ,
-        ( \ a →
+    ( ( ( first (first is-equiv-g))
+      , ( \ a →
           concat A
             ( first (first is-equiv-g) (f a))
             ( first (first is-equiv-g) (g a))
             ( a)
             ( ap B A (f a) (g a) (first (first is-equiv-g)) (H a))
-            ( second (first is-equiv-g) a))) ,
-      ( ( first (second is-equiv-g)) ,
-        ( \ b →
+            ( second (first is-equiv-g) a)))
+    , ( ( first (second is-equiv-g))
+      , ( \ b →
           concat B
             ( f (first (second is-equiv-g) b))
             ( g (first (second is-equiv-g) b))
@@ -786,8 +804,8 @@ dependent function types.
   ( famisequiv : (x : X) → is-equiv (A x) (B x) (f x))
   : is-equiv ((x : X) → A x) ((x : X) → B x) ( \ a x → f x (a x))
   :=
-    ( ( ( \ b x → first (first (famisequiv x)) (b x)) ,
-        ( \ a →
+    ( ( ( \ b x → first (first (famisequiv x)) (b x))
+      , ( \ a →
            eq-htpy
             X A
            ( \ x →
@@ -795,13 +813,12 @@ dependent function types.
                 ( first (famisequiv x))
                 ( f x (a x)))
             ( a)
-            ( \ x → second (first (famisequiv x)) (a x)))) ,
-      ( ( \ b x → first (second (famisequiv x)) (b x)) ,
-        ( \ b →
+            ( \ x → second (first (famisequiv x)) (a x))))
+    , ( ( \ b x → first (second (famisequiv x)) (b x))
+      , ( \ b →
             eq-htpy
             X B
-            ( \ x →
-               f x (first (second (famisequiv x)) (b x)))
+            ( \ x → f x (first (second (famisequiv x)) (b x)))
             ( b)
             ( \ x → second (second (famisequiv x)) (b x)))))
 ```
@@ -813,8 +830,8 @@ dependent function types.
   ( famequiv : (x : X) → Equiv (A x) (B x))
   : Equiv ((x : X) → A x) ((x : X) → B x)
   :=
-    ( ( \ a x → (first (famequiv x)) (a x)) ,
-      ( is-equiv-function-is-equiv-family
+    ( ( \ a x → (first (famequiv x)) (a x))
+    , ( is-equiv-function-is-equiv-family
         ( X)
         ( A)
         ( B)
@@ -863,6 +880,16 @@ dependent function types.
   := (rev A x y , ((rev A y x , rev-rev A x y) , (rev A y x , rev-rev A y x)))
 ```
 
+```rzk
+#def ind-rev
+  ( A : U)
+  ( x y : A)
+  ( B : (x = y) → U)
+  : ((p : y = x) → B (rev A y x p)) → ( q : x = y) → B q
+  :=
+    ind-has-section-equiv (y = x) (x = y) (equiv-rev A y x) ( B)
+```
+
 ## Concatenation with a fixed path is an equivalence
 
 ```rzk
@@ -872,20 +899,20 @@ dependent function types.
   ( p : x = y)
   : Equiv (y = z) (x = z)
   :=
-    ( concat A x y z p,
-      ( ( concat A y x z (rev A x y p), retraction-preconcat A x y z p),
-        ( concat A y x z (rev A x y p), section-preconcat A x y z p)))
+    ( concat A x y z p
+    , ( ( concat A y x z (rev A x y p), retraction-preconcat A x y z p)
+      , ( concat A y x z (rev A x y p), section-preconcat A x y z p)))
 
 #def equiv-postconcat
   ( A : U)
   ( x y z : A)
   ( q : y = z) : Equiv (x = y) (x = z)
   :=
-    ( \ p → concat A x y z p q,
-      ( ( \ r → concat A x z y r (rev A y z q),
-          retraction-postconcat A x y z q),
-        ( \ r → concat A x z y r (rev A y z q),
-          section-postconcat A x y z q)))
+    ( \ p → concat A x y z p q
+    , ( ( \ r → concat A x z y r (rev A y z q)
+        , retraction-postconcat A x y z q)
+      , ( \ r → concat A x z y r (rev A y z q)
+        , section-postconcat A x y z q)))
 ```
 
 ## Transport along a path is an equivalence
@@ -911,8 +938,8 @@ dependent function types.
   ( β : B' → B)
   : U
   :=
-    Σ ( ( s',s) : product ( A' → B' ) ( A → B)),
-      ( ( a' : A') → β ( s' a') = s ( α a'))
+    Σ ( ( s',s) : product ( A' → B' ) ( A → B))
+    , ( ( a' : A') → β ( s' a') = s ( α a'))
 
 #def Equiv-of-maps
   ( A' A : U)
@@ -921,11 +948,10 @@ dependent function types.
   ( β : B' → B)
   : U
   :=
-    Σ ( ((s', s), _) : map-of-maps A' A α B' B β),
-      ( product
-          ( is-equiv A' B' s')
-          ( is-equiv A B s)
-      )
+    Σ ( ((s', s), _) : map-of-maps A' A α B' B β)
+    , ( product
+        ( is-equiv A' B' s')
+        ( is-equiv A B s))
 
 #def is-equiv-equiv-is-equiv
   ( A' A : U)
@@ -940,11 +966,10 @@ dependent function types.
   :=
     is-equiv-right-factor A' A B α s is-equiv-s
       ( is-equiv-rev-homotopy A' B
-          ( comp A' B' B β s')
-          ( comp A' A B s α)
-          ( η )
-          ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β)
-      )
+        ( comp A' B' B β s')
+        ( comp A' A B s α)
+        ( η )
+        ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β))
 
 #def is-equiv-Equiv-is-equiv
   ( A' A : U)
@@ -953,8 +978,7 @@ dependent function types.
   ( β : B' → B)
   ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β )
   : is-equiv B' B β → is-equiv A' A α
-  :=
-    is-equiv-equiv-is-equiv A' A α B' B β S is-equiv-s' is-equiv-s
+  := is-equiv-equiv-is-equiv A' A α B' B β S is-equiv-s' is-equiv-s
 
 #def is-equiv-equiv-is-equiv'
   ( A' A : U)
@@ -972,8 +996,7 @@ dependent function types.
         ( comp A' B' B β s')
         ( comp A' A B s α)
         ( η)
-        ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s)
-      )
+        ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s))
 
 #def is-equiv-Equiv-is-equiv'
   ( A' A : U)
@@ -982,6 +1005,5 @@ dependent function types.
   ( β : B' → B)
   ( ( S, (is-equiv-s',is-equiv-s)) : Equiv-of-maps A' A α B' B β )
   : is-equiv A' A α → is-equiv B' B β
-  :=
-    is-equiv-equiv-is-equiv' A' A α B' B β S is-equiv-s' is-equiv-s
+  := is-equiv-equiv-is-equiv' A' A α B' B β S is-equiv-s' is-equiv-s
 ```
diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index f16ca147..0e0553e3 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -48,7 +48,7 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
   :=
     \ τ → ( τ, refl)
 
-#def extension-type-weakening-section
+#def section-extension-type-weakening'
   : ( σ : (t : ϕ) → A t)
   → ( th : homotopy-extension-type σ)
   → Σ (τ : extension-type σ), (( τ, refl) =_{homotopy-extension-type σ} th)
@@ -63,17 +63,24 @@ restriction map `(ψ → A) → (ϕ → A)`, which we can view as the types of
   ( σ : (t : ϕ) → A t)
   : (homotopy-extension-type σ) → (extension-type σ)
   :=
-    \ th → first (extension-type-weakening-section σ th)
+    \ th → first (section-extension-type-weakening' σ th)
+
+#def has-section-extension-type-weakening
+  ( σ : (t : ϕ) → A t)
+  : has-section (extension-type σ) (homotopy-extension-type σ)
+      (extension-type-weakening-map σ)
+  :=
+    ( extension-strictification σ
+    , \ th → ( second (section-extension-type-weakening' σ th)))
+
 
 #def is-equiv-extension-type-weakening
   ( σ : (t : ϕ) → A t)
   : is-equiv (extension-type σ) (homotopy-extension-type σ)
       (extension-type-weakening-map σ)
   :=
-    ( ( extension-strictification σ ,
-        \ _ → refl),
-      ( extension-strictification σ,
-        \ th → ( second (extension-type-weakening-section σ th))))
+    ( ( extension-strictification σ, \ _ → refl)
+    , has-section-extension-type-weakening σ)
 
 #def extension-type-weakening
   ( σ : (t : ϕ) → A t)
@@ -113,10 +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
@@ -1057,3 +1061,191 @@ $\left \langle_{t : I |\psi} f(t) = a'(t) \biggr|^\phi_{\lambda t.refl} \right\r
         ( a)
         ( f))))
 ```
+
+### Pointwise homotopy extension types
+
+Using `ExtExt` we can write the homotopy in the homotopy extension type
+pointwise.
+
+```rzk
+#section pointwise-homotopy-extension-type
+
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variable A : ψ → U
+
+#def pointwise-homotopy-extension-type
+  ( σ : (t : ϕ) → A t)
+  : U
+  :=
+    Σ ( τ : (t : ψ) → A t) , ( (t : ϕ) → (τ t =_{ A t} σ t))
+
+#def equiv-pointwise-homotopy-extension-type uses (extext)
+  ( σ : (t : ϕ) → A t)
+  : Equiv
+    ( homotopy-extension-type I ψ ϕ A σ)
+    ( pointwise-homotopy-extension-type σ)
+  :=
+    total-equiv-family-equiv
+    ( (t : ψ) → A t)
+    ( \ τ → (\ t → τ t) =_{ (t : ϕ) → A t} σ)
+    ( \ τ → (t : ϕ) → (τ t = σ t))
+    ( \ τ →
+      equiv-ExtExt extext I (\ t → ϕ t) (\ _ → BOT) (\ t → A t)
+      ( \ _ → recBOT) (\ t → τ t) σ)
+
+#def extension-type-pointwise-weakening uses (extext)
+  ( σ : (t : ϕ) → A t)
+  : Equiv
+    ( extension-type I ψ ϕ A σ)
+    ( pointwise-homotopy-extension-type σ)
+  := equiv-comp
+    ( extension-type I ψ ϕ A σ)
+    ( homotopy-extension-type I ψ ϕ A σ)
+    ( pointwise-homotopy-extension-type σ)
+    ( extension-type-weakening I ψ ϕ A σ)
+    ( equiv-pointwise-homotopy-extension-type σ)
+
+
+#end pointwise-homotopy-extension-type
+```
+
+## Relative extension types
+
+Given a map `α : A' → A`, there is also a notion of relative extension types.
+
+```rzk
+#section 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)]
+
+#def relative-extension-type
+  : U
+  :=
+    Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
+    , ( ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ refl])
+
+#def relative-extension-type'
+  : U
+  :=
+    fib
+    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
+    ( (t : ψ) → A t [ϕ t ↦ α t (σ' t)])
+    ( \ τ' t → α t (τ' t))
+    ( τ)
+
+#def equiv-relative-extension-type-fib uses (extext)
+  : Equiv
+    ( relative-extension-type')
+    ( relative-extension-type)
+  :=
+    total-equiv-family-equiv
+    ( (t : ψ) → A' t [ϕ t ↦ σ' t])
+    ( \ τ' → (\ 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)) ( τ))
+#end relative-extension-types
+```
+
+### Generalized relative extension types
+
+We will also need to allow more general relative extension types, where we start
+with a `τ : ψ → A` that does not strictly restrict to `\ t → α (σ' t)`.
+
+```rzk
+#section general-extension-types
+
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variables A' A : ψ → U
+#variable α : (t : ψ) → A' t → A t
+
+#def general-relative-extension-type
+  ( σ' : (t : ϕ) → A' t)
+  ( τ : (t : ψ) → A t)
+  ( h : (t : ϕ) → α t (σ' t) = τ t)
+  : U
+  :=
+    Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t])
+    , ( t : ψ) → (α t (τ' t) = τ t) [ϕ t ↦ h t]
+```
+
+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 ↦ α 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)))
+
+#def has-contr-relative-extension-types-generalize' uses (extext)
+  ( has-contr-relext-α : has-contr-relative-extension-types)
+  ( σ' : (t : ϕ) → A' t)
+  ( τ : (t : ψ) → A t)
+  ( 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))))
+  :=
+    ind-has-section-equiv
+    ( extension-type I ψ ϕ A (\ t → α t (σ' t)))
+    ( pointwise-homotopy-extension-type I ψ ϕ A (\ t → α t (σ' t)))
+    ( extension-type-pointwise-weakening I ψ ϕ A (\ t → α t (σ' t)))
+    ( \ (τ̂ , ĥ) →
+      is-contr
+      ( general-relative-extension-type σ' τ̂
+        ( \ t → rev (A t) (τ̂ t) (α t (σ' t)) (ĥ t))))
+    ( \ τ → has-contr-relext-α σ' τ)
+    ( τ , \ t → (rev (A t) (α t (σ' t)) (τ t) (h t)))
+
+#def has-contr-relative-extension-types-generalize uses (extext)
+  ( has-contr-relext-α : has-contr-relative-extension-types)
+  : has-contr-general-relative-extension-types
+  :=
+  \ σ' τ h →
+    transport
+    ( (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)))
+    ( h)
+    ( naiveextext-extext extext
+      ( I) (\ t → ϕ t) (\ _ → BOT) (\ t → α t (σ' t ) = τ t) (\ _ → recBOT)
+      ( \ t → rev (A t) (τ t) (α t (σ' t)) (rev (A t) (α t (σ' t)) (τ t) (h t)))
+      ( h)
+      ( \ t → rev-rev (A t) (α t (σ' t)) (τ t) (h t)))
+    ( has-contr-relative-extension-types-generalize'
+         has-contr-relext-α σ' τ h)
+```
+
+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)
+
+#end general-extension-types
+```
diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index d161a3da..a170619f 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -12,6 +12,7 @@ Some of the definitions in this file rely on extension extensionality:
 
 ```rzk
 #assume naiveextext : NaiveExtExt
+#assume extext : ExtExt
 #assume weakextext : WeakExtExt
 ```
 
@@ -41,7 +42,7 @@ orthogonal_ to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ 
 ```rzk title="BW23, Section 3"
 #def is-right-orthogonal-to-shape
   ( I : CUBE)
-  ( ψ : I → TOPE )
+  ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
   ( A' A : U)
   ( α : A' → A)
@@ -53,6 +54,80 @@ orthogonal_ to the map `α`, if `α : A' → A` is right orthogonal to `ϕ ⊂ 
       ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
 ```
 
+## Contractible relative extension types
+
+Using `ExtExt`, we can characterize right orthogonal maps in terms of the
+contractibility of relative extension types or, equivalently, generalized
+extension types.
+
+```rzk
+#section has-contr-relative-extension-types-iff-is-right-orthogonal
+
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+#variables A' A : U
+#variable α : A' → A
+
+#def is-right-orthogonal-to-shape-has-contr-relative-extension-types uses (extext)
+  ( are-contr-relext-α
+    : has-contr-relative-extension-types I ψ ϕ
+      ( \ _ → A') (\ _ → A) (\ _ → α))
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+    \ σ' →
+    is-equiv-is-contr-map
+    ( (t : ψ) → A' [ϕ t ↦ σ' t])
+    ( (t : ψ) → A [ϕ t ↦ α (σ' t)])
+    ( \ τ' t → α (τ' t))
+    ( \ τ →
+      is-contr-equiv-is-contr'
+      ( fib
+        ( (t : ψ) → A' [ϕ t ↦ σ' t])
+        ( (t : ψ) → A [ϕ t ↦ α (σ' t)])
+        ( \ τ' t → α (τ' t))
+        ( τ))
+      ( relative-extension-type I ψ ϕ
+        ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
+      ( equiv-relative-extension-type-fib extext I ψ ϕ
+        ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
+      ( 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 α)
+  : has-contr-relative-extension-types I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α)
+  :=
+    \ σ' τ →
+      is-contr-equiv-is-contr
+      ( fib
+        ( (t : ψ) → A' [ϕ t ↦ σ' t])
+        ( (t : ψ) → A [ϕ t ↦ α (σ' t)])
+        ( \ τ' t → α (τ' t))
+        ( τ))
+      ( relative-extension-type I ψ ϕ
+        ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
+      ( equiv-relative-extension-type-fib extext I ψ ϕ
+        ( \ _ → A') (\ _ → A) (\ _ → α) σ' τ)
+      ( is-contr-map-is-equiv
+        ( (t : ψ) → A' [ϕ t ↦ σ' t])
+        ( (t : ψ) → A [ϕ t ↦ α (σ' t)])
+        ( \ τ' t → α (τ' t))
+        ( is-orth-α σ')
+        ( τ))
+
+#def has-contr-general-relative-extension-types-is-right-orthogonal-to-shape
+  uses (extext)
+  ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : has-contr-general-relative-extension-types I ψ ϕ
+      ( \ _ → A') (\ _ → A) (\ _ → α)
+  :=
+    has-contr-relative-extension-types-generalize extext I ψ ϕ
+      ( \ _ → A') (\ _ → A) (\ _ → α)
+      ( has-contr-relative-extension-types-is-right-orthogonal-to-shape is-orth-α)
+
+#end has-contr-relative-extension-types-iff-is-right-orthogonal
+```
+
 ## Stability properties of left orthogonal shape inclusions
 
 We fix a map `α : A' → A`.
@@ -76,7 +151,6 @@ conditions.
 #variable is-orth-χ-ϕ : is-right-orthogonal-to-shape
                           I ( \ t → χ t) ( \ t → ϕ t) A' A α
 #variable is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
-  -- rzk does not accept these terms after η-reduction
 ```
 
 Using the vertical pasting calculus for homotopy cartesian squares, it is not
@@ -107,10 +181,10 @@ occasionally go back or forth along the functorial equivalence
       ( ( t : ψ) → A' [ϕ t ↦ σ' t])
       ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
       ( \ υ' t → α ( υ' t))
-      ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]),
-      ( ( t : ψ) → A' [χ t ↦ τ' t]))
-      ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]),
-      ( ( t : ψ) → A [χ t ↦ τ t]))
+      ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t])
+        , ( ( t : ψ) → A' [χ t ↦ τ' t]))
+      ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)])
+        , ( ( t : ψ) → A [χ t ↦ τ t]))
       ( \ (τ', υ') → ( \ t → α (τ' t), \t → α (υ' t)))
       ( cofibration-composition-functorial I ψ χ ϕ
         ( \ _ → A') ( \ _ → A) ( \ _ → α) σ')
@@ -131,10 +205,10 @@ Left orthogonal shape inclusions are preserved under composition.
         ( ( t : ψ) → A' [ϕ t ↦ σ' t])
         ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
         ( \ υ' t → α ( υ' t))
-        ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]),
-          ( ( t : ψ) → A' [χ t ↦ τ' t]))
-        ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]),
-          ( ( t : ψ) → A [χ t ↦ τ t]))
+        ( Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t])
+          , ( ( t : ψ) → A' [χ t ↦ τ' t]))
+        ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)])
+          , ( ( t : ψ) → A [χ t ↦ τ t]))
         ( \ (τ', υ') → ( \ t → α (τ' t), \t → α (υ' t)))
         ( cofibration-composition-functorial I ψ χ ϕ
           ( \ _ → A') ( \ _ → A) ( \ _ → α) σ')
@@ -175,7 +249,7 @@ If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so i
           ( is-orth-χ-ϕ )
           (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape)
           ( \ ( t : ϕ) → τ' t)
-          τ'
+          ( τ')
 ```
 
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` and `χ ⊂ ψ` is a (functorial)
@@ -197,7 +271,7 @@ shape retract, then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
       ( \ _ τ' x → α (τ' x) )
       ( \ _ _ υ' x → α (υ' x) )
       ( relativize-is-functorial-shape-retract I ψ χ is-fretract-ψ-χ ϕ A' A α)
-      (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape)
+      ( is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape)
 
 #end left-orthogonal-calculus-1
 ```
@@ -225,12 +299,10 @@ naive form of) extension extensionality.
       ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) A' A α
   :=
     \ ( σ' : ( (t,s) : J × I | χ t ∧ ϕ s) → A') →
-      (
-        ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))])
+      ( ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))])
             ( t, s) →
           ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
-        ,
-          \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) →
+        , \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) →
             naiveextext
               ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s)
               ( \ _ → A')
@@ -246,15 +318,11 @@ naive form of) extension extensionality.
                   ( \ s' → τ' (t, s') )
                   ( ( second (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                     ( \ s' → τ' (t, s')))
-                  ( s)
-              )
-        )
-      ,
-        ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))])
+                  ( s)))
+      , ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))])
             ( t, s) →
           ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
-        ,
-          \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) →
+        , \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) →
             naiveextext
               ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s)
               ( \ _ → A)
@@ -268,14 +336,11 @@ naive form of) extension extensionality.
                   ( \ s'' →
                       α ( ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                           ( \ s' → τ (t, s'))
-                          (s'')))
+                          ( s'')))
                   ( \ s' → τ (t, s') )
                   ( ( second ( second (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                     ( \ s' → τ (t, s')))
-                  ( s)
-              )
-        )
-      )
+                  ( s))))
 ```
 
 ### Stability under exact pushouts
@@ -303,6 +368,218 @@ For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to
          ( is-orth-ϕ-ψ∧ϕ ( \ t → τ' t))
 ```
 
+## Stability properties of right orthogonal maps
+
+Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate
+stability properties of maps right orthogonal to it.
+
+```rzk
+#section right-orthogonal-calculus
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable ϕ : ψ → TOPE
+```
+
+### Stability under composition
+
+```rzk
+#variables A'' A' A : U
+#variable α' : A'' → A'
+#variable α : A' → A
+
+#variable is-orth-ψ-ϕ-α' : is-right-orthogonal-to-shape I ψ ϕ A'' A' α'
+#variable is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α
+#variable is-orth-ψ-ϕ-αα' : is-right-orthogonal-to-shape I ψ ϕ A'' A
+                            ( comp A'' A' A α α')
+
+#def is-right-orthogonal-comp-to-shape
+  uses (is-orth-ψ-ϕ-α' is-orth-ψ-ϕ-α)
+  : is-right-orthogonal-to-shape I ψ ϕ A'' A (comp A'' A' A α α')
+  :=
+    \ σ'' →
+      is-equiv-comp
+      ( extension-type I ψ ϕ (\ _ → A'') σ'')
+      ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t)))
+      ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t))))
+      ( \ τ'' t → α' (τ'' t))
+      ( is-orth-ψ-ϕ-α' σ'')
+      ( \ τ' t → α (τ' t))
+      ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t)))
+```
+
+### Right cancellation
+
+```rzk
+#def is-right-orthogonal-right-cancel-to-shape
+  uses (is-orth-ψ-ϕ-α is-orth-ψ-ϕ-αα')
+  : is-right-orthogonal-to-shape I ψ ϕ A'' A' α'
+  :=
+    \ σ'' →
+    is-equiv-right-factor
+      ( extension-type I ψ ϕ (\ _ → A'') σ'')
+      ( extension-type I ψ ϕ (\ _ → A') (\ t → α' (σ'' t)))
+      ( extension-type I ψ ϕ (\ _ → A) (\ t → α (α' (σ'' t))))
+      ( \ τ'' t → α' (τ'' t))
+      ( \ τ' t → α (τ' t))
+      ( is-orth-ψ-ϕ-α (\ t → α' (σ'' t)))
+      ( is-orth-ψ-ϕ-αα' σ'')
+```
+
+### Stability under pullback
+
+Right orthogonal maps are stable under pullback. More precisely: If `α : A' → A`
+is right orthogonal, then so is the second projection
+`relative-product A A' α B f → B` for every `f : B → A`.
+
+To prove this, we first show that each relative extension type of
+`relative-product A A' α B f → B`, is a retract of a generalized extension type
+for `A' → A`. Since the latter are all contractible by assumption, the same
+follows for the former.
+
+```rzk
+#variable B : U
+#variable f : B → A
+
+#def relative-extension-type-pullback-general-relative-extension-type
+  ( σB' : ϕ → relative-product A A' α B f)
+  ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)])
+  ( (τA', hA)
+    : general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α)
+      ( \ t → first-relative-product A A' α B f (σB' t))
+      ( \ t → f (τB t))
+      ( \ t → homotopy-relative-product A A' α B f (σB' t)))
+  : relative-extension-type I ψ ϕ
+    ( \ _ → relative-product A A' α B f) ( \ _ → B)
+    ( \ _ → second-relative-product A A' α B f)
+    ( σB') ( τB)
+  :=
+    ( \ t → ( (τA' t, τB t) , hA t)
+    , \ t → refl)
+
+#def general-relative-extension-type-relative-extension-type-pullback
+  ( σB' : ϕ → relative-product A A' α B f)
+  ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)])
+  ( (τB', hB)
+    : relative-extension-type I ψ ϕ
+      ( \ _ → relative-product A A' α B f) ( \ _ → B)
+      ( \ _ → second-relative-product A A' α B f)
+      ( σB') ( τB))
+  : general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α)
+    ( \ t → first-relative-product A A' α B f (σB' t))
+    ( \ t → f (τB t))
+    ( \ t → homotopy-relative-product A A' α B f (σB' t))
+  :=
+    ( \ t → first-relative-product A A' α B f (τB' t)
+    , \ t →
+      concat A
+      ( α (first-relative-product A A' α B f (τB' t)))
+      ( f (second-relative-product A A' α B f (τB' t)))
+      ( f (τB t))
+      ( homotopy-relative-product A A' α B f (τB' t))
+      ( ap B A
+        ( second-relative-product A A' α B f (τB' t))
+        ( τB t)
+        ( f) ( hB t)))
+
+#def is-id-rel-ext-type-pb-gen-rel-ext-type-rel-ext-type-pb uses (extext)
+  ( σB' : ϕ → relative-product A A' α B f)
+  ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)])
+  : ( τhB
+      : relative-extension-type I ψ ϕ
+        ( \ _ → relative-product A A' α B f) ( \ _ → B)
+        ( \ _ → second-relative-product A A' α B f)
+        ( σB') ( τB))
+  → ( relative-extension-type-pullback-general-relative-extension-type σB' τB
+      ( general-relative-extension-type-relative-extension-type-pullback σB' τB τhB)
+    = τhB)
+  :=
+    ind-has-section-equiv
+    ( relative-extension-type' I ψ ϕ
+      ( \ _ → relative-product A A' α B f) ( \ _ → B)
+      ( \ _ → second-relative-product A A' α B f)
+      ( σB') ( τB))
+    ( relative-extension-type I ψ ϕ
+      ( \ _ → relative-product A A' α B f) ( \ _ → B)
+      ( \ _ → second-relative-product A A' α B f)
+      ( σB') ( τB))
+    ( equiv-relative-extension-type-fib extext I ψ ϕ
+      ( \ _ → relative-product A A' α B f) ( \ _ → B)
+      ( \ _ → second-relative-product A A' α B f)
+      ( σB') ( τB))
+    ( \ τhB →
+      ( relative-extension-type-pullback-general-relative-extension-type σB' τB
+        ( general-relative-extension-type-relative-extension-type-pullback σB' τB τhB)
+      = τhB))
+    ( ind-fib
+      ( (t : ψ) → relative-product A A' α B f [ϕ t ↦ σB' t])
+      ( (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)])
+      ( \ τB' t → second-relative-product A A' α B f (τB' t))
+      ( \ τB₁ (τB'₁, h₁) →
+        ( relative-extension-type-pullback-general-relative-extension-type σB' τB₁
+          ( general-relative-extension-type-relative-extension-type-pullback σB' τB₁
+            ( τB'₁
+            , ext-htpy-eq I ψ ϕ (\ _ → B)
+              ( \ t → second-relative-product A A' α B f (σB' t))
+              ( \ t → second-relative-product A A' α B f (τB'₁ t))
+              ( τB₁) ( h₁)))
+        = ( τB'₁
+          , ext-htpy-eq I ψ ϕ (\ _ → B)
+            ( \ t → second-relative-product A A' α B f (σB' t))
+            ( \ t → second-relative-product A A' α B f (τB'₁ t))
+            ( τB₁) ( h₁))))
+      ( \ τB' → refl)
+      ( τB))
+
+#def is-retract-of-rel-ext-type-pb-gen-rel-ext-type uses (extext)
+  ( σB' : ϕ → relative-product A A' α B f)
+  ( τB : (t : ψ) → B [ϕ t ↦ second-relative-product A A' α B f (σB' t)])
+  : is-retract-of
+    ( relative-extension-type I ψ ϕ
+      ( \ _ → relative-product A A' α B f) ( \ _ → B)
+      ( \ _ → second-relative-product A A' α B f)
+      ( σB') ( τB))
+    ( general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α)
+      ( \ t → first-relative-product A A' α B f (σB' t))
+      ( \ t → f (τB t))
+      ( \ t → homotopy-relative-product A A' α B f (σB' t)))
+  :=
+    ( general-relative-extension-type-relative-extension-type-pullback σB' τB
+    , ( relative-extension-type-pullback-general-relative-extension-type σB' τB
+      , is-id-rel-ext-type-pb-gen-rel-ext-type-rel-ext-type-pb σB' τB))
+```
+
+Then we can deduce that right orthogonal maps are preserved under pullback:
+
+```rzk
+#def is-right-orthoponal-pullback-to-shape uses (extext is-orth-ψ-ϕ-α)
+  : is-right-orthogonal-to-shape I ψ ϕ
+    ( relative-product A A' α B f) ( B)
+    ( second-relative-product A A' α B f)
+  :=
+    is-right-orthogonal-to-shape-has-contr-relative-extension-types I ψ ϕ
+    ( relative-product A A' α B f) ( B)
+    ( second-relative-product A A' α B f)
+    ( \ σB' τB →
+      is-contr-is-retract-of-is-contr
+      ( relative-extension-type I ψ ϕ
+        ( \ _ → relative-product A A' α B f) ( \ _ → B)
+        ( \ _ → second-relative-product A A' α B f)
+        ( σB') ( τB))
+      ( general-relative-extension-type I ψ ϕ (\ _ → A') (\ _ → A) (\ _ → α)
+        ( \ t → first-relative-product A A' α B f (σB' t))
+        ( \ t → f (τB t))
+        ( \ t → homotopy-relative-product A A' α B f (σB' t)))
+      ( is-retract-of-rel-ext-type-pb-gen-rel-ext-type σB' τB)
+      ( has-contr-general-relative-extension-types-is-right-orthogonal-to-shape
+        I ψ ϕ A' A α
+        ( is-orth-ψ-ϕ-α)
+        ( \ t → first-relative-product A A' α B f (σB' t))
+        ( \ t → f (τB t))
+        ( \ t → homotopy-relative-product A A' α B f (σB' t))))
+
+#end right-orthogonal-calculus
+```
+
 ## Types with unique extension
 
 We say that an type `A` has unique extensions for a shape inclusion `ϕ ⊂ ψ`, if
@@ -317,8 +594,7 @@ for each `σ : ϕ → A` the type of `ψ`-extensions is contractible.
 
 #def has-unique-extensions
   : U
-  :=
-    ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t])
+  := ( σ : ϕ → A) → is-contr ( (t : ψ) → A [ϕ t ↦ σ t])
 ```
 
 There are other equivalent characterizations which we shall prove below:
@@ -356,11 +632,11 @@ of the restriction map `(ψ → A) → (ϕ → A)`.
   :=
     is-equiv-is-contr-map (ψ → A) (ϕ → A) ( \ τ t → τ t)
       ( \ ( σ : ϕ → A) →
-          is-contr-equiv-is-contr
-            ( extension-type I ψ ϕ ( \ t → A) σ)
-            ( homotopy-extension-type I ψ ϕ ( \ t → A) σ)
-            ( extension-type-weakening I ψ ϕ ( \ t → A) σ)
-            ( has-ue-ψ-ϕ-A σ))
+        is-contr-equiv-is-contr
+          ( extension-type I ψ ϕ ( \ t → A) σ)
+          ( homotopy-extension-type I ψ ϕ ( \ t → A) σ)
+          ( extension-type-weakening I ψ ϕ ( \ t → A) σ)
+          ( has-ue-ψ-ϕ-A σ))
 
 #def has-unique-extensions-is-local-type
   ( is-lt-ψ-ϕ-A : is-local-type)