From fff8adbbac354c075dc11ba3d8b5e249eead1a6c Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 13:42:14 +0100
Subject: [PATCH 01/11] every discrete type is rezk

---
 src/simplicial-hott/10-rezk-types.rzk.md | 147 ++++++++++++++++++-----
 1 file changed, 117 insertions(+), 30 deletions(-)

diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md
index 0c426fec..c34c5181 100644
--- a/src/simplicial-hott/10-rezk-types.rzk.md
+++ b/src/simplicial-hott/10-rezk-types.rzk.md
@@ -692,54 +692,61 @@ The predicate `#!rzk is-iso-arrow` is a proposition.
 
 ## Rezk types
 
-A Segal type $A$ is a Rezk type just when, for all `#!rzk x y : A`, the natural
-map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence.
+For every `x : A`, the identity arrow `id-hom A x : hom A x x` is an
+isomorphism.
 
 ```rzk
+#def is-iso-arrow-id-hom
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( x : A)
+  : is-iso-arrow A is-segal-A x x (id-hom A x)
+  :=
+    ( ( id-hom A x , comp-id-is-segal A is-segal-A x x (id-hom A x))
+    , ( id-hom A x , comp-id-is-segal A is-segal-A x x (id-hom A x)))
+
 #def iso-id-arrow
-  (A : U)
-  (is-segal-A : is-segal A)
+  ( A : U)
+  ( is-segal-A : is-segal A)
   : (x : A) → Iso A is-segal-A x x
+  := \ x → ( id-hom A x , is-iso-arrow-id-hom A is-segal-A x)
+```
+
+More generally, every path induces an isomorphism.
+
+```rzk
+#def is-iso-arrow-hom-eq
+  ( A : U)
+  ( is-segal-A : is-segal A)
+  ( x y : A)
+  : ( p : x = y)
+  → is-iso-arrow A is-segal-A x y (hom-eq A x y p)
   :=
-    \ x →
-    (
-    (id-hom A x) ,
-    (
-    (
-      (id-hom A x) ,
-      (id-comp-is-segal A is-segal-A x x (id-hom A x))
-    ) ,
-    (
-      (id-hom A x) ,
-      (id-comp-is-segal A is-segal-A x x (id-hom A x))
-    )
-      )
-  )
+    ind-path A x
+    ( \ y' p' → is-iso-arrow A is-segal-A x y' (hom-eq A x y' p'))
+    ( is-iso-arrow-id-hom A is-segal-A x)
+    ( y)
 
 #def iso-eq
   ( A : U)
   ( is-segal-A : is-segal A)
   ( x y : A)
   : (x = y) → Iso A is-segal-A x y
-  :=
-    \ p →
-    ind-path
-      ( A)
-      ( x)
-      ( \ y' p' → Iso A is-segal-A x y')
-      ( iso-id-arrow A is-segal-A x)
-      ( y)
-      ( p)
+  := \ p → (hom-eq A x y p , is-iso-arrow-hom-eq A is-segal-A x y p)
 ```
 
+A Segal type `A` is a Rezk type just when, for all `#!rzk x y : A`, this natural
+map from `#!rzk x = y` to `#!rzk Iso A is-segal-A x y` is an equivalence.
+
 ```rzk title="RS17, Definition 10.6"
 #def is-rezk
   ( A : U)
   : U
   :=
-    Σ ( is-segal-A : is-segal A) ,
-      (x : A) → (y : A) →
-        is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y)
+    Σ ( is-segal-A : is-segal A)
+    , ( (x : A)
+      → (y : A)
+      → is-equiv (x = y) (Iso A is-segal-A x y) (iso-eq A is-segal-A x y))
 ```
 
 The inverse to `#!rzk iso-eq` for a Rezk type.
@@ -836,3 +843,83 @@ arrows.
       ( y)
       ( e)
 ```
+
+## Isomorphisms in discrete types
+
+In a discrete type every arrow is an isomorphisms. This is a straightforward
+path induction since every identity arrow is an isomorphism. Note that with
+extension extensionality, `is-discrete A` implies `is-segal A` but we state the
+first statement in a way that works without it.
+
+```rzk
+#def has-iso-arrows-is-segal-is-discrete
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  ( is-segal-A : is-segal A)
+  ( x y : A)
+  : ( f : hom A x y)
+  → ( is-iso-arrow A is-segal-A x y f)
+  :=
+    ind-has-section-equiv (x =_{A} y) (hom A x y)
+    ( hom-eq A x y , is-discrete-A x y)
+    ( \ f → is-iso-arrow A is-segal-A x y f)
+    ( ind-path A x
+      ( \ y' p → is-iso-arrow A is-segal-A x y' (hom-eq A x y' p))
+      ( is-iso-arrow-id-hom A is-segal-A x)
+      ( y))
+
+#def has-iso-arrows-is-discrete uses (extext)
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  ( x y : A)
+  ( f : hom A x y)
+  : ( is-iso-arrow A (is-segal-is-discrete extext A is-discrete-A)
+      x y f)
+  :=
+    has-iso-arrows-is-segal-is-discrete A
+    is-discrete-A
+    ( is-segal-is-discrete extext A is-discrete-A)
+    ( x) (y) (f)
+
+#def is-equiv-hom-iso-is-discrete uses (extext)
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  ( x y : A)
+  : is-equiv
+    ( Iso A (is-segal-is-discrete extext A is-discrete-A)
+      x y)
+    ( hom A x y)
+    ( \ (f , _) → f)
+  :=
+    is-equiv-projection-contractible-fibers
+    ( hom A x y) (is-iso-arrow A (is-segal-is-discrete extext A is-discrete-A) x y)
+    ( \ f →
+      is-contr-is-inhabited-is-prop
+      ( is-iso-arrow A (is-segal-is-discrete extext A is-discrete-A) x y f)
+      ( is-prop-is-iso-arrow A
+        ( is-segal-is-discrete extext A is-discrete-A)
+        ( x) (y) (f))
+      ( has-iso-arrows-is-discrete A is-discrete-A x y f))
+```
+
+As a corollary we obtain that every discrete type is Rezk.
+
+```rzk
+#def is-rezk-is-discrete uses (extext)
+  ( A : U)
+  ( is-discrete-A : is-discrete A)
+  : is-rezk A
+  :=
+  ( is-segal-is-discrete extext A is-discrete-A
+  , ( \ x y →
+      is-equiv-right-factor
+      ( x = y)
+      ( Iso A (is-segal-is-discrete extext A is-discrete-A)
+        x y)
+      ( hom A x y)
+      ( iso-eq A (is-segal-is-discrete extext A is-discrete-A)
+        x y)
+      ( \ (f , _) → f)
+      ( is-equiv-hom-iso-is-discrete A is-discrete-A x y)
+      ( is-discrete-A x y)))
+```

From 2bf8d8b35ee36a824e39c98335fcfe8a3656f8e8 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 14:11:16 +0100
Subject: [PATCH 02/11] contractible and discrete types are Rezk

---
 .../04-right-orthogonal.rzk.md                | 32 +++++++++++--------
 src/simplicial-hott/05-segal-types.rzk.md     |  5 ++-
 src/simplicial-hott/07-discrete.rzk.md        | 20 ++++++++++++
 src/simplicial-hott/10-rezk-types.rzk.md      | 22 +++++++++++--
 4 files changed, 61 insertions(+), 18 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 46b5e1ee..ed7818d1 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -15,7 +15,6 @@ function extensionality:
 #assume naiveextext : NaiveExtExt
 #assume extext : ExtExt
 #assume funext : FunExt
-#assume weakextext : WeakExtExt
 ```
 
 ## Right orthogonal maps with respect to shapes
@@ -948,18 +947,25 @@ Weak extension extensionality says that every contractible type has unique
 extensions for every shape inclusion `ϕ ⊂ ψ`.
 
 ```rzk
-#def has-unique-extensions-is-contr uses (weakextext)
+#def has-unique-extensions-is-contr uses (extext)
   ( C : U)
   ( is-contr-C : is-contr C)
   : has-unique-extensions I ψ ϕ C
   :=
-    weakextext I ψ ϕ
+    weakextext-extext extext I ψ ϕ
     ( \ _ → C) ( \ _ → is-contr-C)
 
-#def has-unique-extensions-Unit uses (weakextext)
+#def is-local-type-is-contr uses (extext)
+  ( C : U)
+  ( is-contr-C : is-contr C)
+  : is-local-type I ψ ϕ C
+  :=
+    is-local-type-has-unique-extensions I ψ ϕ C
+    ( has-unique-extensions-is-contr C is-contr-C)
+
+#def has-unique-extensions-Unit uses (extext)
   : has-unique-extensions I ψ ϕ Unit
   := has-unique-extensions-is-contr Unit is-contr-Unit
-
 ```
 
 Unique extension types are closed under equivalence.
@@ -991,7 +997,7 @@ Unique extension types are closed under equivalence.
 
 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`).
+`Unit` has unique extensions (using `extext`).
 
 ```rzk
 #section is-right-orthogonal-terminal-map
@@ -1001,7 +1007,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
 #variable A : U
 
 #def has-unique-extensions-is-right-orthogonal-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : has-unique-extensions I ψ ϕ A
   :=
@@ -1011,7 +1017,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-Unit I ψ ϕ)
 
 #def has-unique-extensions-is-right-orthogonal-a-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( tm : A → Unit)
   ( is-orth-ψ-ϕ-tm : is-right-orthogonal-to-shape I ψ ϕ A Unit tm)
   : has-unique-extensions I ψ ϕ A
@@ -1022,7 +1028,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-Unit I ψ ϕ)
 
 #def is-right-orthogonal-terminal-map-has-unique-extensions
