From 3605f59bac0cd7b4082754f9abfce5f71f621a14 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 02:28:04 +0200
Subject: [PATCH 1/4] fibers or right orthogonal maps have unique extensions

---
 src/hott/11-homotopy-pullbacks.rzk.md         |  33 ++--
 src/simplicial-hott/03-extension-types.rzk.md | 183 ++++++++++++------
 .../04-right-orthogonal.rzk.md                | 110 ++++++++---
 3 files changed, 232 insertions(+), 94 deletions(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 124ebda2..56ef196f 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -590,26 +590,35 @@ product of all fibers.
 
 ### Fiber product with singleton type
 
-The relative product of `β : B → A` with a map `Unit → A` corresponding to
-`a : A` is nothing but the fiber `fib B A β a`.
+The relative product of `f : B → A` with a map `Unit → A` corresponding to
+`a : A` is nothing but the fiber `fib B A f a`.
 
 ```rzk
-#def compute-relative-product-singleton
-  ( A B : U)
-  ( β : B → A)
+#def compute-pullback-to-Unit
+  ( B A : U)
+  ( f : B → A)
+  ( a : A)
+  : Equiv (fib B A f a) (relative-product A B f Unit (\ unit → a))
+  :=
+    ( ( \ (b , p) → ((b , unit) , p))
+    , ( ( ( ( \ ((b , unit) , p) → (b, p))
+          , ( \ _ → refl))
+        , ( ( \ ((b , unit) , p) → (b, p))
+          , ( \ _ → refl)))))
+
+#def compute-map-pullback-to-Unit
+  ( B A : U)
+  ( f : B → A)
   ( a : A)
   : Equiv-of-maps
-    ( fib B A β a) (Unit) (\ _ → unit)
-    ( relative-product A B β Unit (\ unit → a))
-    ( Unit) ( second-relative-product A B β Unit (\ unit → a))
+    ( fib B A f a) (Unit) (\ _ → unit)
+    ( relative-product A B f Unit (\ unit → a))
+    ( Unit) ( second-relative-product A B f Unit (\ unit → a))
   :=
     ( ( ( ( \ (b , p) → ((b , unit) , p))
         , ( identity Unit))
       , \ _ → refl)
-    , ( ( ( ( \ ((b , unit) , p) → (b, p))
-          , ( \ _ → refl))
-        , ( ( \ ((b , unit) , p) → (b, p))
-          , ( \ _ → refl)))
+    , ( second (compute-pullback-to-Unit B A f a)
       , is-equiv-identity Unit))
 
 ```
diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index 0cfaf9ec..7dc0b91d 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -723,66 +723,6 @@ retraction to `#!rzk ext-htpy-eq`.
   := first (first (extext I ψ ϕ A a f g))
 ```
 
-### Functoriality properties of extension types
-
-By extension extensionality, fiberwise equivalences of extension types define
-equivalences of extension types. For simplicity, we extend from `#!rzk BOT`.
-
-```rzk
-#def equiv-extension-equiv-family uses (extext)
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( A B : ψ → U)
-  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
-  : Equiv ((t : ψ) → A t) ((t : ψ) → B t)
-  :=
-    ( ( \ a t → (first (famequiv t)) (a t)) ,
-      ( ( ( \ b t → (first (first (second (famequiv t)))) (b t)) ,
-          ( \ a →
-            eq-ext-htpy
-              ( I)
-              ( ψ)
-              ( \ t → BOT)
-              ( A)
-              ( \ u → recBOT)
-              ( \ t →
-                first (first (second (famequiv t))) (first (famequiv t) (a t)))
-              ( a)
-              ( \ t → second (first (second (famequiv t))) (a t)))) ,
-        ( ( \ b t → first (second (second (famequiv t))) (b t)) ,
-          ( \ b →
-            eq-ext-htpy
-              ( I)
-              ( ψ)
-              ( \ t → BOT)
-              ( B)
-              ( \ u → recBOT)
-              ( \ t →
-                first (famequiv t) (first (second (second (famequiv t))) (b t)))
-              ( b)
-              ( \ t → second (second (second (famequiv t))) (b t))))))
-```
-
-Similarly, a fiberwise section of a map `(t : ψ) → A t → B t` induces a section
-on extension types
-
-```rzk
-#def has-section-extension-has-section-family uses (naiveextext)
-  ( I : CUBE)
-  ( ψ : I → TOPE)
-  ( A B : ψ → U)
-  ( f : ( t : ψ) → A t → B t)
-  ( has-fiberwise-section-f : (t : ψ) → has-section (A t ) (B t) (f t))
-  : has-section ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t))
-  :=
-    ( ( \ b t → first (has-fiberwise-section-f t) (b t))
-    , \ b →
-      ( naiveextext I ψ (\ _ → BOT) B (\ _ → recBOT)
-        ( \ t → f t (first (has-fiberwise-section-f t) (b t)))
-        ( \ t → b t)
-        ( \ t → second (has-fiberwise-section-f t) (b t))))
-```
-
 ### Homotopy extension property
 
 We have a homotopy extension property.
@@ -1274,3 +1214,126 @@ The converse is of course trivial.
 
 #end general-extension-types
 ```
+
+## Functoriality of extension types
+
+For simplicity, we only consider extesions of `#!rzk BOT`.
+
+For each map `f : A → B` and each shape inclusion `ϕ ⊂ ψ`,
+we have a commutative square.
+
+```
+(ψ → A') → (ψ → A)
+
+   ↓          ↓
+
+(ϕ → A') → (ϕ → A)
+```
+
+We can view it as a map of maps either vertically or horizontally.
+
+```rzk
+#def map-of-restriction-maps
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( f : (t : ψ) → A t → B t)
+  : map-of-maps
+    ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
+    ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
+  :=
+    ( ( ( \ a t → f t (a t))
+      , ( \ a t → f t (a t)))
+    , \ _ → refl)
+
+#def map-of-map-extension-type
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( f : (t : ψ) → A t → B t)
+  : map-of-maps
+    ( (t : ψ) → A t) ( (t : ψ) → B t) (\ a t → f t (a t))
+    ( (t : ϕ) → A t) ( (t : ϕ) → B t) (\ a t → f t (a t))
+  :=
+    ( ( ( \ a t → a t)
+      , ( \ b t → b t))
+    , \ _ → refl)
+```
+
+It follows from extension extensionality that if `f : A → B` is an equivalence,
+then so is the map of maps `map-of-restriction-maps`.
+
+```rzk
+#def is-equiv-extension-is-equiv-family uses (extext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( A B : ψ → U)
+  ( f : (t : ψ) → (A t) → (B t))
+  ( is-equiv-f : (t : ψ) → is-equiv (A t) (B t) (f t))
+  : is-equiv ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t))
+  :=  ( ( ( \ b t → (first (first (is-equiv-f t))) (b t))
+        , ( \ a →
+            eq-ext-htpy I ψ ( \ t → BOT)
+              ( A)
+              ( \ u → recBOT)
+              ( \ t → first (first (is-equiv-f t)) (f t (a t)))
+              ( a)
+              ( \ t → second (first (is-equiv-f t)) (a t))))
+      , ( ( \ b t → first (second (is-equiv-f t)) (b t))
+        , ( \ b →
+            eq-ext-htpy I ψ ( \ t → BOT)
+              ( B)
+              ( \ u → recBOT)
+              ( \ t → f t (first (second (is-equiv-f t)) (b t)))
+              ( b)
+              ( \ t → second (second (is-equiv-f t)) (b t)))))
+
+#def equiv-extension-equiv-family uses (extext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( A B : ψ → U)
+  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
+  : Equiv ((t : ψ) → A t) ((t : ψ) → B t)
+  :=
+    ( ( \ a t → first ( famequiv t) (a t))
+    , is-equiv-extension-is-equiv-family I ψ A B
+      ( \ t → first (famequiv t))
+      ( \ t → second (famequiv t)))
+
+#def equiv-of-restriction-maps-equiv-family uses (extext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A B : ψ → U)
+  ( famequiv : (t : ψ) → (Equiv (A t) (B t)))
+  : Equiv-of-maps
+    ( (t : ψ) → A t) ( (t : ϕ) → A t)  (\ a t → a t)
+    ( (t : ψ) → B t) ( (t : ϕ) → B t)  (\ b t → b t)
+  :=
+    ( map-of-restriction-maps I ψ ϕ A B (\ t → first (famequiv t))
+    , ( second (equiv-extension-equiv-family I ψ A B famequiv)
+      , second ( equiv-extension-equiv-family I
+                 (\ t → ϕ t) (\ t → A t) (\ t → B t) (\ t → famequiv t))))
+```
+
+Similarly, a fiberwise section of a map `(t : ψ) → A t → B t` induces a section
+on extension types.
+
+```rzk
+#def has-section-extension-has-section-family uses (naiveextext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( A B : ψ → U)
+  ( f : ( t : ψ) → A t → B t)
+  ( has-fiberwise-section-f : (t : ψ) → has-section (A t ) (B t) (f t))
+  : has-section ((t : ψ) → A t) ((t : ψ) → B t) ( \ a t → f t (a t))
+  :=
+    ( ( \ b t → first (has-fiberwise-section-f t) (b t))
+    , \ b →
+      ( naiveextext I ψ (\ _ → BOT) B (\ _ → recBOT)
+        ( \ t → f t (first (has-fiberwise-section-f t) (b t)))
+        ( \ t → b t)
+        ( \ t → second (has-fiberwise-section-f t) (b t))))
+```
diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 0b25eace..393c7e3c 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -24,8 +24,8 @@ 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
+We say that `α : A' → A` is **right orthogonal** to the shape inclusion
+`ϕ ⊂ ψ`, if the square
 
 ```
 (ψ → A') → (ψ → A)
@@ -38,8 +38,9 @@ if the square
 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 `ϕ ⊂ ψ`.
+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
@@ -621,7 +622,7 @@ follows for the former.
 Then we can deduce that right orthogonal maps are preserved under pullback:
 
 ```rzk
-#def is-right-orthoponal-pullback-to-shape uses (extext is-orth-ψ-ϕ-α)
+#def is-right-orthogonal-pullback-to-shape uses (extext is-orth-ψ-ϕ-α B f)
   : is-right-orthogonal-to-shape I ψ ϕ
     ( relative-product A A' α B f) ( B)
     ( second-relative-product A A' α B f)
@@ -728,16 +729,16 @@ equivalence.
     is-equiv (ψ → A) (ϕ → A) ( \ τ t → τ t)
 ```
 
-We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`
+We can ask that the terminal map `A → Unit` is right orthogonal to `ϕ ⊂ ψ`.
 
 ```rzk
-#def is-right-orthogonal-to-shape-terminal-map
+#def is-right-orthogonal-terminal-map
   : U
   :=
     is-right-orthogonal-to-shape I ψ ϕ A Unit (terminal-map A)
 ```
 
-### Proof of first alternative characterization
+### Unique extensions types are local types
 
 The equivalence between `is-local-type` and `has-unique-extensions` follows
 straightforwardly from the fact that for every `σ : ϕ → A` we have an
@@ -862,25 +863,49 @@ extensions for every shape inclusion `ϕ ⊂ ψ`.
   : has-unique-extensions I ψ ϕ Unit
   := has-unique-extensions-is-contr Unit is-contr-Unit
 
+```
+
+Unique extension types are closed under equivalence.
+
+```rzk
+#def is-local-type-equiv-is-local-type uses (extext)
+  ( A' A : U)
+  ( A'≃A : Equiv A' A)
+  : is-local-type I ψ ϕ A → is-local-type I ψ ϕ A'
+  :=
+    is-equiv-Equiv-is-equiv
+      ( ψ → A') ( ϕ → A') ( \ τ' t → τ' t)
+      ( ψ → A)  ( ϕ → A)  ( \ τ t → τ t)
+      ( equiv-of-restriction-maps-equiv-family extext I ψ ϕ
+        ( \ _ → A') ( \ _ → A) ( \ _ → A'≃A))
+
+#def has-unique-extensions-equiv-has-unique-extensions uses (extext)
+  ( A' A : U)
+  ( (α , is-equiv-α) : Equiv A' A)
+  : has-unique-extensions I ψ ϕ A → has-unique-extensions I ψ ϕ A'
+  :=
+    has-unique-extensions-right-orthogonal-has-unique-extensions A' A α
+    ( is-right-orthogonal-is-equiv-to-shape I ψ ϕ A' A α is-equiv-α)
+
 #end stability-properties-local-types
 ```
 
-### Proof of second alternative characterization
+### Unique extension types are types with right orthogonal terminal map
 
 Next we prove the logical equivalence between `has-unique-extensions` and
-`is-right-orthogonal-to-shape-terminal-map`. This follows directly from the fact
+`is-right-orthogonal-terminal-map`. This follows directly from the fact
 that `Unit` has unique extensions (using `weakextext : WeakExtExt`).
 
 ```rzk
-#section is-right-orthogonal-to-shape-terminal-map
+#section is-right-orthogonal-terminal-map
 #variable I : CUBE
 #variable ψ : I → TOPE
 #variable ϕ : ψ → TOPE
 #variable A : U
 
-#def has-unique-extensions-is-right-orthogonal-to-shape-terminal-map
+#def has-unique-extensions-is-right-orthogonal-terminal-map
   uses (weakextext)
-  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A)
+  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : has-unique-extensions I ψ ϕ A
   :=
     has-unique-extensions-right-orthogonal-has-unique-extensions
@@ -888,31 +913,72 @@ that `Unit` has unique extensions (using `weakextext : WeakExtExt`).
     ( is-orth-ψ-ϕ-tm-A)
     ( has-unique-extensions-Unit I ψ ϕ)
 
-#def is-right-orthogonal-to-shape-terminal-map-has-unique-extensions
+#def has-unique-extensions-is-right-orthogonal-a-terminal-map
+  uses (weakextext)
+  ( tm : A → Unit)
+  ( is-orth-ψ-ϕ-tm : is-right-orthogonal-to-shape I ψ ϕ A Unit tm)
+  : has-unique-extensions I ψ ϕ A
+  :=
+    has-unique-extensions-right-orthogonal-has-unique-extensions
+      I ψ ϕ A Unit tm
+    ( is-orth-ψ-ϕ-tm)
+    ( has-unique-extensions-Unit I ψ ϕ)
+
+#def is-right-orthogonal-terminal-map-has-unique-extensions
   uses (weakextext)
   ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
-  : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A
+  : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
     is-right-orthogonal-have-unique-extensions I ψ ϕ A Unit
     ( has-ue-ψ-ϕ-A) ( has-unique-extensions-Unit I ψ ϕ)
     ( terminal-map A)
 
-#def is-right-orthogonal-to-shape-terminal-map-is-local-type
+#def is-right-orthogonal-terminal-map-is-local-type
   uses (weakextext)
   ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
-  : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A
+  : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
-    is-right-orthogonal-to-shape-terminal-map-has-unique-extensions
+    is-right-orthogonal-terminal-map-has-unique-extensions
     ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
 
-#def is-local-type-is-right-orthogonal-to-shape-terminal-map
+#def is-local-type-is-right-orthogonal-terminal-map
   uses (weakextext)
-  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-to-shape-terminal-map I ψ ϕ A)
+  ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : is-local-type I ψ ϕ A
   :=
     is-local-type-has-unique-extensions I ψ ϕ A
-    ( has-unique-extensions-is-right-orthogonal-to-shape-terminal-map
+    ( has-unique-extensions-is-right-orthogonal-terminal-map
       ( is-orth-ψ-ϕ-tm-A))
 
-#end is-right-orthogonal-to-shape-terminal-map
+#end is-right-orthogonal-terminal-map
+```
+
+## Fibers of right orthogonal maps
+
+Let `α : A' → A` be right orthogonal to `ϕ ⊂ ψ`.
+Then every fiber of `α` has unique extensions along `ϕ ⊂ ψ`.
+This follows immediately since the fibers of `α`
+are just the relative products of `α : A' → A`
+with the maps `a : Unit → A` from the unit type.
+
+```rzk
+#def has-fiberwise-unique-extensions-is-right-orthogonal-to-shape
+  uses (extext weakextext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-orth-ψ-ϕ-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  ( a : A)
+  : has-unique-extensions I ψ ϕ (fib A' A α a)
+  :=
+    has-unique-extensions-equiv-has-unique-extensions I ψ ϕ
+    ( fib A' A α a)
+    ( relative-product A A' α Unit (\ unit → a))
+    ( compute-pullback-to-Unit A' A α a)
+    ( has-unique-extensions-is-right-orthogonal-terminal-map I ψ ϕ
+      ( relative-product A A' α Unit (\ unit → a))
+      ( is-right-orthogonal-pullback-to-shape I ψ ϕ A' A α
+        ( is-orth-ψ-ϕ-α) ( Unit) (\ unit → a)))
 ```

From 214bd61fdce7843f072a62b869261eb40f85b2d0 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 02:46:45 +0200
Subject: [PATCH 2/4] maps between ue-types have ue-fibers

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

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 393c7e3c..fcbe9a4a 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -982,3 +982,24 @@ with the maps `a : Unit → A` from the unit type.
       ( is-right-orthogonal-pullback-to-shape I ψ ϕ A' A α
         ( is-orth-ψ-ϕ-α) ( Unit) (\ unit → a)))
 ```
+
+Corollary:
+Given two types  `A'` and `A` with unique extensions w.r.t. `ϕ ⊂ ψ`,
+every fiber of every map `α : A' → A` also has unique extensions.
+
+```rzk
+#def has-fiberwise-unique-extensions-have-unique-extensions
+  uses (extext weakextext)
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  ( has-ue-ψ-ϕ-A' : has-unique-extensions I ψ ϕ A')
+  ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
+  : (a : A) → has-unique-extensions I ψ ϕ (fib A' A α a)
+  :=
+    has-fiberwise-unique-extensions-is-right-orthogonal-to-shape I ψ ϕ A' A α
+    ( is-right-orthogonal-have-unique-extensions I ψ ϕ A' A
+      ( has-ue-ψ-ϕ-A') ( has-ue-ψ-ϕ-A) ( α))
+```

From 4457bc448f6880b063a76642af0ea00f74a995a5 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 03:05:52 +0200
Subject: [PATCH 3/4] autoformat

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

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index fcbe9a4a..12154ce0 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -24,8 +24,8 @@ 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
+We say that `α : A' → A` is **right orthogonal** to the shape inclusion `ϕ ⊂ ψ`,
+if the square
 
 ```
 (ψ → A') → (ψ → A)
@@ -38,9 +38,8 @@ We say that `α : A' → A` is **right orthogonal** to the shape inclusion
 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 `ϕ ⊂ ψ`.
+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
@@ -893,8 +892,8 @@ Unique extension types are closed under equivalence.
 ### Unique extension types are types with right orthogonal terminal map
 
 Next we prove the logical equivalence between `has-unique-extensions` and
-`is-right-orthogonal-terminal-map`. This follows directly from the fact
-that `Unit` has unique extensions (using `weakextext : WeakExtExt`).
+`is-right-orthogonal-terminal-map`. This follows directly from the fact that
+`Unit` has unique extensions (using `weakextext : WeakExtExt`).
 
 ```rzk
 #section is-right-orthogonal-terminal-map
@@ -955,11 +954,10 @@ that `Unit` has unique extensions (using `weakextext : WeakExtExt`).
 
 ## Fibers of right orthogonal maps
 
-Let `α : A' → A` be right orthogonal to `ϕ ⊂ ψ`.
-Then every fiber of `α` has unique extensions along `ϕ ⊂ ψ`.
-This follows immediately since the fibers of `α`
-are just the relative products of `α : A' → A`
-with the maps `a : Unit → A` from the unit type.
+Let `α : A' → A` be right orthogonal to `ϕ ⊂ ψ`. Then every fiber of `α` has
+unique extensions along `ϕ ⊂ ψ`. This follows immediately since the fibers of
+`α` are just the relative products of `α : A' → A` with the maps `a : Unit → A`
+from the unit type.
 
 ```rzk
 #def has-fiberwise-unique-extensions-is-right-orthogonal-to-shape
@@ -983,8 +981,7 @@ with the maps `a : Unit → A` from the unit type.
         ( is-orth-ψ-ϕ-α) ( Unit) (\ unit → a)))
 ```
 
-Corollary:
-Given two types  `A'` and `A` with unique extensions w.r.t. `ϕ ⊂ ψ`,
+Corollary: Given two types `A'` and `A` with unique extensions w.r.t. `ϕ ⊂ ψ`,
 every fiber of every map `α : A' → A` also has unique extensions.
 
 ```rzk

From 7b9622889745cd5efb39d0260cdd568c779a5975 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-Air.fritz.box>
Date: Sat, 14 Oct 2023 03:10:15 +0200
Subject: [PATCH 4/4] autoformat more

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

diff --git a/src/simplicial-hott/03-extension-types.rzk.md b/src/simplicial-hott/03-extension-types.rzk.md
index 7dc0b91d..b96a608a 100644
--- a/src/simplicial-hott/03-extension-types.rzk.md
+++ b/src/simplicial-hott/03-extension-types.rzk.md
@@ -1219,8 +1219,8 @@ The converse is of course trivial.
 
 For simplicity, we only consider extesions of `#!rzk BOT`.
 
-For each map `f : A → B` and each shape inclusion `ϕ ⊂ ψ`,
-we have a commutative square.
+For each map `f : A → B` and each shape inclusion `ϕ ⊂ ψ`, we have a commutative
+square.
 
 ```
 (ψ → A') → (ψ → A)