From e047325606f6577c1aac77e011d044a791618429 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Thu, 28 Sep 2023 11:10:01 +0200
Subject: [PATCH 01/15] define j-orthogonal and claim that they are closed
 under exp

---
 src/simplicial-hott/04-extension-types.rzk.md | 73 +++++++++++++++++--
 1 file changed, 65 insertions(+), 8 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index ec874972..938c3843 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -536,7 +536,7 @@ extensionality.
         ( \ t → ( a t , e t) )))
 ```
 
-In an extension type of a dependent type that is pointwise contractible, then we have an inhabitant of the extension type witnessing the contraction, at every inhabitant of the base, of each point in the fiber to the center of the fiber. Both directions of this statement will be needed. 
+In an extension type of a dependent type that is pointwise contractible, then we have an inhabitant of the extension type witnessing the contraction, at every inhabitant of the base, of each point in the fiber to the center of the fiber. Both directions of this statement will be needed.
 
 ```rzk
 
@@ -558,16 +558,16 @@ In an extension type of a dependent type that is pointwise contractible, then we
   ( a : (t : ϕ ) → A t)
   ( is-contr-fiberwise-A : (t : ψ ) → is-contr ( A t))
   : (t : ϕ ) → (a t = first (is-contr-fiberwise-A t))
-  :=  \ t → 
+  :=  \ t →
           rev
             ( A t )
             ( first (is-contr-fiberwise-A t) )
-            ( a t) -- 
+            ( a t) --
             ( second (is-contr-fiberwise-A t) (a t))
 
 ```
 
-```rzk 
+```rzk
 
 #define first-4-11
   (weak-ext-ext : WeakExtExt)
@@ -578,11 +578,11 @@ In an extension type of a dependent type that is pointwise contractible, then we
   ( a : (t : ϕ ) → A t)
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
   : Σ (a' : (t : ψ ) → A t [ϕ t ↦ a t]),
-           ((t : ψ ) → 
-            (restrict I ψ ϕ A a a' t = 
+           ((t : ψ ) →
+            (restrict I ψ ϕ A a a' t =
               first (is-contr-fiberwise-A t))
               [ϕ t ↦ codomain-eq-ext-is-contr I ψ ϕ A a is-contr-fiberwise-A t] )
-  := 
+  :=
     htpy-ext-property
     ( weak-ext-ext)
     ( I )
@@ -605,9 +605,66 @@ In an extension type of a dependent type that is pointwise contractible, then we
   ( f : (t : ψ ) → A t [ϕ t ↦ a t])
   (is-contr-fiberwise-A : (t : ψ ) → is-contr (A t))
   : (t : ψ ) → f t = (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t
-  := \ t → eq-is-contr 
+  := \ t → eq-is-contr
               ( A t)
               ( is-contr-fiberwise-A t)
               ( f t )
               ( restrict I ψ ϕ A a (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
+
+## Right orthogonal fibrations
+
+For every shape inclusion `ϕ ⊂ ψ`,
+we obtain a possible fibrancy condition for a map `α : A' → A`
+in terms of unique extension along `ϕ ⊂ ψ`.
+We say that `α : A' → A` is _j-orthogonal_ to the shape `ϕ ⊂ ψ`
+if the following holds:
+
+
+```rzk title="BW23, Section 3"
+#def is-j-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) )
+```
+
+The j-orthogonality condition is preserved when crossing the inclusion `ϕ ⊂ ψ`
+with another shape `χ`.
+
+
+```rzk title="uncurried version of BW23, Corollary 3.16"
+#def is-j-orthogonal-to-shape-×
+  ( extext : ExtExt)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-jo : is-j-orthogonal-to-shape I ψ ϕ A' A α)
+  : is-j-orthogonal-to-shape
+      ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) A' A α
+  :=
+    \ σ →
+      (
+        ( \ τ (t, s) →
+          ( first (first (is-jo (\ s' → σ (t, s'))))) ( \ s' → τ (t, s')) s,
+          \ τ' → undefined
+
+        ),
+        ( \ τ (t, s) →
+          ( first (first (is-jo (\ s' → σ (t, s'))))) ( \ s' → τ (t, s')) s,
+          \ τ → undefined
+        )
+      )
+
+```

From a73580963559e44746492d56bbc354f7ce9faa17 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Thu, 28 Sep 2023 20:09:00 +0200
Subject: [PATCH 02/15] finish j-orthogonality exp and move to separate file