-  uses (weakextext)
+  uses (extext)
   ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
   : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
@@ -1031,7 +1037,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( terminal-map A)
 
 #def is-right-orthogonal-terminal-map-is-local-type
-  uses (weakextext)
+  uses (extext)
   ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
   : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
@@ -1039,7 +1045,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
 
 #def is-local-type-is-right-orthogonal-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : is-local-type I ψ ϕ A
   :=
@@ -1059,7 +1065,7 @@ from the unit type.
 
 ```rzk
 #def has-fiberwise-unique-extensions-is-right-orthogonal-to-shape
-  uses (extext weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -1084,7 +1090,7 @@ every fiber of every map `α : A' → A` also has unique extensions.
 
 ```rzk
 #def has-fiberwise-unique-extensions-have-unique-extensions
-  uses (extext weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index fb2aaccc..775804d1 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -1910,7 +1910,7 @@ Segal type. This is an instance of a general statement about types with unique
 extensions for the shape inclusion `Λ ⊂ Δ²`.
 
 ```rzk
-#def is-fiberwise-segal-are-segal uses (extext weakextext)
+#def is-fiberwise-segal-are-segal uses (extext)
   ( A B : U)
   ( f : A → B)
   ( is-segal-A : is-segal A)
@@ -1919,8 +1919,7 @@ extensions for the shape inclusion `Λ ⊂ Δ²`.
   : is-segal (fib A B f b)
   :=
     is-segal-has-unique-inner-extensions (fib A B f b)
