diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index 60b49a06..a1f238ef 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -739,6 +739,19 @@ dependent function types.
     Σ ( ( s',s) : product ( A' → B' ) ( A → B)),
       ( ( a' : A') → β ( s' a') = s ( α a'))
 
+#def Equiv-of-maps
+  ( A' A : U)
+  ( α : A' → A)
+  ( B' B : U)
+  ( β : B' → B)
+  : U
+  :=
+    Σ ( ((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)
   ( α : A' → A)
@@ -758,6 +771,16 @@ dependent function types.
           ( is-equiv-comp A' B' B s' is-equiv-s' β is-equiv-β)
       )
 
+#def is-equiv-Equiv-is-equiv
+  ( A' A : U)
+  ( α : A' → A)
+  ( B' B : U)
+  ( β : 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
+
 #def is-equiv-equiv-is-equiv'
   ( A' A : U)
   ( α : A' → A)
@@ -776,4 +799,14 @@ dependent function types.
         ( η)
         ( is-equiv-comp A' A B α is-equiv-α s is-equiv-s)
       )
+
+#def is-equiv-Equiv-is-equiv'
+  ( A' A : U)
+  ( α : A' → A)
+  ( B' B : U)
+  ( β : 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
 ```
diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 1588a6ca..972814f4 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -314,20 +314,38 @@ the corresponding statements about equivalences established above.
         ( is-homotopy-cartesian-upper-to-fibers is-hc-γ-δ a')
         ( is-hc-α-γ a' )
 
-#def is-homotopy-cartesian-lower-cancellation
+#def is-homotopy-cartesian-vertical-pasting-from-fibers
+  ( is-hc-α-γ : is-homotopy-cartesian A' C' A C α γ )
+  ( is-fiberwise-hc-γ-δ
+    : ( a' : A') →
+      is-homotopy-cartesian (C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a'))
+  : is-homotopy-cartesian-vertical-pasted
+  :=
+    is-homotopy-cartesian-vertical-pasting
+      is-hc-α-γ
+      ( is-homotopy-cartesian-upper-from-fibers is-fiberwise-hc-γ-δ)
+
+#def is-homotopy-cartesian-lower-cancel-to-fibers
+  ( is-hc-α-γ : is-homotopy-cartesian A' C' A C α γ )
+  ( is-hc-α-δ : is-homotopy-cartesian-vertical-pasted)
+  ( a' : A')
+  : is-homotopy-cartesian (C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a')
+  :=
+    is-homotopy-cartesian-is-horizontal-equiv
+      ( C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a')
+      ( is-hc-α-γ a')
+      ( is-hc-α-δ a')
+
+#def is-homotopy-cartesian-lower-cancel uses (D D' δ)
   ( is-hc-α-γ : is-homotopy-cartesian A' C' A C α γ )
   ( is-hc-α-δ : is-homotopy-cartesian-vertical-pasted
   )
   : is-homotopy-cartesian-upper
   :=
     is-homotopy-cartesian-upper-from-fibers
-    ( \ a' →
-        is-homotopy-cartesian-is-horizontal-equiv
-        ( C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a')
-        ( is-hc-α-γ a')
-        ( is-hc-α-δ a'))
+      (is-homotopy-cartesian-lower-cancel-to-fibers is-hc-α-γ is-hc-α-δ)
 
-#def is-homotopy-cartesian-upper-cancellation-with-section
+#def is-homotopy-cartesian-upper-cancel-with-section
   ( has-sec-γ-δ : (a' : A') →
       has-section-family-over-map
         (C' a') (D' a') (C (α a')) (D (α a')) (γ a') (δ a'))
@@ -376,7 +394,7 @@ from composition and cancelling laws for equivalences.
       (F' a'') (ihc' a'')
       (F (f' a'')) (ihc (f' a''))
 
-#def is-homotopy-cartesian-right-cancellation
+#def is-homotopy-cartesian-right-cancel
   ( ihc : is-homotopy-cartesian A' C' A C f F)
   ( ihc'' : is-homotopy-cartesian A'' C'' A C
               ( comp A'' A' A f f')
diff --git a/src/simplicial-hott/03-simplicial-type-theory.rzk.md b/src/simplicial-hott/03-simplicial-type-theory.rzk.md
index 7351a875..9c758c4e 100644
--- a/src/simplicial-hott/03-simplicial-type-theory.rzk.md
+++ b/src/simplicial-hott/03-simplicial-type-theory.rzk.md
@@ -178,6 +178,36 @@ For example, this applies to `Δ² ⊂ Δ¹×Δ¹`.
           \ a' → refl)
 ```
 
+Every functorial shape retract automatically induces a section
+when restricting to diagrams extending a fixed diagram `σ': ϕ → A'`
+(or, respectively, its image `ϕ → A` under α).
+
+```rzk
+#def relativize-is-functorial-shape-retract
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( χ : ψ → TOPE)
+  ( is-fretract-ψ-χ : is-functorial-shape-retract I ψ χ)
+  ( ϕ : χ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  ( σ' : ϕ → A')
+  : has-section-family-over-map
+      ( (t : χ) → A' [ϕ t ↦ σ' t])
+      ( \ τ' → (t : ψ) → A' [χ t ↦ τ' t])
+      ( (t : χ) → A [ϕ t ↦ α (σ' t)])
+      ( \ τ → (t : ψ) → A [χ t ↦ τ t])
+      ( \ τ' t → α (τ' t))
+      ( \ _ υ' t → α (υ' t))
+  :=
+    ( ( \ τ' → first (first (is-fretract-ψ-χ A' A α)) τ'
+      , \ τ → second (first (is-fretract-ψ-χ A' A α)) τ
+      )
+    , \ τ' → second (is-fretract-ψ-χ A' A α) τ'
+    )
+
+```
+
 ### Pushout product
 
 Pushout product Φ×ζ ∪\_{Φ×χ} ψ×χ of Φ ↪ ψ and χ ↪ ζ, domain of the co-gap map.
@@ -210,7 +240,7 @@ The intersection of shapes is defined by conjunction on topes.
 The union of shapes is defined by disjunction on topes.
 
 ```rzk
-#def shapeUnion
+#def shape-union
   ( I : CUBE)
   ( ψ χ : I → TOPE)
   : I → TOPE
diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 2bb44827..3f8942bb 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -162,6 +162,31 @@ The original form.
     ( \ h → (\ t → h t , \ t → h t) ,
       ( ( \ (_f , g) t → g t , \ h → refl) ,
         ( ( \ (_f , g) t → g t , \ h → refl))))
+
+#def cofibration-composition-functorial
+  ( I : CUBE)
+  ( χ : I → TOPE)
+  ( ψ : χ → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A' A : χ → U)
+  ( α : (t : χ) → A' t → A t)
+  ( σ' : (t : ϕ) → A' t)
+  : Equiv-of-maps
+     ( (t : χ) → A' t [ϕ t ↦ σ' t])
+     ( (t : χ) → A t [ϕ t ↦ α t (σ' t)])
+     ( \ τ' t → α t (τ' t))
+     ( Σ ( τ' : (t : ψ) → A' t [ϕ t ↦ σ' t]) ,
+        ( (t : χ) → A' t [ψ t ↦ τ' t]))
+     ( Σ ( τ : (t : ψ) → A t [ϕ t ↦ α t (σ' t)]) ,
+        ( (t : χ) → A t [ψ t ↦ τ t]))
+     ( \ (τ', υ') → ( \ t → α t (τ' t), \t → α t (υ' t)))
+  :=
+    ( ( ( \ h → (\ t → h t , \ t → h t) , \ h → (\ t → h t , \ t → h t)),
+        \ _ → refl),
+      ( ( ( \ (_f , g) t → g t , \ h → refl) ,
+          ( ( \ (_f , g) t → g t , \ h → refl))),
+        ( ( \ (_f , g) t → g t , \ h → refl) ,
+          ( ( \ (_f , g) t → g t , \ h → refl)))))
 ```
 
 A reformulated version via tope disjunction instead of inclusion (see
@@ -196,6 +221,31 @@ A reformulated version via tope disjunction instead of inclusion (see
     (\ h t → h t ,
       ( ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl) ,
         ( \ g t → recOR (ϕ t ↦ g t , ψ t ↦ a t) , \ _ → refl)))
+
+#def cofibration-union-functorial
+  ( I : CUBE)
+  ( ϕ ψ : I → TOPE)
+  ( A' A : (t : I | ϕ t ∨ ψ t) → U)
+  ( α : (t : I | ϕ t ∨ ψ t) → A' t → A t)
+  ( τ' : (t : ψ) → A' t)
+  : Equiv-of-maps
+      ( (t : I | ϕ t ∨ ψ t) → A' t [ψ t ↦ τ' t])
+      ( (t : I | ϕ t ∨ ψ t) → A t [ψ t ↦ α t (τ' t)])
+      ( \ υ' t → α t (υ' t))
+      ( (t : ϕ) → A' t [ϕ t ∧ ψ t ↦ τ' t])
+      ( (t : ϕ) → A t [ϕ t ∧ ψ t ↦ α t (τ' t)])
+      ( \ ν' t → α t (ν' t))
+  :=
+     ( ( ( \ υ' t → υ' t
+         , \ υ t → υ t
+         )
+       , \ _ → refl
+       )
+     , ( second (cofibration-union I ϕ ψ A' τ')
+       ,
+         second (cofibration-union I ϕ ψ A ( \ t → α t (τ' t)))
+       )
+     )
 ```
 
 ## Extension extensionality
@@ -352,7 +402,7 @@ cases an extension type to a function type.
       ( ϕ )
       ( A )
       ( \ t y → (ext-projection-temp) t = y)
-      ( a ) -- a
+      ( a )
       ( \t → refl ))
     ( is-contr-ext-based-paths)
 
@@ -640,7 +690,7 @@ Both directions of this statement will be needed.
           rev
             ( A t )
             ( first (is-contr-fiberwise-A t) )
-            ( a t) --
+            ( a t)
             ( second (is-contr-fiberwise-A t) (a t))
 
 ```
diff --git a/src/simplicial-hott/04a-right-orthogonal.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
new file mode 100644
index 00000000..71e28d00
--- /dev/null
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -0,0 +1,304 @@
+# 4a. Right orthogonal fibrations
+
+This is a literate `rzk` file:
+
+```rzk
+#lang rzk-1
+```
+
+## Prerequisites
+
+Some of the definitions in this file rely on naive extension extensionality:
+
+```rzk
+#assume naiveextext : NaiveExtExt
+```
+
+## Right orthogonal maps with respect to shapes
+
+For every shape inclusion `ϕ ⊂ ψ`,
+we obtain a fibrancy condition for a map `α : A' → A`
+in terms of unique extension along `ϕ ⊂ ψ`.
+This is a relative version of unique extension along `ϕ ⊂ ψ`.
+
+We say that `α : A' → A` is _right orthogonal_ to the shape inclusion `ϕ ⊂ ψ`,
+if the square
+```
+(ψ → A') → (ψ → A)
+
+   ↓          ↓
+
+(ϕ → A') → (ϕ → A)
+```
+is homotopy cartesian.
+
+Equivalently, we can interpret this orthogonality
+as a cofibrancy condition on the shape inclusion.
+We say that the shape inclusion `ϕ ⊂ ψ` is _left 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 )
+  ( ϕ : ψ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  : U
+  :=
+    is-homotopy-cartesian
+      ( ϕ → A' ) ( \ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+      ( ϕ → A ) ( \ σ → (t : ψ) → A [ϕ t ↦ σ t])
+      ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
+```
+
+## Stability properties of left orthogonal shape inclusions
+
+We fix a map `α : A' → A`.
+
+```rzk
+#section left-orthogonal-calculus-1
+
+#variables A' A : U
+#variable α : A' → A
+```
+Consider nested shapes `ϕ ⊂ χ ⊂ ψ`
+and the three possible right orthogonality conditions.
+
+```rzk
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable χ : ψ → TOPE
+#variable ϕ : χ → TOPE
+#variable is-orth-ψ-χ : is-right-orthogonal-to-shape I ψ χ A' A α
+#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 hard to deduce the corresponding composition and cancellation properties
+for left orthogonality of shape inclusion with respect to `α : A' → A`.
+
+### Σ over an intermediate shape
+
+The only fact that stops some of these laws from being a direct corollary
+is that the `Σ`-types appearing in the vertical pasting of the relevant squares
+(such as `Σ (\ σ : ϕ → A), ( (t : χ) → A [ϕ t ↦ σ t])`)
+are not literally equal to the corresponding extension types
+(such as `τ → A `).
+Therefore we have to occasionally go back or forth along the
+functorial equivalence `cofibration-composition-functorial`.
+
+```rzk
+#def is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape uses (is-orth-ψ-ϕ)
+  : is-homotopy-cartesian
+    ( ϕ → A')
+    ( \ σ' → Σ ( τ' : (t : χ) → A' [ϕ t ↦ σ' t]), ( t : ψ) → A' [χ t ↦ τ' t])
+    ( ϕ → A)
+    ( \ σ → Σ ( τ : (t : χ) → A [ϕ t ↦ σ t]), ( t : ψ) → A [χ t ↦ τ t])
+    ( \ σ' t → α (σ' t))
+    ( \ _ (τ', υ') → ( \ t → α (τ' t), \ t → α (υ' t) ))
+  :=
+    ( \ (σ' : ϕ → A') →
+    is-equiv-Equiv-is-equiv'
+      ( ( 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 → α (τ' t), \t → α (υ' t)))
+      ( cofibration-composition-functorial I ψ χ ϕ
+        ( \ _ → A') ( \ _ → A) ( \ _ → α) σ')
+      ( is-orth-ψ-ϕ σ'))
+```
+
+### Stability under composition
+
+Left orthogonal shape inclusions are preserved under composition.
+
+```rzk title="right-orthogonality for composition of shape inclusions"
+
+#def is-right-orthogonal-to-shape-comp uses (is-orth-ψ-χ is-orth-χ-ϕ)
+  : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
+  :=
+    \ σ' →
+      is-equiv-Equiv-is-equiv
+        ( ( 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 → α (τ' t), \t → α (υ' t)))
+        ( cofibration-composition-functorial I ψ χ ϕ
+          ( \ _ → A') ( \ _ → A) ( \ _ → α) σ')
+        ( is-homotopy-cartesian-vertical-pasting-from-fibers
+          ( ϕ → A' )
+          ( \ σ' → (t : χ) → A' [ϕ t ↦ σ' t])
+          ( \ _ τ' → (t : ψ) → A' [χ t ↦ τ' t])
+          ( ϕ → A )
+          ( \ σ → (t : χ) → A [ϕ t ↦ σ t])
+          ( \ _ τ → (t : ψ) → A [χ t ↦ τ t])
+          ( \ σ' t → α (σ' t))
+          ( \ _ τ' x → α (τ' x) )
+          ( \ _ _ υ' x → α (υ' x) )
+          is-orth-χ-ϕ
+          ( \ _ τ' → is-orth-ψ-χ τ')
+          σ')
+```
+
+### Cancellation laws
+
+If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so is `χ ⊂ ψ`.
+
+```rzk
+#def is-right-orthogonal-to-shape-left-cancel uses (is-orth-χ-ϕ is-orth-ψ-ϕ)
+  : is-right-orthogonal-to-shape I ψ χ A' A α
+  :=
+    \ τ' →
+        is-homotopy-cartesian-lower-cancel-to-fibers
+          ( ϕ → A' )
+          ( \ σ' → (t : χ) → A' [ϕ t ↦ σ' t])
+          ( \ _ τ' → (t : ψ) → A' [χ t ↦ τ' t])
+          ( ϕ → A )
+          ( \ σ → (t : χ) → A [ϕ t ↦ σ t])
+          ( \ _ τ → (t : ψ) → A [χ t ↦ τ t])
+          ( \ σ' t → α (σ' t))
+          ( \ _ τ' x → α (τ' x) )
+          ( \ _ _ υ' x → α (υ' x) )
+          ( is-orth-χ-ϕ )
+          (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape)
+          ( \ ( t : ϕ) → τ' t)
+          τ'
+```
+
+If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`
+and `χ ⊂ ψ` is a (functorial) shape retract,
+then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
+
+```rzk
+#def is-right-orthogonal-to-shape-right-cancel-retract uses (is-orth-ψ-ϕ)
+  ( is-fretract-ψ-χ : is-functorial-shape-retract I ψ χ)
+  : is-right-orthogonal-to-shape I ( \ t → χ t) ( \ t → ϕ t) A' A α
+  :=
+    is-homotopy-cartesian-upper-cancel-with-section
+      ( ϕ → A' )
+      ( \ σ' → (t : χ) → A' [ϕ t ↦ σ' t])
+      ( \ _ τ' → (t : ψ) → A' [χ t ↦ τ' t])
+      ( ϕ → A )
+      ( \ σ → (t : χ) → A [ϕ t ↦ σ t])
+      ( \ _ τ → (t : ψ) → A [χ t ↦ τ t])
+      ( \ σ' t → α (σ' t))
+      ( \ _ τ' x → α (τ' x) )
+      ( \ _ _ υ' x → α (υ' x) )
+      ( relativize-is-functorial-shape-retract I ψ χ is-fretract-ψ-χ ϕ A' A α)
+      (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape)
+
+#end left-orthogonal-calculus-1
+```
+
+### Stability under exponentiation
+
+If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`
+then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
+
+The following proof uses a lot of currying and uncurrying
+and relies on (the naive form of) extension extensionality.
+
+```rzk
+#def is-right-orthogonal-to-shape-× uses (naiveextext)
+-- this should be refactored by introducing cofibration-product-functorial
+  ( A' A : U)
+  ( α : A' → A)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  : is-right-orthogonal-to-shape
+      ( J × I) ( shape-prod J I χ ψ) ( \ (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) →
+          ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
+        ,
+          \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) →
+            naiveextext
+              ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s)
+              ( \ _ → A')
+              ( \ ( t,s) → σ' (t,s))
+              ( \ ( t,s) →
+                ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
+                  ( \ s' → α (τ' (t, s'))) s)
+              ( τ')
+              ( \ ( t,s) →
+                ext-htpy-eq I ψ ϕ (\ _ → A') ( \ s' → σ' (t, s'))
+                  ( ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
+                    ( \ s' → α (τ' (t, s'))))
+                  ( \ s' → τ' (t, s') )
+                  ( ( second (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
+                    ( \ 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))]) →
+            naiveextext
+              ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s)
+              ( \ _ → A)
+              ( \ (t,s) → α (σ' (t,s)))
+              ( \ (t,s) →
+                α ( ( first ( second ( is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
+                      ( \ s' → τ (t, s')) s))
+              ( τ)
+              ( \ ( t,s) →
+                ext-htpy-eq I ψ ϕ (\ _ → A) ( \ s' → α (σ' (t, s')))
+                  ( \ s'' →
+                      α ( ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
+                          ( \ s' → τ (t, s'))
+                          (s'')))
+                  ( \ s' → τ (t, s') )
+                  ( ( second ( second (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
+                    ( \ s' → τ (t, s')))
+                  ( s)
+              )
+        )
+      )
+```
+
+### Stability under exact pushouts
+
+For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to `α : A' → A`,
+then so is `ψ ⊂ ϕ ∪ ψ`.
+
+```rzk
+#def is-right-orthogonal-to-shape-pushout
+  ( A' A : U)
+  ( α : A' → A)
+  ( I : CUBE)
+  ( ϕ ψ : I → TOPE)
+  ( is-orth-ϕ-ψ∧ϕ : is-right-orthogonal-to-shape I ϕ ( \ t → ϕ t ∧ ψ t) A' A α)
+  : is-right-orthogonal-to-shape I ( \ t → ϕ t ∨ ψ t) ( \ t → ψ t) A' A α
+  := \ ( τ' : ψ → A') →
+       is-equiv-Equiv-is-equiv
+         ( (t : I | ϕ t ∨ ψ t) → A' [ψ t ↦ τ' t])
+         ( (t : I | ϕ t ∨ ψ t) → A [ψ t ↦ α (τ' t)])
+         ( \ υ' t → α (υ' t))
+         ( (t : ϕ) → A' [ϕ t ∧ ψ t ↦ τ' t])
+         ( (t : ϕ) → A [ϕ t ∧ ψ t ↦ α (τ' t)])
+         ( \ ν' t → α (ν' t))
+         ( cofibration-union-functorial I ϕ ψ (\ _ → A') (\ _ → A) (\ _ → α) τ')
+         ( is-orth-ϕ-ψ∧ϕ ( \ t → τ' t))
+```