---
 src/simplicial-hott/04-extension-types.rzk.md |  57 --------
 src/simplicial-hott/04a-jorthogonality.rzk.md | 126 ++++++++++++++++++
 2 files changed, 126 insertions(+), 57 deletions(-)
 create mode 100644 src/simplicial-hott/04a-jorthogonality.rzk.md

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 938c3843..8eaa6e39 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -611,60 +611,3 @@ In an extension type of a dependent type that is pointwise contractible, then we
               ( f t )
               ( restrict I ψ ϕ A a (first (first-4-11 weak-ext-ext I ψ ϕ A a is-contr-fiberwise-A)) t)
 ```
-
-## Right orthogonal fibrations
-
-For every shape inclusion `ϕ ⊂ ψ`,
-we obtain a possible fibrancy condition for a map `α : A' → A`
-in terms of unique extension along `ϕ ⊂ ψ`.
-We say that `α : A' → A` is _j-orthogonal_ to the shape `ϕ ⊂ ψ`
-if the following holds:
-
-
-```rzk title="BW23, Section 3"
-#def is-j-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) )
-```
-
-The j-orthogonality condition is preserved when crossing the inclusion `ϕ ⊂ ψ`
-with another shape `χ`.
-
-
-```rzk title="uncurried version of BW23, Corollary 3.16"
-#def is-j-orthogonal-to-shape-×
-  ( extext : ExtExt)
-  ( J : CUBE)
-  ( χ : J → TOPE)
-  ( I : CUBE)
-  ( ψ : I → TOPE )
-  ( ϕ : ψ → TOPE)
-  ( A' A : U)
-  ( α : A' → A)
-  ( is-jo : is-j-orthogonal-to-shape I ψ ϕ A' A α)
-  : is-j-orthogonal-to-shape
-      ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) A' A α
-  :=
-    \ σ →
-      (
-        ( \ τ (t, s) →
-          ( first (first (is-jo (\ s' → σ (t, s'))))) ( \ s' → τ (t, s')) s,
-          \ τ' → undefined
-
-        ),
-        ( \ τ (t, s) →
-          ( first (first (is-jo (\ s' → σ (t, s'))))) ( \ s' → τ (t, s')) s,
-          \ τ → undefined
-        )
-      )
-
-```
diff --git a/src/simplicial-hott/04a-jorthogonality.rzk.md b/src/simplicial-hott/04a-jorthogonality.rzk.md
new file mode 100644
index 00000000..ce80915a
--- /dev/null
+++ b/src/simplicial-hott/04a-jorthogonality.rzk.md
@@ -0,0 +1,126 @@
+# 4a. Right orthogonal fibrations
+
+This is a literate `rzk` file:
+
+```rzk
+#lang rzk-1
+```
+
+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 _j-orthogonal_ to the shape inclusion `ϕ ⊂ ψ`,
+or a right orthogonal fibration with respect to `ϕ ⊂ ψ`,
+if the square
+```
+(ψ → A') → (ψ → A)
+
+   ↓          ↓
+
+(ϕ → A') → (ϕ → A)
+```
+is homotopy cartesian.
+
+```rzk title="BW23, Section 3"
+#def is-j-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 right orthogonal fibrations
+
+Right orthogonal fibrations with respect to a shape inclusion `ϕ ⊂ ψ`
+are stable under many operations.
+
+### Stability under exponentiation
+
+The j-orthogonality condition is preserved when crossing the inclusion `ϕ ⊂ ψ`
+with another shape `χ`.
+
+```rzk title="uncurried version of BW23, Corollary 3.16"
+#def is-j-orthogonal-to-shape-×
+  ( naiveextext : NaiveExtExt)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-jo : is-j-orthogonal-to-shape I ψ ϕ A' A α)
+  : is-j-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-jo (\ 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-jo (\ s' → σ' (t, s')))))
+                  ( \ s' → α (τ' (t, s'))) s
+              )
+              ( τ')
+              ( \ ( t,s) →
+                ext-htpy-eq I ψ ϕ (\ _ → A') ( \ s' → σ' (t, s'))
+                  ( ( first (first (is-jo (\ s' → σ' (t, s')))))
+                    ( \ s' → α (τ' (t, s')))
+                  )
+                  ( \ s' → τ' (t, s') )
+                  ( ( second (first (is-jo (\ s' → σ' (t, s')))))
+                    ( \ s' → τ' (t, s'))
+                  )
+                  ( s)
+              )
+        )
+      ,
+        ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))])
+            ( t, s) →
+          ( first (second (is-jo (\ 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-jo (\ s' → σ' (t, s')))))
+                      ( \ s' → τ (t, s')) s
+                  )
+              )
+              ( τ)
+              ( \ ( t,s) →
+                ext-htpy-eq I ψ ϕ (\ _ → A) ( \ s' → α (σ' (t, s')))
+                  ( \ s'' →
+                      α ( ( first (second (is-jo (\ s' → σ' (t, s')))))
+                          ( \ s' → τ (t, s'))
+                          (s'')
+                        )
+                  )
+                  ( \ s' → τ (t, s') )
+                  ( ( second ( second (is-jo (\ s' → σ' (t, s')))))
+                    ( \ s' → τ (t, s'))
+                  )
+                  ( s)
+
+              )
+        )
+      )
+```

From adba7ddb996af1e9c71b6c01901328db574fef38 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Thu, 28 Sep 2023 22:52:27 +0200
Subject: [PATCH 03/15] attempt to prove stability under composition (broken)

---
 src/simplicial-hott/04a-jorthogonality.rzk.md | 47 +++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/src/simplicial-hott/04a-jorthogonality.rzk.md b/src/simplicial-hott/04a-jorthogonality.rzk.md
index ce80915a..ddc4acd7 100644
--- a/src/simplicial-hott/04a-jorthogonality.rzk.md
+++ b/src/simplicial-hott/04a-jorthogonality.rzk.md
@@ -43,6 +43,53 @@ is homotopy cartesian.
 Right orthogonal fibrations with respect to a shape inclusion `ϕ ⊂ ψ`
 are stable under many operations.
 
+### Stability under composition
+
+The j-orthogonality is preserved both by composition of maps
+and by composition of shape inclusions.
+
+```rzk title="j-orthogonality for composition of shape inclusions"
+#section j-orthogonal-to-shape-comp
+#variable I : CUBE
+#variable ψ : I → TOPE
+#variable χ : ψ → TOPE
+#variable ϕ : χ → TOPE
+#variables A' A : U
+#variable α : A' → A
+#variable is-jo-ψ-χ : is-j-orthogonal-to-shape I ψ χ A' A α
+#variable is-jo-χ-ϕ : is-j-orthogonal-to-shape I
+                        ( \ t → χ t) ( \ t → ϕ t) A' A α
+
+#def is-j-orthogonal-to-shape-comp
+  : is-j-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
+  :=
+    is-homotopy-cartesian-vertical-pasting
+      ( ϕ → 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-jo-χ-ϕ
+      ( is-homotopy-cartesian-upper-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-jo-ψ-χ τ')
+      )
+
+#end j-orthogonal-to-shape-comp
+```
+
 ### Stability under exponentiation
 
 The j-orthogonality condition is preserved when crossing the inclusion `ϕ ⊂ ψ`

From efcf6761ab5cb51632b7becdc59bdcf985614a27 Mon Sep 17 00:00:00 2001
From: Tashi Walde <tashi.walde@gmail.com>
Date: Fri, 29 Sep 2023 00:20:47 +0200
Subject: [PATCH 04/15] Update src/simplicial-hott/04a-jorthogonality.rzk.md

Co-authored-by: Nikolai Kudasov <fizruk@users.noreply.github.com>
---
 src/simplicial-hott/04a-jorthogonality.rzk.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/simplicial-hott/04a-jorthogonality.rzk.md b/src/simplicial-hott/04a-jorthogonality.rzk.md
index ce80915a..ae734354 100644
--- a/src/simplicial-hott/04a-jorthogonality.rzk.md
+++ b/src/simplicial-hott/04a-jorthogonality.rzk.md
@@ -33,8 +33,8 @@ is homotopy cartesian.
   : U
   :=
     is-homotopy-cartesian
-      ( ϕ → A' ) ( \ σ' → (t : ψ) → A'[ϕ t ↦ σ' t])
-      ( ϕ → A ) ( \ σ → (t : ψ) → A[ϕ t ↦ σ t])
+      ( ϕ → A' ) ( \ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+      ( ϕ → A ) ( \ σ → (t : ψ) → A [ϕ t ↦ σ t])
       ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
 ```
 

From e661c4d9f5ec8163f2ac031a9fcd2d1368e8abcb Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 29 Sep 2023 02:31:48 +0200
Subject: [PATCH 05/15] j-orthogonality for composition of shape inclusions

---
 src/hott/11-homotopy-pullbacks.rzk.md         | 11 ++++
 src/simplicial-hott/04a-jorthogonality.rzk.md | 59 +++++++++++--------
 2 files changed, 47 insertions(+), 23 deletions(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 1e20be0d..3f980d15 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -314,6 +314,17 @@ the corresponding statements about equivalences established above.
         ( is-homotopy-cartesian-upper-to-fibers is-hc-γ-δ a')
         ( is-hc-α-γ a' )
 
+#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-cancellation
   ( is-hc-α-γ : is-homotopy-cartesian A' C' A C α γ )
   ( is-hc-α-δ : is-homotopy-cartesian-vertical-pasted
diff --git a/src/simplicial-hott/04a-jorthogonality.rzk.md b/src/simplicial-hott/04a-jorthogonality.rzk.md
index ddc4acd7..78047363 100644
--- a/src/simplicial-hott/04a-jorthogonality.rzk.md
+++ b/src/simplicial-hott/04a-jorthogonality.rzk.md
@@ -63,29 +63,42 @@ and by composition of shape inclusions.
 #def is-j-orthogonal-to-shape-comp
   : is-j-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
   :=
-    is-homotopy-cartesian-vertical-pasting
-      ( ϕ → 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-jo-χ-ϕ
-      ( is-homotopy-cartesian-upper-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-jo-ψ-χ τ')
-      )
+    \ σ' →
+      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)))
+        ( (
+            ( first ( cofibration-composition I ψ χ ϕ ( \ _ → A') σ'))
+          ,
+            ( first ( cofibration-composition I ψ χ ϕ
+                      ( \ _ → A) ( \ t → α (σ' t))))
+          ),
+          ( \ _ → refl)
+        )
+        ( second ( cofibration-composition I ψ χ ϕ ( \ _ → A') σ'))
+        ( second ( cofibration-composition I ψ χ ϕ ( \ _ → A) ( \ t → α (σ' t))))
+        ( 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-jo-χ-ϕ
+          ( \ _ τ' → is-jo-ψ-χ τ')
+          σ'
+        )
 
 #end j-orthogonal-to-shape-comp
 ```

From e3fb831ceddb4200a28722827e36112a42d85df9 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 29 Sep 2023 11:26:47 +0200
Subject: [PATCH 06/15] j-orthogonal -> right orthogonal; add closure under
 shape comp

---
 ...ity.rzk.md => 04a-right-orthogonal.rzk.md} | 92 ++++++++++---------
 1 file changed, 50 insertions(+), 42 deletions(-)
 rename src/simplicial-hott/{04a-jorthogonality.rzk.md => 04a-right-orthogonal.rzk.md} (68%)

diff --git a/src/simplicial-hott/04a-jorthogonality.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
similarity index 68%
rename from src/simplicial-hott/04a-jorthogonality.rzk.md
rename to src/simplicial-hott/04a-right-orthogonal.rzk.md
index abaf106e..da3425e1 100644
--- a/src/simplicial-hott/04a-jorthogonality.rzk.md
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -6,13 +6,22 @@ This is a literate `rzk` file:
 #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 _j-orthogonal_ to the shape inclusion `ϕ ⊂ ψ`,
-or a right orthogonal fibration with respect to `ϕ ⊂ ψ`,
+We say that `α : A' → A` is _right orthogonal_ to the shape inclusion `ϕ ⊂ ψ`,
 if the square
 ```
 (ψ → A') → (ψ → A)
@@ -22,9 +31,11 @@ if the square
 (ϕ → A') → (ϕ → A)
 ```
 is homotopy cartesian.
+Equivalently,
+we also say that the shape inclusion `ϕ ⊂ ψ` is _left orthogonal_ to the map `α`.
 
 ```rzk title="BW23, Section 3"
-#def is-j-orthogonal-to-shape
+#def is-right-orthogonal-to-shape
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE)
@@ -38,30 +49,31 @@ is homotopy cartesian.
       ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
 ```
 
-## Stability properties of right orthogonal fibrations
-
-Right orthogonal fibrations with respect to a shape inclusion `ϕ ⊂ ψ`
-are stable under many operations.
+## Stability properties of left orthogonal shape inclusions
 
-### Stability under composition
+We fix a map `α : A' → A`.
 
-The j-orthogonality is preserved both by composition of maps
-and by composition of shape inclusions.
+```rzk
+#section left-orthogonal-calculus
 
-```rzk title="j-orthogonality for composition of shape inclusions"
-#section j-orthogonal-to-shape-comp
-#variable I : CUBE
-#variable ψ : I → TOPE
-#variable χ : ψ → TOPE
-#variable ϕ : χ → TOPE
 #variables A' A : U
 #variable α : A' → A
-#variable is-jo-ψ-χ : is-j-orthogonal-to-shape I ψ χ A' A α
-#variable is-jo-χ-ϕ : is-j-orthogonal-to-shape I
-                        ( \ t → χ t) ( \ t → ϕ t) A' A α
+```
 
-#def is-j-orthogonal-to-shape-comp
-  : is-j-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
+### 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
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( χ : ψ → TOPE)
+  ( ϕ : χ → TOPE)
+  ( is-orth-ψ-χ : is-right-orthogonal-to-shape I ψ χ A' A α)
+  ( is-orth-χ-ϕ : is-right-orthogonal-to-shape I ( \ t → χ t) ( \ t → ϕ t) A' A α)
+  : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
   :=
     \ σ' →
       is-equiv-equiv-is-equiv
@@ -95,38 +107,33 @@ and by composition of shape inclusions.
           ( \ σ' t → α (σ' t))
           ( \ _ τ' x → α (τ' x) )
           ( \ _ _ υ' x → α (υ' x) )
-          is-jo-χ-ϕ
-          ( \ _ τ' → is-jo-ψ-χ τ')
+          is-orth-χ-ϕ
+          ( \ _ τ' → is-orth-ψ-χ τ')
           σ'
         )
-
-#end j-orthogonal-to-shape-comp
 ```
 
 ### Stability under exponentiation
 
-The j-orthogonality condition is preserved when crossing the inclusion `ϕ ⊂ ψ`
-with another shape `χ`.
+If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`
+then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
 
 ```rzk title="uncurried version of BW23, Corollary 3.16"
-#def is-j-orthogonal-to-shape-×
-  ( naiveextext : NaiveExtExt)
+#def is-right-orthogonal-to-shape-× uses (naiveextext)
   ( J : CUBE)
   ( χ : J → TOPE)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
-  ( A' A : U)
-  ( α : A' → A)
-  ( is-jo : is-j-orthogonal-to-shape I ψ ϕ A' A α)
-  : is-j-orthogonal-to-shape
+  ( 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-jo (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
+          ( first (first (is-orth (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
         ,
           \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A'[ϕ s ↦ σ' (t,s)]) →
             naiveextext
@@ -134,17 +141,17 @@ with another shape `χ`.
               ( \ _ → A')
               ( \ ( t,s) → σ' (t,s))
               ( \ ( t,s) →
-                ( first (first (is-jo (\ 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-jo (\ s' → σ' (t, s')))))
+                  ( ( first (first (is-orth (\ s' → σ' (t, s')))))
                     ( \ s' → α (τ' (t, s')))
                   )
                   ( \ s' → τ' (t, s') )
-                  ( ( second (first (is-jo (\ s' → σ' (t, s')))))
+                  ( ( second (first (is-orth (\ s' → σ' (t, s')))))
                     ( \ s' → τ' (t, s'))
                   )
                   ( s)
@@ -153,7 +160,7 @@ with another shape `χ`.
       ,
         ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))])
             ( t, s) →
-          ( first (second (is-jo (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
+          ( first (second (is-orth (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
         ,
           \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))]) →
             naiveextext
@@ -161,7 +168,7 @@ with another shape `χ`.
               ( \ _ → A)
               ( \ (t,s) → α (σ' (t,s)))
               ( \ (t,s) →
-                α ( ( first ( second ( is-jo (\ s' → σ' (t, s')))))
+                α ( ( first ( second ( is-orth (\ s' → σ' (t, s')))))
                       ( \ s' → τ (t, s')) s
                   )
               )
@@ -169,18 +176,19 @@ with another shape `χ`.
               ( \ ( t,s) →
                 ext-htpy-eq I ψ ϕ (\ _ → A) ( \ s' → α (σ' (t, s')))
                   ( \ s'' →
-                      α ( ( first (second (is-jo (\ s' → σ' (t, s')))))
+                      α ( ( first (second (is-orth (\ s' → σ' (t, s')))))
                           ( \ s' → τ (t, s'))
                           (s'')
                         )
                   )
                   ( \ s' → τ (t, s') )
-                  ( ( second ( second (is-jo (\ s' → σ' (t, s')))))
+                  ( ( second ( second (is-orth (\ s' → σ' (t, s')))))
                     ( \ s' → τ (t, s'))
                   )
                   ( s)
-
               )
         )
       )
+
+#end left-orthogonal-calculus
 ```

From 494f79fc542d93c19e25e63eef2e95fcb57bcdd3 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 29 Sep 2023 11:32:27 +0200
Subject: [PATCH 07/15] some formatting

---
 .../04a-right-orthogonal.rzk.md               | 48 ++++++++-----------
 1 file changed, 19 insertions(+), 29 deletions(-)

diff --git a/src/simplicial-hott/04a-right-orthogonal.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
index da3425e1..fb43ab01 100644
--- a/src/simplicial-hott/04a-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -31,8 +31,11 @@ if the square
 (ϕ → A') → (ϕ → A)
 ```
 is homotopy cartesian.
-Equivalently,
-we also say that the shape inclusion `ϕ ⊂ ψ` is _left orthogonal_ to the map `α`.
+
+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
@@ -81,20 +84,16 @@ Left orthogonal shape inclusions are preserved under composition.
         ( ( 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 → α (τ' t), \t → α (υ' t)))
-        ( (
-            ( first ( cofibration-composition I ψ χ ϕ ( \ _ → A') σ'))
+        ( ( ( first ( cofibration-composition I ψ χ ϕ ( \ _ → A') σ'))
           ,
             ( first ( cofibration-composition I ψ χ ϕ
                       ( \ _ → A) ( \ t → α (σ' t))))
           ),
-          ( \ _ → refl)
-        )
+          ( \ _ → refl))
         ( second ( cofibration-composition I ψ χ ϕ ( \ _ → A') σ'))
         ( second ( cofibration-composition I ψ χ ϕ ( \ _ → A) ( \ t → α (σ' t))))
         ( is-homotopy-cartesian-vertical-pasting-from-fibers
@@ -109,8 +108,7 @@ Left orthogonal shape inclusions are preserved under composition.
           ( \ _ _ υ' x → α (υ' x) )
           is-orth-χ-ϕ
           ( \ _ τ' → is-orth-ψ-χ τ')
-          σ'
-        )
+          σ')
 ```
 
 ### Stability under exponentiation
@@ -135,56 +133,48 @@ then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
             ( 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')
               ( \ ( t,s) → σ' (t,s))
               ( \ ( t,s) →
                 ( first (first (is-orth (\ s' → σ' (t, s')))))
-                  ( \ s' → α (τ' (t, s'))) 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'))))
                   ( \ s' → τ' (t, s') )
                   ( ( second (first (is-orth (\ s' → σ' (t, s')))))
-                    ( \ 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))])
             ( 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)
               ( \ (t,s) → α (σ' (t,s)))
               ( \ (t,s) →
                 α ( ( first ( second ( is-orth (\ s' → σ' (t, s')))))
-                      ( \ s' → τ (t, s')) 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'')))
                   ( \ s' → τ (t, s') )
                   ( ( second ( second (is-orth (\ s' → σ' (t, s')))))
-                    ( \ s' → τ (t, s'))
-                  )
+                    ( \ s' → τ (t, s')))
                   ( s)
               )
         )

From b4482763372f91fb2202f29f8500470fa435e920 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 29 Sep 2023 15:03:58 +0200
Subject: [PATCH 08/15] functorial instance of cofibration-composition

---
 src/hott/03-equivalences.rzk.md               | 23 ++++++++++++++++
 src/simplicial-hott/04-extension-types.rzk.md | 26 +++++++++++++++++++
 2 files changed, 49 insertions(+)

diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index bc25a2c8..4240f805 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -716,6 +716,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)
@@ -735,6 +748,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)
diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 57b4f759..a1375852 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -162,6 +162,32 @@ 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

From d5075fee0b5c1ab568a5a9e5e8284995bb2f6d21 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Fri, 29 Sep 2023 17:54:53 +0200
Subject: [PATCH 09/15] left cancel for shape inclusions

---
 src/hott/03-equivalences.rzk.md               | 10 +++
 src/hott/11-homotopy-pullbacks.rzk.md         | 23 ++++--
 .../04a-right-orthogonal.rzk.md               | 78 ++++++++++++++-----
 3 files changed, 84 insertions(+), 27 deletions(-)

diff --git a/src/hott/03-equivalences.rzk.md b/src/hott/03-equivalences.rzk.md
index 2496fc17..a1f238ef 100644
--- a/src/hott/03-equivalences.rzk.md
+++ b/src/hott/03-equivalences.rzk.md
@@ -799,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 3f980d15..7b735ff5 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -325,20 +325,27 @@ the corresponding statements about equivalences established above.
       is-hc-α-γ
       ( is-homotopy-cartesian-upper-from-fibers is-fiberwise-hc-γ-δ)
 
-#def is-homotopy-cartesian-lower-cancellation
+#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'))
@@ -387,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/04a-right-orthogonal.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
index fb43ab01..b93c7ff8 100644
--- a/src/simplicial-hott/04a-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -79,7 +79,7 @@ Left orthogonal shape inclusions are preserved under composition.
   : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
   :=
     \ σ' →
-      is-equiv-equiv-is-equiv
+      is-equiv-Equiv-is-equiv
         ( ( t : ψ) → A' [ϕ t ↦ σ' t])
         ( ( t : ψ) → A [ϕ t ↦ α (σ' t)])
         ( \ υ' t → α ( υ' t))
@@ -88,14 +88,8 @@ Left orthogonal shape inclusions are preserved under composition.
         ( Σ ( τ : ( t : χ) → A [ϕ t ↦ α (σ' t)]),
           ( ( t : ψ) → A [χ t ↦ τ t]))
         ( \ (τ', υ') → ( \ t → α (τ' t), \t → α (υ' t)))
-        ( ( ( first ( cofibration-composition I ψ χ ϕ ( \ _ → A') σ'))
-          ,
-            ( first ( cofibration-composition I ψ χ ϕ
-                      ( \ _ → A) ( \ t → α (σ' t))))
-          ),
-          ( \ _ → refl))
-        ( second ( cofibration-composition I ψ χ ϕ ( \ _ → A') σ'))
-        ( second ( cofibration-composition I ψ χ ϕ ( \ _ → A) ( \ t → α (σ' t))))
+        ( cofibration-composition-functorial I ψ χ ϕ
+          ( \ _ → A') ( \ _ → A) ( \ _ → α) σ')
         ( is-homotopy-cartesian-vertical-pasting-from-fibers
           ( ϕ → A' )
           ( \ σ' → (t : χ) → A' [ϕ t ↦ σ' t])
@@ -111,19 +105,65 @@ Left orthogonal shape inclusions are preserved under composition.
           σ')
 ```
 
+### Cancellation laws
+
+If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so is `χ ⊂ ψ`.
+
+```rzk
+#def is-right-orthogonal-to-shape-left-cancel
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( χ : ψ → TOPE)
+  ( ϕ : χ → TOPE)
+  ( is-orth-χ-ϕ : is-right-orthogonal-to-shape I ( \ t → χ t) ( \ t → ϕ t) A' A α)
+  ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α)
+  : 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-χ-ϕ )
+          ( \ (σ' : ϕ → 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-ψ-ϕ σ')
+          )
+          ( \ ( t : ϕ) → τ' t)
+          τ'
+
+
+```
+
 ### Stability under exponentiation
 
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`
 then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
 
-```rzk title="uncurried version of BW23, Corollary 3.16"
+```rzk
 #def is-right-orthogonal-to-shape-× uses (naiveextext)
   ( J : CUBE)
   ( χ : J → TOPE)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
-  ( is-orth : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  ( 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 α
   :=
@@ -131,7 +171,7 @@ then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
       (
         ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))])
             ( t, s) →
-          ( first (first (is-orth (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
+          ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
         ,
           \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) →
             naiveextext
@@ -139,15 +179,15 @@ then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
               ( \ _ → A')
               ( \ ( t,s) → σ' (t,s))
               ( \ ( t,s) →
-                ( first (first (is-orth (\ 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')))))
+                  ( ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                     ( \ s' → α (τ' (t, s'))))
                   ( \ s' → τ' (t, s') )
-                  ( ( second (first (is-orth (\ s' → σ' (t, s')))))
+                  ( ( second (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                     ( \ s' → τ' (t, s')))
                   ( s)
               )
@@ -155,7 +195,7 @@ then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
       ,
         ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))])
             ( t, s) →
-          ( first (second (is-orth (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
+          ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
         ,
           \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) →
             naiveextext
@@ -163,17 +203,17 @@ then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
               ( \ _ → A)
               ( \ (t,s) → α (σ' (t,s)))
               ( \ (t,s) →
-                α ( ( first ( second ( is-orth (\ 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')))))
+                      α ( ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                           ( \ s' → τ (t, s'))
                           (s'')))
                   ( \ s' → τ (t, s') )
-                  ( ( second ( second (is-orth (\ s' → σ' (t, s')))))
+                  ( ( second ( second (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                     ( \ s' → τ (t, s')))
                   ( s)
               )

From 652a5324a8ccf3e2e30e6a19cbd84f956b63650a Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Fri, 29 Sep 2023 17:58:56 +0200
Subject: [PATCH 10/15] remove redundant comments

---
 src/simplicial-hott/04-extension-types.rzk.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 0d037b59..45eb31bd 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -376,7 +376,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)
 
@@ -615,7 +615,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))
 
 ```

From a93b0c1532dbda4f3c85e08d62e0846048944766 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Fri, 29 Sep 2023 18:48:37 +0200
Subject: [PATCH 11/15] add exposition

---
 .../04a-right-orthogonal.rzk.md               | 50 ++++++++++++-------
 1 file changed, 32 insertions(+), 18 deletions(-)

diff --git a/src/simplicial-hott/04a-right-orthogonal.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
index b93c7ff8..307d8739 100644
--- a/src/simplicial-hott/04a-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -57,11 +57,37 @@ if `α : A' → A` is right orthogonal to `ϕ ⊂ ψ`.
 We fix a map `α : A' → A`.
 
 ```rzk
-#section left-orthogonal-calculus
+#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`.
+Apart from the fact that we have to make explicit all arguments,
+the only fact that stops these 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`.
 
 ### Stability under composition
 
@@ -69,13 +95,7 @@ Left orthogonal shape inclusions are preserved under composition.
 
 ```rzk title="right-orthogonality for composition of shape inclusions"
 
-#def is-right-orthogonal-to-shape-comp
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( χ : ψ → TOPE)
-  ( ϕ : χ → TOPE)
-  ( is-orth-ψ-χ : is-right-orthogonal-to-shape I ψ χ A' A α)
-  ( is-orth-χ-ϕ : is-right-orthogonal-to-shape I ( \ t → χ t) ( \ t → ϕ t) A' A α)
+#def is-right-orthogonal-to-shape-comp uses (is-orth-ψ-χ is-orth-χ-ϕ)
   : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α
   :=
     \ σ' →
@@ -110,13 +130,7 @@ Left orthogonal shape inclusions are preserved under composition.
 If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so is `χ ⊂ ψ`.
 
 ```rzk
-#def is-right-orthogonal-to-shape-left-cancel
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( χ : ψ → TOPE)
-  ( ϕ : χ → TOPE)
-  ( is-orth-χ-ϕ : is-right-orthogonal-to-shape I ( \ t → χ t) ( \ t → ϕ t) A' A α)
-  ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ( \ t → ϕ t) A' A α)
+#def is-right-orthogonal-to-shape-left-cancel uses (is-orth-χ-ϕ is-orth-ψ-ϕ)
   : is-right-orthogonal-to-shape I ψ χ A' A α
   :=
     \ τ' →
@@ -148,7 +162,7 @@ If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so i
           ( \ ( t : ϕ) → τ' t)
           τ'
 
-
+#end left-orthogonal-calculus-1
 ```
 
 ### Stability under exponentiation
@@ -158,6 +172,8 @@ then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
 
 ```rzk
 #def is-right-orthogonal-to-shape-× uses (naiveextext)
+  ( A' A : U)
+  ( α : A' → A)
   ( J : CUBE)
   ( χ : J → TOPE)
   ( I : CUBE)
@@ -219,6 +235,4 @@ then so is `χ × ϕ ⊂ χ × ψ` for every other shape `χ`.
               )
         )
       )
-
-#end left-orthogonal-calculus
 ```

From 2d8d8dc55f90267731c77e7b27a3346a70fb0417 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Fri, 29 Sep 2023 18:51:51 +0200
Subject: [PATCH 12/15] right-cancel-with-section (stub; broken)

---
 .../04a-right-orthogonal.rzk.md               | 25 +++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/src/simplicial-hott/04a-right-orthogonal.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
index 307d8739..f49e5c88 100644
--- a/src/simplicial-hott/04a-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -165,6 +165,31 @@ If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so i
 #end left-orthogonal-calculus-1
 ```
 
+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-with-section uses (is-orth-ψ-ϕ)
+  ( is-retract-ψ-χ : 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) )
+      undefined
+      undefined
+
+#end left-orthogonal-calculus-1
+```
+
 ### Stability under exponentiation
 
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`

From 97a415e4ec75bdc072950dde74e842c5755b66c0 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Sat, 30 Sep 2023 11:28:03 +0200
Subject: [PATCH 13/15] cancel with section

---
 .../03-simplicial-type-theory.rzk.md          | 30 ++++++++++
 src/simplicial-hott/04-extension-types.rzk.md |  1 -
 .../04a-right-orthogonal.rzk.md               | 59 ++++++++++++-------
 3 files changed, 67 insertions(+), 23 deletions(-)

diff --git a/src/simplicial-hott/03-simplicial-type-theory.rzk.md b/src/simplicial-hott/03-simplicial-type-theory.rzk.md
index 7351a875..b6452e17 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.
diff --git a/src/simplicial-hott/04-extension-types.rzk.md b/src/simplicial-hott/04-extension-types.rzk.md
index 45eb31bd..e529ab33 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -187,7 +187,6 @@ The original form.
           ( ( \ (_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
diff --git a/src/simplicial-hott/04a-right-orthogonal.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
index f49e5c88..15692a89 100644
--- a/src/simplicial-hott/04a-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -80,8 +80,10 @@ and the three possible right orthogonality conditions.
 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`.
-Apart from the fact that we have to make explicit all arguments,
-the only fact that stops these from being a direct corollary
+
+### Σ over an intermediate shape
+
+The only fact that stops 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
@@ -89,6 +91,31 @@ are not literally equal to the corresponding extension types
 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.
@@ -145,24 +172,9 @@ If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so i
           ( \ _ τ' x → α (τ' x) )
           ( \ _ _ υ' x → α (υ' x) )
           ( is-orth-χ-ϕ )
-          ( \ (σ' : ϕ → 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-ψ-ϕ σ')
-          )
+          (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape)
           ( \ ( t : ϕ) → τ' t)
           τ'
-
-#end left-orthogonal-calculus-1
 ```
 
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`
@@ -170,8 +182,8 @@ and `χ ⊂ ψ` is a (functorial) shape retract,
 then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
 
 ```rzk
-#def is-right-orthogonal-to-shape-right-cancel-with-section uses (is-orth-ψ-ϕ)
-  ( is-retract-ψ-χ : is-functorial-shape-retract I ψ χ)
+#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
@@ -184,8 +196,8 @@ then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
       ( \ σ' t → α (σ' t))
       ( \ _ τ' x → α (τ' x) )
       ( \ _ _ υ' x → α (υ' x) )
-      undefined
-      undefined
+      ( relativize-is-functorial-shape-retract I ψ χ is-fretract-ψ-χ ϕ A' A α)
+      (is-homotopy-cartesian-Σ-is-right-orthogonal-to-shape)
 
 #end left-orthogonal-calculus-1
 ```
@@ -195,6 +207,9 @@ then `ϕ ⊂ ψ` is left orthogonal to `α : A' → A`.
 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)
   ( A' A : U)

From 17be61c3b46dd9b8459fa48ce3c2b5ccf82416b7 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 30 Sep 2023 14:53:38 +0200
Subject: [PATCH 14/15] exact pullbacks of shapes

---
 .../03-simplicial-type-theory.rzk.md          |  2 +-
 src/simplicial-hott/04-extension-types.rzk.md | 25 +++++++++++++++++
 .../04a-right-orthogonal.rzk.md               | 28 ++++++++++++++++++-
 3 files changed, 53 insertions(+), 2 deletions(-)

diff --git a/src/simplicial-hott/03-simplicial-type-theory.rzk.md b/src/simplicial-hott/03-simplicial-type-theory.rzk.md
index b6452e17..9c758c4e 100644
--- a/src/simplicial-hott/03-simplicial-type-theory.rzk.md
+++ b/src/simplicial-hott/03-simplicial-type-theory.rzk.md
@@ -240,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 e529ab33..4bd965fe 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -221,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
diff --git a/src/simplicial-hott/04a-right-orthogonal.rzk.md b/src/simplicial-hott/04a-right-orthogonal.rzk.md
index 15692a89..71e28d00 100644
--- a/src/simplicial-hott/04a-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04a-right-orthogonal.rzk.md
@@ -83,7 +83,7 @@ for left orthogonality of shape inclusion with respect to `α : A' → A`.
 
 ### Σ over an intermediate shape
 
-The only fact that stops these laws from being a direct corollary
+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
@@ -212,6 +212,7 @@ 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)
@@ -276,3 +277,28 @@ and relies on (the naive form of) extension extensionality.
         )
       )
 ```
+
+### 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))
+```

From b445124bcca7826cc20b2c29314990da3fa3f94f Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 30 Sep 2023 15:00:10 +0200
Subject: [PATCH 15/15] relativization and shape-union

---
 .../03-simplicial-type-theory.rzk.md          | 32 ++++++++++++++++++-
 src/simplicial-hott/04-extension-types.rzk.md | 26 ++++++++++++++-
 2 files changed, 56 insertions(+), 2 deletions(-)

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 a1375852..deb9747e 100644
--- a/src/simplicial-hott/04-extension-types.rzk.md
+++ b/src/simplicial-hott/04-extension-types.rzk.md
@@ -187,7 +187,6 @@ The original form.
           ( ( \ (_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
@@ -222,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