-    ( has-fiberwise-unique-extensions-have-unique-extensions
-      extext weakextext
+    ( has-fiberwise-unique-extensions-have-unique-extensions extext
       ( 2 × 2) (Δ²) (\ t → Λ t) A B f
       ( has-unique-inner-extensions-is-segal A is-segal-A)
       ( has-unique-inner-extensions-is-segal B is-segal-B)
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index 7e179143..67f0fe2d 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -336,6 +336,26 @@ For instance, the arrow type of a discrete type is discrete.
   := is-discrete-extension-type 2 Δ¹ (\ _ → A) (\ _ → is-discrete-A)
 ```
 
+## Contractible types are discrete
+
+Every contractible type is automatically discrete.
+
+```rzk
+#def is-discrete-is-contr uses (extext)
+  ( A : U)
+  : is-contr A → is-discrete A
+  :=
+  \ is-contr-A →
+    ( is-discrete-is-Δ¹-local A
+      ( is-Δ¹-local-is-left-local A
+        ( is-local-type-is-contr extext 2 Δ¹ (\ t → t ≡ 0₂) A
+          is-contr-A)))
+
+#def is-discrete-Unit uses (extext)
+  : is-discrete Unit
+  := is-discrete-is-contr Unit (is-contr-Unit)
+```
+
 ## Discrete types are Segal types
 
 Discrete types are automatically Segal types.
diff --git a/src/simplicial-hott/10-rezk-types.rzk.md b/src/simplicial-hott/10-rezk-types.rzk.md
index c34c5181..d357c161 100644
--- a/src/simplicial-hott/10-rezk-types.rzk.md
+++ b/src/simplicial-hott/10-rezk-types.rzk.md
@@ -902,14 +902,16 @@ first statement in a way that works without it.
       ( has-iso-arrows-is-discrete A is-discrete-A x y f))
 ```
 
+### Discrete types are Rezk
+
 As a corollary we obtain that every discrete type is Rezk.
 
 ```rzk
 #def is-rezk-is-discrete uses (extext)
   ( A : U)
-  ( is-discrete-A : is-discrete A)
-  : is-rezk A
+  : is-discrete A → is-rezk A
   :=
+  \ is-discrete-A →
   ( is-segal-is-discrete extext A is-discrete-A
   , ( \ x y →
       is-equiv-right-factor
@@ -923,3 +925,19 @@ As a corollary we obtain that every discrete type is Rezk.
       ( is-equiv-hom-iso-is-discrete A is-discrete-A x y)
       ( is-discrete-A x y)))
 ```
+
+In particular, every contractible type is Rezk
+
+```rzk
+#def is-rezk-is-contr uses (extext)
+  ( A : U)
+  : is-contr A → is-rezk A
+  :=
+  \ is-contr-A →
+    ( is-rezk-is-discrete A
+      ( is-discrete-is-contr extext A is-contr-A))
+
+#def is-rezk-Unit uses (extext)
+  : is-rezk Unit
+  := is-rezk-is-contr Unit (is-contr-Unit)
+```

From 20394c76cff7253a7aac5e540da5105f4ee49824 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 16:29:13 +0100
Subject: [PATCH 03/11] reorganize inner horn being left anodyne

---
 .../04-right-orthogonal.rzk.md                |  59 ++---
 src/simplicial-hott/05-segal-types.rzk.md     |  55 +++--
 src/simplicial-hott/07-discrete.rzk.md        | 209 +++++++++++++++++-
 src/simplicial-hott/08-covariant.rzk.md       | 167 +-------------
 src/simplicial-hott/13-limits.rzk.md          |  11 +-
 5 files changed, 293 insertions(+), 208 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index a572e002..9c361528 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -12,10 +12,8 @@ Some of the definitions in this file rely on extension extensionality or
 function extensionality:
 
 ```rzk
-#assume naiveextext : NaiveExtExt
 #assume extext : ExtExt
 #assume funext : FunExt
-#assume weakextext : WeakExtExt
 ```
 
 ## Right orthogonal maps with respect to shapes
@@ -328,7 +326,7 @@ The following proof uses a lot of currying and uncurrying and relies extension
 extensionality.
 
 ```rzk
-#def is-right-orthogonal-to-shape-product uses (naiveextext)
+#def is-right-orthogonal-to-shape-product uses (extext)
   ( A' A : U)
   ( α : A' → A)
   ( J : CUBE)
@@ -345,7 +343,7 @@ extensionality.
             ( t, s) →
           ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
         , \ ( τ' : ( (t , s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t , s)]) →
-            naiveextext
+            naiveextext-extext extext
               ( J × I) ( \ (t , s) → χ t ∧ ψ s) ( \ (t , s) → χ t ∧ ϕ s)
               ( \ _ → A')
               ( \ ( t,s) → σ' (t , s))
@@ -365,7 +363,7 @@ extensionality.
             ( t, s) →
           ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
         , \ ( τ : ( (t , s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t , s))]) →
-            naiveextext
+            naiveextext-extext extext
               ( J × I) ( \ (t , s) → χ t ∧ ψ s) ( \ (t , s) → χ t ∧ ϕ s)
               ( \ _ → A)
               ( \ (t , s) → α (σ' (t , s)))
@@ -384,7 +382,7 @@ extensionality.
                     ( \ s' → τ (t, s')))
                   ( s))))
 
-#def is-right-orthogonal-to-shape-product' uses (naiveextext)
+#def is-right-orthogonal-to-shape-product' uses (extext)
   ( A' A : U)
   ( α : A' → A)
   ( I : CUBE)
@@ -433,7 +431,7 @@ Combining the stability under pushouts and crossing with a shape, we get
 stability under pushout products.
 
 ```rzk
-#def is-right-orthogonal-to-shape-pushout-product uses (naiveextext)
+#def is-right-orthogonal-to-shape-pushout-product uses (extext)
   ( A' A : U)
   ( α : A' → A)
   ( J : CUBE)
@@ -460,7 +458,7 @@ stability under pushout products.
     ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ
       ( is-orth-ψ-ϕ))
 
-#def is-right-orthogonal-to-shape-pushout-product' uses (naiveextext)
+#def is-right-orthogonal-to-shape-pushout-product' uses (extext)
   ( A' A : U)
   ( α : A' → A)
   ( I : CUBE)
@@ -948,18 +946,25 @@ Weak extension extensionality says that every contractible type has unique
 extensions for every shape inclusion `ϕ ⊂ ψ`.
 
 ```rzk
-#def has-unique-extensions-is-contr uses (weakextext)
+#def has-unique-extensions-is-contr uses (extext)
   ( C : U)
   ( is-contr-C : is-contr C)
   : has-unique-extensions I ψ ϕ C
   :=
-    weakextext I ψ ϕ
+    weakextext-extext extext I ψ ϕ
     ( \ _ → C) ( \ _ → is-contr-C)
 
-#def has-unique-extensions-Unit uses (weakextext)
+#def is-local-type-is-contr uses (extext)
+  ( C : U)
+  ( is-contr-C : is-contr C)
+  : is-local-type I ψ ϕ C
+  :=
+    is-local-type-has-unique-extensions I ψ ϕ C
+    ( has-unique-extensions-is-contr C is-contr-C)
+
+#def has-unique-extensions-Unit uses (extext)
   : has-unique-extensions I ψ ϕ Unit
   := has-unique-extensions-is-contr Unit is-contr-Unit
-
 ```
 
 Unique extension types are closed under equivalence.
@@ -991,7 +996,7 @@ Unique extension types are closed under equivalence.
 
 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`).
+`Unit` has unique extensions (using `extext`).
 
 ```rzk
 #section is-right-orthogonal-terminal-map
@@ -1001,7 +1006,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
 #variable A : U
 
 #def has-unique-extensions-is-right-orthogonal-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : has-unique-extensions I ψ ϕ A
   :=
@@ -1011,7 +1016,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-Unit I ψ ϕ)
 
 #def has-unique-extensions-is-right-orthogonal-a-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( tm : A → Unit)
   ( is-orth-ψ-ϕ-tm : is-right-orthogonal-to-shape I ψ ϕ A Unit tm)
   : has-unique-extensions I ψ ϕ A
@@ -1022,7 +1027,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-Unit I ψ ϕ)
 
 #def is-right-orthogonal-terminal-map-has-unique-extensions
-  uses (weakextext)
+  uses (extext)
   ( has-ue-ψ-ϕ-A : has-unique-extensions I ψ ϕ A)
   : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
@@ -1031,7 +1036,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( terminal-map A)
 
 #def is-right-orthogonal-terminal-map-is-local-type
-  uses (weakextext)
+  uses (extext)
   ( is-lt-ψ-ϕ-A : is-local-type I ψ ϕ A)
   : is-right-orthogonal-terminal-map I ψ ϕ A
   :=
@@ -1039,7 +1044,7 @@ Next we prove the logical equivalence between `has-unique-extensions` and
     ( has-unique-extensions-is-local-type I ψ ϕ A is-lt-ψ-ϕ-A)
 
 #def is-local-type-is-right-orthogonal-terminal-map
-  uses (weakextext)
+  uses (extext)
   ( is-orth-ψ-ϕ-tm-A : is-right-orthogonal-terminal-map I ψ ϕ A)
   : is-local-type I ψ ϕ A
   :=
@@ -1059,7 +1064,7 @@ from the unit type.
 
 ```rzk
 #def has-fiberwise-unique-extensions-is-right-orthogonal-to-shape
-  uses (extext weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -1084,7 +1089,7 @@ every fiber of every map `α : A' → A` also has unique extensions.
 
 ```rzk
 #def has-fiberwise-unique-extensions-have-unique-extensions
-  uses (extext weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -1177,7 +1182,7 @@ conditions of being anodyne.
     ( is-right-orthogonal-to-shape-right-cancel-retract A' A α I ψ χ ϕ
       ( f A' A α is-orth₀) ( r))
 
-#def is-anodyne-pushout-product-for-shape uses (naiveextext)
+#def is-anodyne-pushout-product-for-shape uses (extext)
   ( J : CUBE)
   ( χ : J → TOPE)
   ( ζ : χ → TOPE)
@@ -1193,7 +1198,7 @@ conditions of being anodyne.
     ( is-right-orthogonal-to-shape-pushout-product A' A α J χ ζ I ψ ϕ
       ( f A' A α is-orth₀))
 
-#def is-anodyne-pushout-product-for-shape' uses (naiveextext)
+#def is-anodyne-pushout-product-for-shape' uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1230,7 +1235,7 @@ implication with respect to types with unique extensions.
 Every anodyne shape inclusion is weak anodyne.
 
 ```rzk
-#def is-weak-anodyne-is-anodyne-for-shape uses (weakextext)
+#def is-weak-anodyne-is-anodyne-for-shape uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1255,7 +1260,7 @@ analog fo weak anodyne shape inclusions.
   := \ _ has-ue₀ → has-ue₀
 
 #def implication-has-unique-extension-implication-right-orthogonal
-  uses (weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1276,8 +1281,7 @@ analog fo weak anodyne shape inclusions.
       ( is-right-orthogonal-terminal-map-has-unique-extensions I ψ ϕ A
         has-ue-ψ-ϕ))
 
-#def is-weak-anodyne-pushout-product-for-shape
-  uses (naiveextext weakextext)
+#def is-weak-anodyne-pushout-product-for-shape uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1297,8 +1301,7 @@ analog fo weak anodyne shape inclusions.
       is-right-orthogonal-to-shape-pushout-product A'₁ A₁ α₁ J χ ζ I ψ ϕ)
     ( A) (f A has-ue₀)
 
-#def is-weak-anodyne-pushout-product-for-shape'
-  uses (naiveextext weakextext)
+#def is-weak-anodyne-pushout-product-for-shape' uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 844be699..904d40b2 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -1671,6 +1671,43 @@ Interchange law
 #end homotopy-interchange-law
 ```
 
+## Inner anodyne shape inclusions
+
+An **inner fibration** is a map `α : A' → A` which is right orthogonal to
+`Λ ⊂ Δ²`. This is the relative notion of a Segal type.
+
+```rzk
+#def is-inner-fibration
+  ( A' A : U)
+  ( α : A' → A)
+  : U
+  := is-right-orthogonal-to-shape (2 × 2) Δ² (\ t → Λ t) A' A α
+```
+
+We say that a shape inclusion `ϕ ⊂ ψ` is **inner anodyne** if it is anodyne for
+`Λ ⊂ Δ²`, i.e., if every inner fibration `A' → A` is right orthogonal to
+`ϕ ⊂ ψ`.
+
+```rzk
+#def is-inner-anodyne
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  : U
+  := is-anodyne-for-shape (2 × 2) (Δ²) (\ t → Λ t) I ψ ϕ
+
+#def unpack-is-inner-anodyne
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  : is-inner-anodyne I ψ ϕ
+  = ( (A' : U) → (A : U) → (α : A' → A)
+    → is-inner-fibration A' A α
+    → is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  := refl
+
+```
+
 ## Weak inner anodyne shape inclusions
 
 We say that a shape inclusion `ϕ ⊂ ψ` is **weak inner anodyne** if every Segal
@@ -1871,19 +1908,6 @@ It should be easy to adapt it to prove that it is actually inner anodyne.
         ( h^ A h))
 ```
 
-## Inner fibrations
-
-An inner fibration is a map `α : A' → A` which is right orthogonal to `Λ ⊂ Δ²`.
-This is the relative notion of a Segal type.
-
-```rzk
-#def is-inner-fibration
-  ( A' A : U)
-  ( α : A' → A)
-  : U
-  := is-right-orthogonal-to-shape (2 × 2) Δ² (\ t → Λ t) A' A α
-```
-
 ## Products of Segal types
 
 This is an additional section which describes morphisms in products of types as
@@ -1940,7 +1964,7 @@ Segal type. This is an instance of a general statement about types with unique
 extensions for the shape inclusion `Λ ⊂ Δ²`.
 
 ```rzk
-#def is-fiberwise-segal-are-segal uses (extext weakextext)
+#def is-fiberwise-segal-are-segal uses (extext)
   ( A B : U)
   ( f : A → B)
   ( is-segal-A : is-segal A)
@@ -1949,8 +1973,7 @@ extensions for the shape inclusion `Λ ⊂ Δ²`.
   : is-segal (fib A B f b)
   :=
     is-segal-has-unique-inner-extensions (fib A B f b)
-    ( has-fiberwise-unique-extensions-have-unique-extensions
-      extext weakextext
+    ( has-fiberwise-unique-extensions-have-unique-extensions extext
       ( 2 × 2) (Δ²) (\ t → Λ t) A B f
       ( has-unique-inner-extensions-is-segal A is-segal-A)
       ( has-unique-inner-extensions-is-segal B is-segal-B)
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index 7e179143..2dd8b9a4 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -336,9 +336,212 @@ For instance, the arrow type of a discrete type is discrete.
   := is-discrete-extension-type 2 Δ¹ (\ _ → A) (\ _ → is-discrete-A)
 ```
 
-## Discrete types are Segal types
+## Left and right fibrations
 
-Discrete types are automatically Segal types.
+Recall that we can characterize discrete type eithe as those local for
+`{0} ⊂ Δ¹` _or_, equivalently, as those that are local for `{1} ⊂ Δ¹`. This
+suggests two different relative notions of discreteness and corresponding
+notions of anodyne shape inclusions.
+
+```rzk
+#def is-left-fibration
+  ( A' A : U)
+  ( α : A' → A)
+  : U
+  := is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α
+
+#def is-right-fibration
+  ( A' A : U)
+  ( α : A' → A)
+  : U
+  := is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 1₂) A' A α
+```
+
+### Left and right anodyne shape inclusions
+
+```rzk
+#def is-left-anodyne
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  : U
+  := is-anodyne-for-shape 2 Δ¹ ( \ s → s ≡ 0₂) I ψ ϕ
+
+#def is-right-anodyne
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  : U
+  := is-anodyne-for-shape 2 Δ¹ ( \ s → s ≡ 1₂) I ψ ϕ
+```
+
+### Left fibrations are inner fibrations
+
+We aim to show that every left fibration is an inner fibration. This is a
+sequence of manipulations where we start with the assumption that `{0} ⊂ Δ¹` is
+left orthogonal to `α : A' → A`, i.e.
+
+```rzk
+#section is-inner-fibration-is-left-fibration
+
+#variables A' A : U
+#variable α : A' → A
+
+#variable is-left-fib-α : is-left-fibration A' A α
+```
+
+and deduce that various other shape inclusions are left orthogonal as well.
+
+The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes
+`{1} ⊂ right-leg-of-Λ` of `Λ`.
+
+```rzk
+#def right-leg-of-Λ : Λ → TOPE
+  := \ (t, s) → t ≡ 1₂
+
+#def is-equiv-Δ¹-to-right-leg-of-Λ-rel-start
+  ( B : U)
+  ( b : B)
+  : is-equiv
+    ( ( s : Δ¹) → B [ s ≡ 0₂ ↦ b])
+    ( ( (t,s) : right-leg-of-Λ) → B [ s ≡ 0₂ ↦ b])
+    ( \ τ (t,s) → τ s)
+  :=
+    ( ( \ υ s → υ (1₂, s) , \ _ → refl)
+    , ( \ υ s → υ (1₂, s) , \ _ → refl))
+
+#def is-right-orthogonal-to-10-1×Δ¹-is-left-fibration uses (is-left-fib-α)
+  : is-right-orthogonal-to-shape
+      ( 2 × 2) (\ ts → right-leg-of-Λ ts) ( \ (_,s) → s ≡ 0₂) A' A α
+  :=
+    \ ( σ' : ( (t,s) : 2 × 2 | right-leg-of-Λ (t,s) ∧ s ≡ 0₂) → A') →
+      is-equiv-Equiv-is-equiv'
+      ( ( s : Δ¹) → A' [s ≡ 0₂ ↦ σ' (1₂, s)])
+      ( ( s : Δ¹) → A [s ≡ 0₂ ↦ α (σ' (1₂, s))])
+      ( \ τ s → α (τ s))
+      ( ( (_, s) : right-leg-of-Λ) → A' [ s ≡ 0₂ ↦ σ' (1₂,s)])
+      ( ( (_, s) : right-leg-of-Λ) → A [ s ≡ 0₂ ↦ α ( σ' (1₂,s))])
+      ( \ υ ts → α (υ ts))
+      ( ( ( \ τ' (t,s) → τ' s , \ τ (t,s) → τ s) , \ _ → refl),
+        ( is-equiv-Δ¹-to-right-leg-of-Λ-rel-start A' ( σ' (1₂, 0₂))
+        , is-equiv-Δ¹-to-right-leg-of-Λ-rel-start A ( α ( σ' (1₂, 0₂)))))
+      ( is-left-fib-α ( \ ( s : 2 | Δ¹ s ∧ s ≡ 0₂) → σ' (1₂,s)))
+```
+
+Next we use that `Λ` is the pushout of its left leg and its right leg to deduce
+that the pair `left-leg-of-Λ ⊂ Λ` is left orthogonal.
+
+```rzk
+#def left-leg-of-Λ : Λ → TOPE
+  := \ (t, s) → s ≡ 0₂
+
+#def is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration uses (is-left-fib-α)
+  : is-right-orthogonal-to-shape
+      ( 2 × 2) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts) A' A α
+  :=
+    is-right-orthogonal-to-shape-pushout A' A α
+    ( 2 × 2) ( \ ts → right-leg-of-Λ ts) (\ ts → left-leg-of-Λ ts)
+    ( is-right-orthogonal-to-10-1×Δ¹-is-left-fibration)
+```
+
+Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the product of
+`Δ¹` with the left orthogonal pair `{0} ⊂ Δ¹`, hence left orthogonal itself.
+
+```rzk
+#def is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration
+       uses (extext is-left-fib-α)
+  : is-right-orthogonal-to-shape
+      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts) A' A α
+  :=
+    is-right-orthogonal-to-shape-product extext A' A α
+      2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) is-left-fib-α
+```
+
+Next, we use the left cancellation of left orthogonal shape inclusions to deduce
+that `Λ ⊂ Δ¹×Δ¹` is left orthogonal to `α : A' → A`.
+
+```rzk
+#def is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration
+       uses (extext is-left-fib-α)
+  : is-right-orthogonal-to-shape
+      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) A' A α
+  :=
+    is-right-orthogonal-to-shape-left-cancel A' A α
+    ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts)
+    ( is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration)
+    ( is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration)
+```
+
+Finally, we right cancel the functorial retract `Δ² ⊂ Δ¹×Δ¹` to obtain the
+desired left orthogonal shape inclusion `Λ ⊂ Δ²`.
+
+```rzk
+#def is-inner-fibration-is-left-fibration uses (extext is-left-fib-α)
+  : is-inner-fibration A' A α
+  :=
+    is-right-orthogonal-to-shape-right-cancel-retract A' A α
+    ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Δ² ts) ( \ ts → Λ ts)
+    ( is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration)
+    ( Δ²-is-functorial-retract-Δ¹×Δ¹)
+
+#end is-inner-fibration-is-left-fibration
+```
+
+In other words, we have shown that the inner horn inclusion `Λ ⊂ Δ²` is left
+anodyne.
+
+```rzk
+#def is-left-anodyne-Λ-Δ² uses (extext)
+  : is-left-anodyne (2 × 2) Δ² (\ t → Λ t)
+  := is-inner-fibration-is-left-fibration
+```
+
+### Left fibrations and Segal types
+
+Since the Segal types are precisely the local types with respect to `Λ ⊂ Δ²`, we
+immediately deduce that in any left fibration `α : A' → A`, if `A` is a Segal
+type, then so is `A'`.
+
+```rzk title="RS 17, Theorem 8.8, categorical version"
+#def is-segal-domain-left-fibration-is-segal-codomain uses (extext)
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-left-fib-α : is-left-fibration A' A α)
+  ( is-segal-A : is-segal A)
+  : is-segal A'
+  :=
+    is-segal-is-local-horn-inclusion A'
+      ( is-local-type-right-orthogonal-is-local-type
+        ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α
+        ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α)
+        ( is-local-horn-inclusion-is-segal A is-segal-A))
+```
+
+### Discrete types are Segal types
+
+Another immediate corollary is that every discrete type is Segal.
+
+```rzk
+#def is-segal-is-discrete uses (extext)
+  ( A : U)
+  : is-discrete A → is-segal A
+  :=
+  \ is-discrete-A →
+  ( is-segal-has-unique-inner-extensions A
+    ( is-weak-anodyne-is-anodyne-for-shape extext
+      ( 2) (Δ¹) (\ t → t ≡ 0₂) ( 2 × 2) (Δ²) (\ t → Λ t)
+      ( is-left-anodyne-Λ-Δ²)
+      ( A)
+      ( has-unique-extensions-is-local-type 2 Δ¹ (\ t → t ≡ 0₂) A
+        ( is-left-local-is-Δ¹-local A
+          ( is-Δ¹-local-is-discrete A is-discrete-A)))))
+```
+
+## Discrete types are Segal types (original proof of RS17)
+
+This chapter contains the original proof of RS17 that discrete types are
+automatically Segal types. We retain it since some intermediate calculations
+might still be of use.
 
 ```rzk
 #section discrete-arr-equivalences
@@ -941,7 +1144,7 @@ general case to the one just proven:
 Finally, we conclude:
 
 ```rzk title="RS17, Proposition 7.3"
-#def is-segal-is-discrete uses (extext)
+#def is-segal-is-discrete' uses (extext)
   ( A : U)
   ( is-discrete-A : is-discrete A)
   : is-segal A
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 0afb7daf..bc10f0e2 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -25,8 +25,6 @@ Some of the definitions in this file rely on extension extensionality:
 ```rzk
 #assume extext : ExtExt
 #assume weakfunext : WeakFunExt
-#assume naiveextext : NaiveExtExt
-
 ```
 
 ## Dependent hom types
@@ -225,26 +223,20 @@ As a sanity check we unpack the definition of `is-naive-left-fibration`.
 
 ### Naive left fibrations are left fibrations
 
-A map `α : A' → A` is called a left fibration if it is right orthogonal to the
-shape inclusion `{0} ⊂ Δ¹`.
+Recall that a map `α : A' → A` is called a left fibration if it is right
+orthogonal to the shape inclusion `{0} ⊂ Δ¹`.
+
+This notion agrees with that of a naive left fibration.
 
 ```rzk
-#section is-left-fibration
+#section is-left-fibration-is-naive-left-fibration
 
 #variables A' A : U
 #variable α : A' → A
 
-#def is-left-fibration
-  : U
-  := is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α
-```
-
-This notion agrees with that of a naive left fibration.
-
-```rzk
 #def is-left-fibration-is-naive-left-fibration
   ( is-nlf : is-naive-left-fibration A A' α)
-  : is-left-fibration
+  : is-left-fibration A' A α
   :=
     \ a' →
       is-equiv-equiv-is-equiv
@@ -259,7 +251,7 @@ This notion agrees with that of a naive left fibration.
         ( is-nlf (a' 0₂))
 
 #def is-naive-left-fibration-is-left-fibration
-  ( is-lf : is-left-fibration)
+  ( is-lf : is-left-fibration A' A α)
   : is-naive-left-fibration A A' α
   :=
     \ a' →
@@ -277,149 +269,12 @@ This notion agrees with that of a naive left fibration.
 #def is-naive-left-fibration-iff-is-left-fibration
   : iff
       ( is-naive-left-fibration A A' α)
-      ( is-left-fibration)
+      ( is-left-fibration A' A α)
   :=
     ( is-left-fibration-is-naive-left-fibration,
       is-naive-left-fibration-is-left-fibration)
 
-#end is-left-fibration
-```
-
-### Left fibrations are inner fibrations
-
-Recall that an inner fibration is a map `α : A' → A` which is right orthogonal
-to `Λ ⊂ Δ²`.
-
-We aim to show that every left fibration is an inner fibration. This is a
-sequence of manipulations where we start with the assumption that `{0} ⊂ Δ¹` is
-left orthogonal to `α : A' → A`, i.e.
-
-```rzk
-#section is-inner-fibration-is-left-fibration
-
-#variables A' A : U
-#variable α : A' → A
-
-#variable is-left-fib-α : is-left-fibration A' A α
-```
-
-and deduce that various other shape inclusions are left orthogonal as well.
-
-The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes
-`{1} ⊂ right-leg-of-Λ` of `Λ`.
-
-```rzk
-#def right-leg-of-Λ : Λ → TOPE
-  := \ (t, s) → t ≡ 1₂
-
-#def is-equiv-Δ¹-to-right-leg-of-Λ-rel-start
-  ( B : U)
-  ( b : B)
-  : is-equiv
-      ( ( s : Δ¹) → B [ s ≡ 0₂ ↦ b])
-      ( ( (t,s) : right-leg-of-Λ) → B [ s ≡ 0₂ ↦ b])
-      ( \ τ (t,s) → τ s)
-  :=
-    ( ( \ υ s → υ (1₂, s) , \ _ → refl),
-      ( \ υ s → υ (1₂, s) , \ _ → refl))
-
-#def is-right-orthogonal-to-10-1×Δ¹-is-left-fibration uses (is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) (\ ts → right-leg-of-Λ ts) ( \ (_,s) → s ≡ 0₂) A' A α
-  :=
-    \ ( σ' : ( (t,s) : 2 × 2 | right-leg-of-Λ (t,s) ∧ s ≡ 0₂) → A') →
-      is-equiv-Equiv-is-equiv'
-        ( ( s : Δ¹) → A' [s ≡ 0₂ ↦ σ' (1₂, s)])
-        ( ( s : Δ¹) → A [s ≡ 0₂ ↦ α (σ' (1₂, s))])
-        ( \ τ s → α (τ s))
-        ( ( (_, s) : right-leg-of-Λ) → A' [ s ≡ 0₂ ↦ σ' (1₂,s)])
-        ( ( (_, s) : right-leg-of-Λ) → A [ s ≡ 0₂ ↦ α ( σ' (1₂,s))])
-        ( \ υ ts → α (υ ts))
-        ( ( ( \ τ' (t,s) → τ' s , \ τ (t,s) → τ s) , \ _ → refl),
-          ( is-equiv-Δ¹-to-right-leg-of-Λ-rel-start A' ( σ' (1₂, 0₂))
-          , is-equiv-Δ¹-to-right-leg-of-Λ-rel-start A ( α ( σ' (1₂, 0₂)))
-          )
-        )
-        ( is-left-fib-α ( \ ( s : 2 | Δ¹ s ∧ s ≡ 0₂) → σ' (1₂,s)))
-```
-
-Next we use that `Λ` is the pushout of its left leg and its right leg to deduce
-that the pair `left-leg-of-Λ ⊂ Λ` is left orthogonal.
-
-```rzk
-#def left-leg-of-Λ : Λ → TOPE
-  := \ (t, s) → s ≡ 0₂
-
-#def is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration uses (is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts) A' A α
-  :=
-    is-right-orthogonal-to-shape-pushout A' A α
-      ( 2 × 2) ( \ ts → right-leg-of-Λ ts) (\ ts → left-leg-of-Λ ts)
-      ( is-right-orthogonal-to-10-1×Δ¹-is-left-fibration)
-
-```
-
-Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the product of
-`Δ¹` with the left orthogonal pair `{0} ⊂ Δ¹`, hence left orthogonal itself.
-
-```rzk
-#def is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration
-       uses (naiveextext is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts) A' A α
-  :=
-    is-right-orthogonal-to-shape-product naiveextext A' A α
-      2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) is-left-fib-α
-```
-
-Next, we use the left cancellation of left orthogonal shape inclusions to deduce
-that `Λ ⊂ Δ¹×Δ¹` is left orthogonal to `α : A' → A`.
-
-```rzk
-#def is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration
-       uses (naiveextext is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) A' A α
-  :=
-    is-right-orthogonal-to-shape-left-cancel A' A α
-      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts)
-      ( is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration)
-      ( is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration)
-```
-
-Finally, we right cancel the functorial retract `Δ² ⊂ Δ¹×Δ¹` to obtain the
-desired left orthogonal shape inclusion `Λ ⊂ Δ²`.
-
-```rzk
-#def is-inner-fibration-is-left-fibration uses (naiveextext is-left-fib-α)
-  : is-inner-fibration A' A α
-  :=
-    is-right-orthogonal-to-shape-right-cancel-retract A' A α
-      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Δ² ts) ( \ ts → Λ ts)
-      ( is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration)
-      ( Δ²-is-functorial-retract-Δ¹×Δ¹)
-
-#end is-inner-fibration-is-left-fibration
-```
-
-Since the Segal types are precisely the local types with respect to `Λ ⊂ Δ¹`, we
-immediately deduce that in any left fibration `α : A' → A`, if `A` is a Segal
-type, then so is `A'`.
-
-```rzk title="Theorem 8.8, categorical version"
-#def is-segal-domain-left-fibration-is-segal-codomain uses (naiveextext)
-  ( A' A : U)
-  ( α : A' → A)
-  ( is-left-fib-α : is-left-fibration A' A α)
-  ( is-segal-A : is-segal A)
-  : is-segal A'
-  :=
-    is-segal-is-local-horn-inclusion A'
-      ( is-local-type-right-orthogonal-is-local-type
-        ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α
-        ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α)
-        ( is-local-horn-inclusion-is-segal A is-segal-A))
+#end is-left-fibration-is-naive-left-fibration
 ```
 
 ### Naive left fibrations vs. covariant families
@@ -599,13 +454,13 @@ fibration, hence an inner fibration. It immediately follows that if `A` is
 Segal, then so is `Σ A, C`.
 
 ```rzk title="RS17, Theorem 8.8"
-#def is-segal-total-type-covariant-family-is-segal-base uses (naiveextext)
+#def is-segal-total-type-covariant-family-is-segal-base uses (extext)
   ( A : U)
   ( C : A → U)
   ( is-covariant-C : is-covariant A C)
   : is-segal A → is-segal (total-type A C)
   :=
-    is-segal-domain-left-fibration-is-segal-codomain
+    is-segal-domain-left-fibration-is-segal-codomain extext
       ( total-type A C) A (\ (a,_) → a)
         ( is-left-fibration-is-naive-left-fibration
             ( total-type A C) A (\ (a,_) → a)
diff --git a/src/simplicial-hott/13-limits.rzk.md b/src/simplicial-hott/13-limits.rzk.md
index 0af7298a..c38eb081 100644
--- a/src/simplicial-hott/13-limits.rzk.md
+++ b/src/simplicial-hott/13-limits.rzk.md
@@ -8,11 +8,12 @@ This is a literate `rzk` file:
 #lang rzk-1
 ```
 
-Some definitions make use of function extentionality.
+Some definitions make use of function extentionality and extension
+extensionality.
 
 ```rzk
 #assume funext : FunExt
-#assume naiveextext : NaiveExtExt
+#assume extext : ExtExt
 ```
 
 ## Definition limits and colimits
@@ -262,14 +263,14 @@ The type of cocones of a function with codomain a Segal type is a Segal type.
         ( f))
     ( \ b → constant A B b)
 
-#def is-segal-cocone-is-segal uses (funext)
+#def is-segal-cocone-is-segal uses (funext extext)
   ( A B : U)
   ( is-segal-B : is-segal B)
   ( f : A → B)
   : is-segal ( cocone A B f)
   :=
     is-segal-total-type-covariant-family-is-segal-base
-    ( naiveextext)
+    ( extext)
     ( B)
     ( family-cocone A B f)
     ( is-covariant-family-cone-is-segal
@@ -283,7 +284,7 @@ The type of cocones of a function with codomain a Segal type is a Segal type.
 Colimits are unique up to isomorphism.
 
 ```rzk title="BM, Corollary 1 (i)"
-#def iso-colimit-is-segal uses ( naiveextext funext)
+#def iso-colimit-is-segal uses ( extext funext)
   ( A B : U)
   ( is-segal-B : is-segal B)
   ( f : A → B)

From ada39fcb732e8cbf096c98e2682eb2ef924fccb2 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 16:59:45 +0100
Subject: [PATCH 04/11] minor edits and formatting

---
 src/simplicial-hott/07-discrete.rzk.md | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index 2dd8b9a4..5af68bc6 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -338,11 +338,15 @@ For instance, the arrow type of a discrete type is discrete.
 
 ## Left and right fibrations
 
-Recall that we can characterize discrete type eithe as those local for
+Recall that we can characterize discrete type either as those local for
 `{0} ⊂ Δ¹` _or_, equivalently, as those that are local for `{1} ⊂ Δ¹`. This
 suggests two different relative notions of discreteness and corresponding
 notions of anodyne shape inclusions.
 
+Note that while the absolute notions of locality for `{0} ⊂ Δ¹` and `{1} ⊂ Δ¹`
+agree, the relative notions _do not_. We will explore this discrepancy more when
+we introduce covariant and contravariant type families.
+
 ```rzk
 #def is-left-fibration
   ( A' A : U)

From 65127c2fe04a9238178b1a5ae60d268c496eb276 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 17:06:10 +0100
Subject: [PATCH 05/11] fix typechecking error introduced by merging main

---
 src/simplicial-hott/04-right-orthogonal.rzk.md | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 6ca6962b..c4460528 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -1236,7 +1236,7 @@ implication with respect to types with unique extensions.
 Every anodyne shape inclusion is weak anodyne.
 
 ```rzk
-#def is-weak-anodyne-is-anodyne-for-shape uses (weakextext)
+#def is-weak-anodyne-is-anodyne-for-shape uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1261,7 +1261,7 @@ analog fo weak anodyne shape inclusions.
   := \ _ has-ue₀ → has-ue₀
 
 #def implication-has-unique-extension-implication-right-orthogonal
-  uses (weakextext)
+  uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1283,7 +1283,7 @@ analog fo weak anodyne shape inclusions.
         has-ue-ψ-ϕ))
 
 #def is-weak-anodyne-pushout-product-for-shape
-  uses (naiveextext weakextext)
+  uses (naiveextext extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1304,7 +1304,7 @@ analog fo weak anodyne shape inclusions.
     ( A) (f A has-ue₀)
 
 #def is-weak-anodyne-pushout-product-for-shape'
-  uses (naiveextext weakextext)
+  uses (naiveextext extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )

From 8e46d6c3836769336fd635323ae280e1c10be64a Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 18:45:49 +0100
Subject: [PATCH 06/11] reformulate is-inner-fibration-is-left-fibration with
 anodyne

---
 .../02-simplicial-type-theory.rzk.md          |  2 +-
 src/simplicial-hott/07-discrete.rzk.md        | 91 ++++++++-----------
 2 files changed, 41 insertions(+), 52 deletions(-)

diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
index 24c1d77a..58eebd2b 100644
--- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md
+++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
@@ -298,7 +298,7 @@ for a section of the family of extensions of a function `ϕ → A` to a function
 For example, this applies to `Δ² ⊂ Δ¹×Δ¹`.
 
 ```rzk
-#def Δ²-is-functorial-retract-Δ¹×Δ¹
+#def is-functorial-retract-Δ²-Δ¹×Δ¹
   : is-functorial-shape-retract (2 × 2) (Δ¹×Δ¹) (Δ²)
   :=
     \ A' A α →
diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index 5af68bc6..79064b78 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -381,20 +381,8 @@ we introduce covariant and contravariant type families.
 
 ### Left fibrations are inner fibrations
 
-We aim to show that every left fibration is an inner fibration. This is a
-sequence of manipulations where we start with the assumption that `{0} ⊂ Δ¹` is
-left orthogonal to `α : A' → A`, i.e.
-
-```rzk
-#section is-inner-fibration-is-left-fibration
-
-#variables A' A : U
-#variable α : A' → A
-
-#variable is-left-fib-α : is-left-fibration A' A α
-```
-
-and deduce that various other shape inclusions are left orthogonal as well.
+We aim to show that every left fibration is an inner fibration, i.e. that the
+inner horn inclusion `Λ ⊂ Δ²` is left anodyne.
 
 The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes
 `{1} ⊂ right-leg-of-Λ` of `Λ`.
@@ -414,10 +402,11 @@ The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes
     ( ( \ υ s → υ (1₂, s) , \ _ → refl)
     , ( \ υ s → υ (1₂, s) , \ _ → refl))
 
-#def is-right-orthogonal-to-10-1×Δ¹-is-left-fibration uses (is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) (\ ts → right-leg-of-Λ ts) ( \ (_,s) → s ≡ 0₂) A' A α
+#def is-left-anodyne-1-right-leg-of-Λ
+  : is-left-anodyne
+    ( 2 × 2) (\ ts → right-leg-of-Λ ts) ( \ (_,s) → s ≡ 0₂)
   :=
+  \ A' A α is-left-fib-α →
     \ ( σ' : ( (t,s) : 2 × 2 | right-leg-of-Λ (t,s) ∧ s ≡ 0₂) → A') →
       is-equiv-Equiv-is-equiv'
       ( ( s : Δ¹) → A' [s ≡ 0₂ ↦ σ' (1₂, s)])
@@ -433,71 +422,71 @@ The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes
 ```
 
 Next we use that `Λ` is the pushout of its left leg and its right leg to deduce
-that the pair `left-leg-of-Λ ⊂ Λ` is left orthogonal.
+that the pair `left-leg-of-Λ ⊂ Λ` is left anodyne.
 
 ```rzk
 #def left-leg-of-Λ : Λ → TOPE
   := \ (t, s) → s ≡ 0₂
 
-#def is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration uses (is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts) A' A α
+#def is-left-anodyne-left-leg-of-Λ-Λ
+  : is-left-anodyne
+      ( 2 × 2) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts)
   :=
+  \ A' A α is-left-fib-α →
     is-right-orthogonal-to-shape-pushout A' A α
     ( 2 × 2) ( \ ts → right-leg-of-Λ ts) (\ ts → left-leg-of-Λ ts)
-    ( is-right-orthogonal-to-10-1×Δ¹-is-left-fibration)
+    ( is-left-anodyne-1-right-leg-of-Λ A' A α is-left-fib-α)
 ```
 
 Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the product of
-`Δ¹` with the left orthogonal pair `{0} ⊂ Δ¹`, hence left orthogonal itself.
+`Δ¹` with the left anodyne pair `{0} ⊂ Δ¹`, hence left anodyne itself.
 
 ```rzk
-#def is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration
-       uses (extext is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts) A' A α
+#def is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹
+  : is-left-anodyne ( 2 × 2)
+    ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts)
   :=
+  \ A' A α is-left-fib-α →
     is-right-orthogonal-to-shape-product extext A' A α
       2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) is-left-fib-α
 ```
 
-Next, we use the left cancellation of left orthogonal shape inclusions to deduce
-that `Λ ⊂ Δ¹×Δ¹` is left orthogonal to `α : A' → A`.
+Next, we use the left cancellation of left anodyne shape inclusions to deduce
+that `Λ ⊂ Δ¹×Δ¹` is left anodyne.
 
 ```rzk
-#def is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration
-       uses (extext is-left-fib-α)
-  : is-right-orthogonal-to-shape
-      ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) A' A α
+#def is-left-anodyne-Λ-Δ¹×Δ¹ uses (extext)
+  : is-left-anodyne ( 2 × 2)
+    ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts)
   :=
-    is-right-orthogonal-to-shape-left-cancel A' A α
-    ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts)
-    ( is-right-orthogonal-to-left-leg-of-Λ-Λ-is-left-fibration)
-    ( is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-left-fibration)
+  is-anodyne-left-cancel-for-shape 2 Δ¹ (\ t → t ≡ 0₂)
+  ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts) ( \ ts → left-leg-of-Λ ts)
+  ( is-left-anodyne-left-leg-of-Λ-Λ)
+  ( is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹)
 ```
 
 Finally, we right cancel the functorial retract `Δ² ⊂ Δ¹×Δ¹` to obtain the
-desired left orthogonal shape inclusion `Λ ⊂ Δ²`.
+desired left anodyne shape inclusion `Λ ⊂ Δ²`.
 
 ```rzk
-#def is-inner-fibration-is-left-fibration uses (extext is-left-fib-α)
-  : is-inner-fibration A' A α
+#def is-left-anodyne-Λ-Δ² uses (extext)
+  : is-left-anodyne (2 × 2)
+    Δ² (\ t → Λ t)
   :=
-    is-right-orthogonal-to-shape-right-cancel-retract A' A α
-    ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Δ² ts) ( \ ts → Λ ts)
-    ( is-right-orthogonal-to-Λ-Δ¹×Δ¹-is-left-fibration)
-    ( Δ²-is-functorial-retract-Δ¹×Δ¹)
-
-#end is-inner-fibration-is-left-fibration
+  is-anodyne-right-cancel-retract-for-shape 2 Δ¹ (\ t → t ≡ 0₂)
+  ( 2 × 2) ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Δ² ts) ( \ ts → Λ ts)
+  ( is-functorial-retract-Δ²-Δ¹×Δ¹)
+  ( is-left-anodyne-Λ-Δ¹×Δ¹)
 ```
 
-In other words, we have shown that the inner horn inclusion `Λ ⊂ Δ²` is left
-anodyne.
+which we can unpack to get the desired implication
 
 ```rzk
-#def is-left-anodyne-Λ-Δ² uses (extext)
-  : is-left-anodyne (2 × 2) Δ² (\ t → Λ t)
-  := is-inner-fibration-is-left-fibration
+#def is-inner-fibration-is-left-fibration uses (extext)
+  ( A' A : U)
+  ( α : A' → A)
+  : is-left-fibration A' A α → is-inner-fibration A' A α
+  := is-left-anodyne-Λ-Δ² A' A α
 ```
 
 ### Left fibrations and Segal types

From f4e6d4a5228f1c3552b2b2acecebf00e24cd28c7 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 22:52:58 +0100
Subject: [PATCH 07/11] functorian isomorphisms

---
 src/hott/11-homotopy-pullbacks.rzk.md         | 116 ++++++++++++++++++
 .../02-simplicial-type-theory.rzk.md          |  91 ++++++++++++++
 .../04-right-orthogonal.rzk.md                |  76 +++++++++++-
 src/simplicial-hott/08-covariant.rzk.md       |   2 -
 4 files changed, 277 insertions(+), 8 deletions(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index a2d6c5c6..3c67c9c9 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -240,6 +240,7 @@ maps `β → α` and obtain another homotopy cartesian square.
         ( is-equiv-transport A C (α (s' b')) (s (β b')) (η b'))
 ```
 
+
 ## Pasting calculus for homotopy cartesian squares
 
 Currently our notion of squares is not symmetric, since the vertical maps are
@@ -247,6 +248,8 @@ given by type families, i.e. they are _display maps_, while the horizontal maps
 are arbitrary. Therefore we distinquish between the vertical and the horizontal
 pasting calculus.
 
+
+
 ### Vertical calculus
 
 The following vertical composition and cancellation laws follow easily from the
@@ -472,6 +475,119 @@ In fact, it suffices to assume that the left square has horizontal sections.
 #end homotopy-cartesian-horizontal-calculus
 ```
 
+### Homotopy cartesian faces of a cube
+
+Consider two squares induced by type families as follows
+
+```rzk
+#section is-homotopy-cartesian-in-cube
+
+#variable A' : U
+#variable C' : A' → U
+#variable A : U
+#variable C : A → U
+#variable α : A' → A
+#variable γ : (a' : A') → C' a' → C (α a')
+
+#variable B' : U
+#variable D' : B' → U
+#variable B : U
+#variable D : B → U
+#variable β : B' → B
+#variable δ : (b' : B') → D' b' → D (β b')
+```
+
+and a map between them in the following strict sense
+
+```rzk
+#variable f' : A' → B'
+#variable f : A → B
+#variable h : (a' : A') → β (f' a') = f (α a')
+
+#variable F' : (a' : A') → C' a' → D' (f' a')
+#variable F : (a : A) → C a → D (f a)
+#variable H
+  : (a' : A')
+  → (c' : C' a')
+  → ( transport B D (β (f' a')) (f (α a')) (h a')
+      ( δ (f' a') (F' a' c'))
+    = F (α a') (γ a' c'))
+```
+
+We view this as a cube
+
+```
+      Σ D'      Σ D
+
+Σ C'      Σ C
+
+       B'        B
+
+ A'        A
+```
+
+with display maps going down and ordinary maps going to the right and up-right.
+
+Assume furthermore that the two squares on the left and right are themselves
+homotopy cartesian.
+
+```rzk
+#variable is-hc-CD' : is-homotopy-cartesian A' C' B' D' f' F'
+#variable is-hc-CD : is-homotopy-cartesian A C B D f F
+```
+
+If the square `B' D' B D` is homotopy cartesian, then so is `A' C' A C`.
+
+```rzk
+#def is-homotopy-cartesian-in-cube
+  : is-homotopy-cartesian B' D' B D β δ
+  → is-homotopy-cartesian A' C' A C α γ
+  :=
+  \ is-hc-BD a' →
+    is-equiv-equiv-is-equiv
+    ( C' a') (C (α a')) (γ a')
+    ( D' (f' a')) (D (f (α a')))
+    (\ d' → transport B D (β (f' a')) (f (α a')) (h a') (δ (f' a') d'))
+    ( ( F' a' ,  F (α a')) , H a')
+    ( is-hc-CD' a')
+    ( is-hc-CD (α a'))
+    ( is-equiv-comp
+      ( D' (f' a')) (D (β (f' a'))) (D (f (α a')))
+      ( δ (f' a')) (is-hc-BD (f' a'))
+      ( transport B D (β (f' a')) (f (α a')) (h a'))
+      ( is-equiv-transport B D (β (f' a')) (f (α a')) (h a')))
+```
+
+The converse holds provided that the map `f' : A' → B'` has a section.
+
+```rzk
+#def is-homotopy-cartesian-in-cube'
+  ( has-sec-f' : has-section A' B' f')
+  : is-homotopy-cartesian A' C' A C α γ
+  → is-homotopy-cartesian B' D' B D β δ
+  :=
+  \ is-hc-AC →
+    ind-has-section A' B' f' has-sec-f'
+    ( \ b' → is-equiv (D' b') (D (β b')) (δ b'))
+    ( \ a' →
+      ( is-equiv-right-factor
+        ( D' (f' a')) (D (β (f' a'))) (D (f (α a')))
+        ( δ (f' a'))
+        ( transport B D (β (f' a')) (f (α a')) (h a'))
+        ( is-equiv-transport B D (β (f' a')) (f (α a')) (h a'))
+        ( is-equiv-equiv-is-equiv'
+          ( C' a') (C (α a')) (γ a')
+          ( D' (f' a')) (D (f (α a')))
+          (\ d' → transport B D (β (f' a')) (f (α a')) (h a') (δ (f' a') d'))
+          ( ( F' a' ,  F (α a')) , H a')
+          ( is-hc-CD' a')
+          ( is-hc-CD (α a'))
+          ( is-hc-AC a'))))
+
+#end is-homotopy-cartesian-in-cube
+```
+
+
 ## Fiber products
 
 Given two type families `B C : A → U`, we can form their **fiberwise product**.
diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
index 24c1d77a..5feded51 100644
--- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md
+++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
@@ -334,3 +334,94 @@ to diagrams extending a fixed diagram `σ': ϕ → A'` (or, respectively, its im
     , \ τ' → second (is-fretract-ψ-χ A' A α) τ'
     )
 ```
+
+### Isomorphisms of shape inclusions
+
+Consider two shape inclusions `ϕ ⊂ ψ` and `ζ ⊂ χ`. We want to express the fact
+that there is an isomorphism `ψ ≅ χ` of shapes which restricts to an isomorphism
+`ϕ ≅ ζ`. Since shapes are not types themselves, the best we can currently do is
+describe this isomorphism on representables.
+
+```rzk
+#def isomorphism-shape-inclusions
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  : U
+  :=
+    ( Σ ( f
+          : (A : U)
+          → Equiv (ζ → A) (ϕ → A))
+      , ( ( A : U)
+        → ( σ : ζ → A)
+        → ( Equiv
+            ( (t : χ) → A [ζ t ↦ σ t])
+            ( (t : ψ) → A [ϕ t ↦ first (f A) σ t]))))
+
+#def functorial-isomorphism-shape-inclusions
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  : U
+  :=
+  Σ ( (f , F) : isomorphism-shape-inclusions I ψ ϕ J χ ζ)
+  , ( Σ ( e
+          : ( A' : U)
+          → ( A : U)
+          → ( α : A' → A)
+          → ( σ' : ζ → A')
+          → ( ( \ (t : I | ϕ t) → α (first (f A') σ' t))
+            = ( first (f A) (\ t → α (σ' t)))))
+      , ( ( A' : U)
+        → ( A : U)
+        → ( α : A' → A)
+        → ( σ' : ζ → A')
+        → ( τ' : (t : χ) → A' [ζ t ↦ σ' t])
+        → ( ( transport (ϕ → A) (\ σ → (t : ψ) → A [ϕ t ↦ σ t])
+              ( \ (t : I | ϕ t) → α (first (f A') σ' t))
+              ( first (f A) (\ t → α (σ' t)))
+              ( e A' A α σ')
+              (\ (t : ψ) → α (first (F A' σ') τ' t)))
+            = ( first (F A (\ (t : ζ) → α (σ' t))) (\ (t : χ) → α (τ' t))))))
+```
+
+As an example, we show establish the canonical isomorphism between the pairs
+`{0} ⊂ Δ¹` and `{1} ⊂ right-leg-of-Λ`. It really just boils down to the two
+formulas `\ τ (t , s) → τ s` describing the map
+`(Δ¹ → A) → (right-leg-of-Λ → A)` and `\ υ s → υ (1₂ , s)` describing its
+inverse. All of the necessary coherences are just `refl`. Unfortunately, there
+is currently no better way to define this functorial isomorphism other than
+spelling out the following monstrosity:
+
+```rzk
+#def right-leg-of-Λ : Λ → TOPE
+  := \ (t, s) → t ≡ 1₂
+
+#def isomorphism-0-Δ¹-1-right-leg-of-Λ
+  : isomorphism-shape-inclusions
+    (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
+    2 Δ¹ (\ t → t ≡ 0₂)
+  :=
+    ( \ A →
+      ( \ τ (t,s) → τ s
+      , ( ( \ υ s → υ (1₂, s) , \ _ → refl)
+        , ( \ υ s → υ (1₂, s) , \ _ → refl)))
+    , \ A _ →
+      ( \ τ (t,s) → τ s
+      , ( ( \ υ s → υ (1₂, s) , \ _ → refl)
+        , ( \ υ s → υ (1₂, s) , \ _ → refl))))
+
+#def functorial-isomorphism-0-Δ¹-1-right-leg-of-Λ
+  : functorial-isomorphism-shape-inclusions
+    (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
+    2 Δ¹ (\ t → t ≡ 0₂)
+  :=
+    ( isomorphism-0-Δ¹-1-right-leg-of-Λ
+    , ( \ _ _ _ _ → refl , \ _ _ _ _ _ → refl))
+```
diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index a572e002..e848442c 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -193,7 +193,7 @@ occasionally go back or forth along the functorial equivalence
       ( is-orth-ψ-ϕ σ'))
 ```
 
-### Stability under composition
+### Composition
 
 Left orthogonal shape inclusions are preserved under composition.
 
@@ -229,7 +229,7 @@ Left orthogonal shape inclusions are preserved under composition.
           σ')
 ```
 
-### Cancellation laws
+### Cancellation
 
 If `ϕ ⊂ χ` and `ϕ ⊂ ψ` are left orthogonal to `α : A' → A`, then so is `χ ⊂ ψ`.
 
@@ -319,7 +319,7 @@ affecting left orthogonality.
     ( is-orth-ψ-ϕ (\ (s , t) → σ' (t , s)))
 ```
 
-### Stability under exponentiation
+### Exponentiation
 
 If `ϕ ⊂ ψ` is left orthogonal to `α : A' → A` then so is `χ × ϕ ⊂ χ × ψ` for
 every other shape `χ`.
@@ -402,7 +402,7 @@ extensionality.
     ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ is-orth-ψ-ϕ)
 ```
 
-### Stability under exact pushouts
+### Exact pushouts
 
 For any two shapes `ϕ, ψ ⊂ I`, if `ϕ ∩ ψ ⊂ ϕ` is left orthogonal to
 `α : A' → A`, then so is `ψ ⊂ ϕ ∪ ψ`.
@@ -482,6 +482,70 @@ stability under pushout products.
       ( is-orth-ψ-ϕ))
 ```
 
+### Functorial isomorphisms of shape inclusion
+
+If two pairs of shape inclusions `ϕ ⊂ ψ` and `ζ ⊂ χ` are isomorphic, then
+`ϕ ⊂ ψ` is left orthogonal if and only if `ζ ⊂ χ` is left orthogonal.
+
+```rzk
+#def is-right-orthogonal-to-shape-isomorphism'
+  ( A' A : U)
+  ( α : A' → A)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( ((f , F) , (e , E)) : functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ)
+  : is-right-orthogonal-to-shape I ψ ϕ A' A α
+  →  is-right-orthogonal-to-shape J χ ζ A' A α
+  :=
+  is-homotopy-cartesian-in-cube
+  ( ζ → A') (\ σ' → (t : χ) → A' [ζ t ↦ σ' t])
+  ( ζ → A) (\ σ' → (t : χ) → A [ζ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+  ( ϕ → A) (\ σ' → (t : ψ) → A [ϕ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( first (f A')) ( first (f A))
+  ( e A' A α)
+  ( \ σ' → first (F A' σ')) (\ σ → first (F A σ))
+  ( E A' A α)
+  ( \ σ' → second (F A' σ')) (\ σ → second (F A σ))
+
+#def is-right-orthogonal-to-shape-isomorphism
+  ( A' A : U)
+  ( α : A' → A)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( ((f , F) , (e , E)) : functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ)
+  : is-right-orthogonal-to-shape J χ ζ A' A α
+  → is-right-orthogonal-to-shape I ψ ϕ A' A α
+  :=
+  is-homotopy-cartesian-in-cube'
+  ( ζ → A') (\ σ' → (t : χ) → A' [ζ t ↦ σ' t])
+  ( ζ → A) (\ σ' → (t : χ) → A [ζ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( ϕ → A') (\ σ' → (t : ψ) → A' [ϕ t ↦ σ' t])
+  ( ϕ → A) (\ σ' → (t : ψ) → A [ϕ t ↦ σ' t])
+  ( \ σ' t → α (σ' t))
+  ( \ _ τ' t → α (τ' t))
+  ( first (f A')) ( first (f A))
+  ( e A' A α)
+  ( \ σ' → first (F A' σ')) (\ σ → first (F A σ))
+  ( E A' A α)
+  ( \ σ' → second (F A' σ')) (\ σ → second (F A σ))
+  ( second (second (f A')))
+```
+
 ## Stability properties of right orthogonal maps
 
 Now we change perspective. We fix a shape inclusion `ϕ ⊂ ψ` and investigate
@@ -523,7 +587,7 @@ Right orthogonality is closed under homotopy.
     ( first (first (funext A' (\ _ → A) α β)) h)
 ```
 
-### Stability under composition
+### Composition
 
 ```rzk
 #variables A'' A' A : U
@@ -596,7 +660,7 @@ right (whether it is right orthogonal or not.)
     ( is-orth-ψ-ϕ-αα')
 ```
 
-### Stability under pullback
+### Pullback
 
 Right orthogonal maps are stable under pullback. More precisely: If `α : A' → A`
 is right orthogonal, then so is the second projection
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 0afb7daf..89889f5d 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -309,8 +309,6 @@ The first step is to identify the pair `{0} ⊂ Δ¹` with the pair of subshapes
 `{1} ⊂ right-leg-of-Λ` of `Λ`.
 
 ```rzk
-#def right-leg-of-Λ : Λ → TOPE
-  := \ (t, s) → t ≡ 1₂
 
 #def is-equiv-Δ¹-to-right-leg-of-Λ-rel-start
   ( B : U)

From 3990b9c3814010a26161864cf5c9d00f1d660937 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 23:07:52 +0100
Subject: [PATCH 08/11] improve exposition

---
 .../02-simplicial-type-theory.rzk.md          | 36 +++++++++++++------
 1 file changed, 26 insertions(+), 10 deletions(-)

diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
index 5feded51..0278b82f 100644
--- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md
+++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
@@ -352,9 +352,7 @@ describe this isomorphism on representables.
   ( ζ : χ → TOPE)
   : U
   :=
-    ( Σ ( f
-          : (A : U)
-          → Equiv (ζ → A) (ϕ → A))
+    ( Σ ( f : (A : U) → Equiv (ζ → A) (ϕ → A))
       , ( ( A : U)
         → ( σ : ζ → A)
         → ( Equiv
@@ -391,17 +389,35 @@ describe this isomorphism on representables.
             = ( first (F A (\ (t : ζ) → α (σ' t))) (\ (t : χ) → α (τ' t))))))
 ```
 
-As an example, we show establish the canonical isomorphism between the pairs
-`{0} ⊂ Δ¹` and `{1} ⊂ right-leg-of-Λ`. It really just boils down to the two
-formulas `\ τ (t , s) → τ s` describing the map
-`(Δ¹ → A) → (right-leg-of-Λ → A)` and `\ υ s → υ (1₂ , s)` describing its
-inverse. All of the necessary coherences are just `refl`. Unfortunately, there
-is currently no better way to define this functorial isomorphism other than
-spelling out the following monstrosity:
+In practice, the isomorphisms are usually given via an explicit formula, which
+would define a map `ψ → ϕ` if `ψ` and `ϕ` were themselves types. In this case
+all the coherences are just `refl`, hence it is easy to produce a term of type
+`functorial-isomorphism-shape-inclusions I ψ ϕ J χ ζ`.
+
+For example, consider the two shape inclusions `{0} ⊂ Δ¹` (subshapes of `2`) and
+`{1} ⊂ right-leg-of-Λ` (subshapes of `2 × 2`), where
 
 ```rzk
 #def right-leg-of-Λ : Λ → TOPE
   := \ (t, s) → t ≡ 1₂
+```
+
+These two shape inclusions are canonically isomorphic via the formulas
+
+```
+-- not valid rzk code
+#def f : Δ¹ → right-leg-of-Λ
+  \ s → (1₂ , s)
+
+#def g : right-leg-of-Λ → Δ¹
+  \ (t , s) → s
+```
+
+We turn these formulas into a functorial shape inclusion as follows.
+Unfortunately we have to repeat the same formula multiple times, leading to some
+ugly boilerplate code.
+
+```rzk
 
 #def isomorphism-0-Δ¹-1-right-leg-of-Λ
   : isomorphism-shape-inclusions

From ff675fc2be4469f2640c4e2ff05b1c122b688bac Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 9 Nov 2023 23:25:08 +0100
Subject: [PATCH 09/11] autoformat

---
 src/hott/11-homotopy-pullbacks.rzk.md                | 4 ----
 src/simplicial-hott/02-simplicial-type-theory.rzk.md | 1 -
 2 files changed, 5 deletions(-)

diff --git a/src/hott/11-homotopy-pullbacks.rzk.md b/src/hott/11-homotopy-pullbacks.rzk.md
index 3c67c9c9..84b336c1 100644
--- a/src/hott/11-homotopy-pullbacks.rzk.md
+++ b/src/hott/11-homotopy-pullbacks.rzk.md
@@ -240,7 +240,6 @@ maps `β → α` and obtain another homotopy cartesian square.
         ( is-equiv-transport A C (α (s' b')) (s (β b')) (η b'))
 ```
 
-
 ## Pasting calculus for homotopy cartesian squares
 
 Currently our notion of squares is not symmetric, since the vertical maps are
@@ -248,8 +247,6 @@ given by type families, i.e. they are _display maps_, while the horizontal maps
 are arbitrary. Therefore we distinquish between the vertical and the horizontal
 pasting calculus.
 
-
-
 ### Vertical calculus
 
 The following vertical composition and cancellation laws follow easily from the
@@ -587,7 +584,6 @@ The converse holds provided that the map `f' : A' → B'` has a section.
 #end is-homotopy-cartesian-in-cube
 ```
 
-
 ## Fiber products
 
 Given two type families `B C : A → U`, we can form their **fiberwise product**.
diff --git a/src/simplicial-hott/02-simplicial-type-theory.rzk.md b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
index 0278b82f..973e5dab 100644
--- a/src/simplicial-hott/02-simplicial-type-theory.rzk.md
+++ b/src/simplicial-hott/02-simplicial-type-theory.rzk.md
@@ -418,7 +418,6 @@ Unfortunately we have to repeat the same formula multiple times, leading to some
 ugly boilerplate code.
 
 ```rzk
-
 #def isomorphism-0-Δ¹-1-right-leg-of-Λ
   : isomorphism-shape-inclusions
     (2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)

From a3c41392599115300a65ee5737e729239513167c Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Sat, 11 Nov 2023 11:30:11 +0100
Subject: [PATCH 10/11] minor edit

---
 src/simplicial-hott/07-discrete.rzk.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/simplicial-hott/07-discrete.rzk.md b/src/simplicial-hott/07-discrete.rzk.md
index b051315a..2b419242 100644
--- a/src/simplicial-hott/07-discrete.rzk.md
+++ b/src/simplicial-hott/07-discrete.rzk.md
@@ -440,13 +440,13 @@ Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹` is the pro
 `Δ¹` with the left anodyne pair `{0} ⊂ Δ¹`, hence left anodyne itself.
 
 ```rzk
-#def is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹
+#def is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹ uses (extext)
   : is-left-anodyne ( 2 × 2)
     ( \ ts → Δ¹×Δ¹ ts) ( \ ts → left-leg-of-Λ ts)
   :=
-  \ A' A α is-left-fib-α →
+  \ A' A α →
     is-right-orthogonal-to-shape-product extext A' A α
-      2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂) is-left-fib-α
+      2 Δ¹ 2 Δ¹ ( \ s → s ≡ 0₂)
 ```
 
 Next, we use the left cancellation of left anodyne shape inclusions to deduce

From 0d4f4576e1bef188173e837e93d98834162ac5fe Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Sat, 11 Nov 2023 11:43:22 +0100
Subject: [PATCH 11/11] typo in mkdocs.yaml

---
 mkdocs.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/mkdocs.yml b/mkdocs.yml
index edb77cb8..d452ca56 100644
--- a/mkdocs.yml
+++ b/mkdocs.yml
@@ -27,7 +27,7 @@ nav:
   - Simplicial HoTT:
       - Simplicial Type Theory: simplicial-hott/02-simplicial-type-theory.rzk.md
       - Extension Types: simplicial-hott/03-extension-types.rzk.md
-      - Right Orthogonal Fibrations: right-orthogonal/04-right-orthogonal.rzk.md
+      - Right Orthogonal Fibrations: simplicial-hott/04-right-orthogonal.rzk.md
       - Segal Types: simplicial-hott/05-segal-types.rzk.md
       - 2-Category of Segal Types: simplicial-hott/06-2cat-of-segal-types.rzk.md
       - Discrete Types: simplicial-hott/07-discrete.rzk.md