From 0cf79a0b4a6298ddbcfce5e2c9399b11f4901342 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Wed, 27 Sep 2023 17:17:47 +0200
Subject: [PATCH 1/8] start stating some intermediate steps

---
 src/simplicial-hott/08-covariant.rzk.md | 40 +++++++++++++++++++++++++
 1 file changed, 40 insertions(+)

diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index dab6e1ff..5d79560f 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -396,6 +396,46 @@ Finally, we deduce the theorem by some straightforward logical bookkeeping.
       is-covariant-is-naive-left-fibration A C)
 ```
 
+### Segal types vs naive left fibrations
+
+We aim to prove that for any naive left fibration `α : A' → A`,
+if `A` is a Segal type, then so is `A'`.
+
+```rzk title="RS17, Theorem 8.8, categorical version"
+#section is-segal-is-naive-left-fibration-is-segal
+#variables A' A : U
+#variable α : A' → A
+
+#assume is-nlf-α : is-naive-left-fibration A A' α
+#assume is-segal-A : is-segal A
+
+#def is-homotopy-cartesian-01-Λ uses (is-nlf-α)
+  : is-homotopy-cartesian
+      ( Δ¹ → A') ( \ σ → coslice A' (σ 1₂))
+      ( Δ¹ → A) ( \ σ → coslice A (σ 1₂))
+      ( \ σ t → α (σ t)) ( \ σ → coslice-fun A' A α (σ 1₂))
+  :=
+    \ σ → is-nlf-α (σ 1₂)
+
+#def is-homotopy-cartesian-0-Δ¹ uses (is-nlf-α)
+  : is-homotopy-cartesian
+        A' ( \ a' → (t : Δ¹) → A' [t ≡ 0₂ ↦ a'] )
+        A ( \ a → (t : Δ¹) → A [t ≡ 0₂ ↦ a] )
+        α ( \ _ σ' t → α (σ' t))
+  :=
+    \ a' → U
+
+#def is-homotopy-cartesian-Δ¹-t0-Δ¹×Δ¹ uses (is-nlf-α)
+  : is-homotopy-cartesian
+      ( Δ¹ → A') ( \ σ' → ((t,s) : Δ¹×Δ¹) → A' [s ≡ 0₂ ↦ σ t])
+      ( Δ¹ → A) ( \ σ → ((t,s) : Δ¹×Δ¹) → A [s ≡ 0₂ ↦ σ t])
+      ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
+  := \ σ' → U
+
+
+#end is-segal-is-naive-left-fibration-is-segal
+```
+
 ## Representable covariant families
 
 If `A` is a Segal type and `a : A` is any term,

From 2172171c06d35df92f70b13f62bd6d9d3d069418 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Wed, 27 Sep 2023 22:29:37 +0200
Subject: [PATCH 2/8] add 0-Delta1

---
 src/simplicial-hott/08-covariant.rzk.md | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 5d79560f..5e5f078c 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -411,11 +411,11 @@ if `A` is a Segal type, then so is `A'`.
 
 #def is-homotopy-cartesian-01-Λ uses (is-nlf-α)
   : is-homotopy-cartesian
-      ( Δ¹ → A') ( \ σ → coslice A' (σ 1₂))
+      ( Δ¹ → A') ( \ σ' → coslice A' (σ' 1₂))
       ( Δ¹ → A) ( \ σ → coslice A (σ 1₂))
-      ( \ σ t → α (σ t)) ( \ σ → coslice-fun A' A α (σ 1₂))
+      ( \ σ' t → α (σ' t)) ( \ σ' → coslice-fun A' A α (σ' 1₂))
   :=
-    \ σ → is-nlf-α (σ 1₂)
+    \ σ' → is-nlf-α (σ' 1₂)
 
 #def is-homotopy-cartesian-0-Δ¹ uses (is-nlf-α)
   : is-homotopy-cartesian
@@ -423,11 +423,20 @@ if `A` is a Segal type, then so is `A'`.
         A ( \ a → (t : Δ¹) → A [t ≡ 0₂ ↦ a] )
         α ( \ _ σ' t → α (σ' t))
   :=
-    \ a' → U
+    \ a' →
+      is-equiv-equiv-is-equiv
+        ( coslice' A' a') (coslice' A (α a'))
+        ( \ σ' t → α (σ' t))
+        ( coslice A' a') (coslice A (α a'))
+        ( coslice-fun A' A α a')
+        ( ( coslice-coslice' A' a', coslice-coslice' A (α a')), \ _ → refl)
+        ( is-equiv-coslice-coslice' A' a')
+        ( is-equiv-coslice-coslice' A (α a'))
+        ( is-nlf-α a')
 
 #def is-homotopy-cartesian-Δ¹-t0-Δ¹×Δ¹ uses (is-nlf-α)
   : is-homotopy-cartesian
-      ( Δ¹ → A') ( \ σ' → ((t,s) : Δ¹×Δ¹) → A' [s ≡ 0₂ ↦ σ t])
+      ( Δ¹ → A') ( \ σ' → ((t,s) : Δ¹×Δ¹) → A' [s ≡ 0₂ ↦ σ' t])
       ( Δ¹ → A) ( \ σ → ((t,s) : Δ¹×Δ¹) → A [s ≡ 0₂ ↦ σ t])
       ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
   := \ σ' → U

From abbc4aa4451cb5f42a86056a07226025ab619f6c Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Thu, 28 Sep 2023 21:55:39 +0200
Subject: [PATCH 3/8] add step about \Delta^1\times

---
 src/simplicial-hott/08-covariant.rzk.md | 37 ++++++++++++-------------
 1 file changed, 18 insertions(+), 19 deletions(-)

diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 3d47f17b..f264708f 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -24,6 +24,8 @@ Some of the definitions in this file rely on extension extensionality:
 ```rzk
 #assume extext : ExtExt
 #assume weakfunext : WeakFunExt
+#assume naiveextext : NaiveExtExt
+
 ```
 
 ## Dependent hom types
@@ -460,6 +462,7 @@ if `A` is a Segal type, then so is `A'`.
 
 ```rzk title="RS17, Theorem 8.8, categorical version"
 #section is-segal-is-naive-left-fibration-is-segal
+
 #variables A' A : U
 #variable α : A' → A
 
@@ -474,29 +477,25 @@ if `A` is a Segal type, then so is `A'`.
   :=
     \ σ' → is-nlf-α (σ' 1₂)
 
-#def is-homotopy-cartesian-0-Δ¹ uses (is-nlf-α)
-  : is-homotopy-cartesian
-        A' ( \ a' → (t : Δ¹) → A' [t ≡ 0₂ ↦ a'] )
-        A ( \ a → (t : Δ¹) → A [t ≡ 0₂ ↦ a] )
-        α ( \ _ σ' t → α (σ' t))
+#def is-j-orthogonal-0-Δ¹-α uses (is-nlf-α)
+  : is-j-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α
   :=
     \ a' →
       is-equiv-equiv-is-equiv
-        ( coslice' A' a') (coslice' A (α a'))
+        ( coslice' A' (a' 0₂)) (coslice' A (α (a' 0₂)))
         ( \ σ' t → α (σ' t))
-        ( coslice A' a') (coslice A (α a'))
-        ( coslice-fun A' A α a')
-        ( ( coslice-coslice' A' a', coslice-coslice' A (α a')), \ _ → refl)
-        ( is-equiv-coslice-coslice' A' a')
-        ( is-equiv-coslice-coslice' A (α a'))
-        ( is-nlf-α a')
-
-#def is-homotopy-cartesian-Δ¹-t0-Δ¹×Δ¹ uses (is-nlf-α)
-  : is-homotopy-cartesian
-      ( Δ¹ → A') ( \ σ' → ((t,s) : Δ¹×Δ¹) → A' [s ≡ 0₂ ↦ σ' t])
-      ( Δ¹ → A) ( \ σ → ((t,s) : Δ¹×Δ¹) → A [s ≡ 0₂ ↦ σ t])
-      ( \ σ' t → α (σ' t)) ( \ _ τ' x → α (τ' x) )
-  := \ σ' → U
+        ( coslice A' (a' 0₂)) (coslice A (α (a' 0₂)))
+        ( coslice-fun A' A α (a' 0₂))
+        ( ( coslice-coslice' A' (a' 0₂), coslice-coslice' A (α (a' 0₂))),
+          \ _ → refl)
+        ( is-equiv-coslice-coslice' A' (a' 0₂))
+        ( is-equiv-coslice-coslice' A (α (a' 0₂)))
+        ( is-nlf-α (a' 0₂))
+
+#def is-homotopy-cartesian-Δ¹-Δ¹×Δ¹-α uses (naiveextext is-nlf-α)
+  : is-j-orthogonal-to-shape (2 × 2) (Δ¹×Δ¹) (\ (t,s) → s ≡ 0₂) A' A α
+  := is-j-orthogonal-to-shape-× naiveextext
+        2 Δ¹ 2 Δ¹ (\ s → s ≡ 0₂) A' A α is-j-orthogonal-0-Δ¹-α
 
 #end is-segal-is-naive-left-fibration-is-segal
 ```

From 2a8e92b24a73bc9bf4cb5c916b6ef4745d9dc3a0 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.fritz.box>
Date: Thu, 5 Oct 2023 17:43:44 +0200
Subject: [PATCH 4/8] stub

---
 src/simplicial-hott/05-segal-types.rzk.md | 11 +++-
 src/simplicial-hott/08-covariant.rzk.md   | 67 +++++++++++++----------
 2 files changed, 46 insertions(+), 32 deletions(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 6f2d33e4..5193b281 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -349,13 +349,18 @@ The underlying horn of a simplex:
   := \ f t → f t
 ```
 
-This provides an alternate definition of Segal types.
+This provides an alternate definition of Segal types as types which are local
+for the inclusion `Λ ⊂ Δ¹`.
 
 ```rzk
 #def is-local-horn-inclusion
+  : U → U
+  := is-local-type (2 × 2) Δ² (\ t → Λ t)
+
+#def is-local-horn-inclusion-explicit
   ( A : U)
-  : U
-  := is-equiv (Δ² → A) (Λ → A) (horn-restriction A)
+  : is-local-horn-inclusion A = is-equiv (Δ² → A) (Λ → A) (horn-restriction A)
+  := refl
 ```
 
 Now we prove this definition is equivalent to the original one. Here, we prove
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 3bcb324c..97a0ff42 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -222,6 +222,36 @@ As a sanity check we unpack the definition of `is-naive-left-fibration`.
   := refl
 ```
 
+### Naive left fibration via right orthogonality
+
+A map `α : A' → A` is a naive left fibration if and only if
+it is right orthogonal with respect to the shape inclusion `{0} ⊂ Δ¹`.
+
+```rzk
+#section naive-left-fibration-iff-has-unique-0-Δ¹-extensions
+
+#variables A' A : U
+#variable α : A' → A
+
+#def is-right-orthogonal-to-0-Δ¹-is-naive-left-fibration
+  ( is-nlf : is-naive-left-fibration A A' α)
+  : is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α
+  :=
+    \ a' →
+      is-equiv-equiv-is-equiv
+        ( coslice' A' (a' 0₂)) (coslice' A (α (a' 0₂)))
+        ( \ σ' t → α (σ' t))
+        ( coslice A' (a' 0₂)) (coslice A (α (a' 0₂)))
+        ( coslice-fun A' A α (a' 0₂))
+        ( ( coslice-coslice' A' (a' 0₂), coslice-coslice' A (α (a' 0₂))),
+          \ _ → refl)
+        ( is-equiv-coslice-coslice' A' (a' 0₂))
+        ( is-equiv-coslice-coslice' A (α (a' 0₂)))
+        ( is-nlf (a' 0₂))
+
+#end naive-left-fibration-iff-has-unique-0-Δ¹-extensions
+```
+
 ### Naive left fibrations vs. covariant families
 
 We aim to prove that a type family `#!rzk C : A → U`, is covariant if and only
@@ -466,36 +496,15 @@ if `A` is a Segal type, then so is `A'`.
 #variables A' A : U
 #variable α : A' → A
 
-#assume is-nlf-α : is-naive-left-fibration A A' α
-#assume is-segal-A : is-segal A
-
-#def is-homotopy-cartesian-01-Λ uses (is-nlf-α)
-  : is-homotopy-cartesian
-      ( Δ¹ → A') ( \ σ' → coslice A' (σ' 1₂))
-      ( Δ¹ → A) ( \ σ → coslice A (σ 1₂))
-      ( \ σ' t → α (σ' t)) ( \ σ' → coslice-fun A' A α (σ' 1₂))
-  :=
-    \ σ' → is-nlf-α (σ' 1₂)
-
-#def is-j-orthogonal-0-Δ¹-α uses (is-nlf-α)
-  : is-j-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α
-  :=
-    \ a' →
-      is-equiv-equiv-is-equiv
-        ( coslice' A' (a' 0₂)) (coslice' A (α (a' 0₂)))
-        ( \ σ' t → α (σ' t))
-        ( coslice A' (a' 0₂)) (coslice A (α (a' 0₂)))
-        ( coslice-fun A' A α (a' 0₂))
-        ( ( coslice-coslice' A' (a' 0₂), coslice-coslice' A (α (a' 0₂))),
-          \ _ → refl)
-        ( is-equiv-coslice-coslice' A' (a' 0₂))
-        ( is-equiv-coslice-coslice' A (α (a' 0₂)))
-        ( is-nlf-α (a' 0₂))
+#variable is-orth-0-Δ¹-α
+  : is-right-orthogonal-to-shape 2 Δ¹ ( \ t → t ≡ 0₂) A' A α
+#variable has-ue-Λ-Δ²-A
+  : has-unique-extensions (2 × 2) Δ² (\ (t, s) → s ≡ 0₂ ∨ t ≡ 1₂) A
 
-#def is-homotopy-cartesian-Δ¹-Δ¹×Δ¹-α uses (naiveextext is-nlf-α)
-  : is-j-orthogonal-to-shape (2 × 2) (Δ¹×Δ¹) (\ (t,s) → s ≡ 0₂) A' A α
-  := is-j-orthogonal-to-shape-× naiveextext
-        2 Δ¹ 2 Δ¹ (\ s → s ≡ 0₂) A' A α is-j-orthogonal-0-Δ¹-α
+#def is-homotopy-cartesian-Δ¹-Δ¹×Δ¹-α uses (naiveextext is-orth-0-Δ¹-α)
+  : is-right-orthogonal-to-shape (2 × 2) (Δ¹×Δ¹) (\ (t,s) → s ≡ 0₂) A' A α
+  := is-right-orthogonal-to-shape-× naiveextext
+       A' A α 2 Δ¹ 2 Δ¹ (\ s → s ≡ 0₂) is-orth-0-Δ¹-α
 
 #end is-segal-is-naive-left-fibration-is-segal
 ```

From 0bb058465d702f16909e7df52524b78892d0d2ac Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Thu, 5 Oct 2023 23:42:16 +0200
Subject: [PATCH 5/8] prove thm 8.8

---
 .../04-right-orthogonal.rzk.md                |  26 ++-
 src/simplicial-hott/05-segal-types.rzk.md     |  16 +-
 src/simplicial-hott/08-covariant.rzk.md       | 209 +++++++++++++++---
 3 files changed, 213 insertions(+), 38 deletions(-)

diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
index 35baa188..c45ecc61 100644
--- a/src/simplicial-hott/04-right-orthogonal.rzk.md
+++ b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -222,7 +222,7 @@ and relies on (the naive form of) extension extensionality.
   ( ϕ : ψ → TOPE )
   ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ϕ A' A α)
   : is-right-orthogonal-to-shape
-      ( J × I) ( shape-prod J I χ ψ) ( \ (t,s) → χ t ∧ ϕ s) A' A α
+      ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s) A' A α
   :=
     \ ( σ' : ( (t,s) : J × I | χ t ∧ ϕ s) → A') →
       (
@@ -323,7 +323,7 @@ The property of having unique extension
 can be pulled back along any right orthogonal map.
 
 ```rzk
-#def has-unique-extensions-right-orthogonal-has-unique-extensions
+#def has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
   ( I : CUBE)
   ( ψ : I → TOPE)
   ( ϕ : ψ → TOPE)
@@ -386,6 +386,26 @@ and the fiber of the restriction map `(ψ → A) → (ϕ → A)`.
             ( ψ → A) (ϕ → A) ( \ τ t → τ t)
             ( is-lt-ψ-ϕ-A)
             ( σ))
-
 #end is-local-type
 ```
+
+Since the property of having unique extensions passes from the codomain to the domain
+of a right orthogonal map, the same is true for locality of types.
+
+```rzk
+#def is-local-type-domain-right-orthogonal-is-local-type-codomain
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-orth-α : is-right-orthogonal-to-shape I ψ ϕ A' A α)
+  ( is-local-A : is-local-type I ψ ϕ A)
+  : is-local-type I ψ ϕ A'
+  :=
+    is-local-type-has-unique-extensions I ψ ϕ A'
+      ( has-unique-extensions-domain-right-orthogonal-has-unique-extensions-codomain
+          I ψ ϕ A' A α is-orth-α
+          ( has-unique-extensions-is-local-type I ψ ϕ A is-local-A))
+
+```
diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index 5193b281..f742d10a 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -357,7 +357,7 @@ for the inclusion `Λ ⊂ Δ¹`.
   : U → U
   := is-local-type (2 × 2) Δ² (\ t → Λ t)
 
-#def is-local-horn-inclusion-explicit
+#def is-local-horn-inclusion-unpacked
   ( A : U)
   : is-local-horn-inclusion A = is-equiv (Δ² → A) (Λ → A) (horn-restriction A)
   := refl
@@ -1610,7 +1610,6 @@ Interchange law
 ## Inner anodyne maps
 
 ```rzk title="RS17, Definition 5.19"
-
 #def is-inner-anodyne
   (I : CUBE)
   (ψ : I → TOPE)
@@ -1778,6 +1777,19 @@ The cofibration Λ²₁ → Δ² is 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 products of morphisms.
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 97a0ff42..4d865fb8 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -222,20 +222,29 @@ As a sanity check we unpack the definition of `is-naive-left-fibration`.
   := refl
 ```
 
-### Naive left fibration via right orthogonality
+### Naive left fibrations via right `{0}⊂Δ¹`-orthogonality
 
-A map `α : A' → A` is a naive left fibration if and only if
-it is right orthogonal with respect to the shape inclusion `{0} ⊂ Δ¹`.
+A map `α : A' → A` is called a left fibration if it is right orthogonal
+to the shape inclusion `{0} ⊂ Δ¹`.
 
 ```rzk
-#section naive-left-fibration-iff-has-unique-0-Δ¹-extensions
+#section is-left-fibration
 
 #variables A' A : U
 #variable α : A' → A
 
-#def is-right-orthogonal-to-0-Δ¹-is-naive-left-fibration
+#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
+-- TODO : prove converse
   ( is-nlf : is-naive-left-fibration A A' α)
-  : is-right-orthogonal-to-shape 2 Δ¹ ( \ s → s ≡ 0₂) A' A α
+  : is-left-fibration
   :=
     \ a' →
       is-equiv-equiv-is-equiv
@@ -249,7 +258,144 @@ it is right orthogonal with respect to the shape inclusion `{0} ⊂ Δ¹`.
         ( is-equiv-coslice-coslice' A (α (a' 0₂)))
         ( is-nlf (a' 0₂))
 
-#end naive-left-fibration-iff-has-unique-0-Δ¹-extensions
+#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-inner-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-inner-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-inner-fibration)
+
+```
+
+Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹`
+is the product of `Δ¹` with the pair `{0} ⊂ Δ¹`.
+
+```rzk
+#def is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-inner-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-× 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-inner-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-inner-fibration)
+      ( is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-inner-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-inner-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-inner-fibration-is-segal-codomain uses (naiveextext)
+  ( A' A : U)
+  ( α : A' → A)
+  ( is-inner-fib-α : is-inner-fibration A' A α)
+  ( is-segal-A : is-segal A)
+  : is-segal A'
+  :=
+    is-segal-is-local-horn-inclusion A'
+      ( is-local-type-domain-right-orthogonal-is-local-type-codomain
+        ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α
+        ( is-inner-fib-α)
+        ( is-local-horn-inclusion-is-segal A is-segal-A))
 ```
 
 ### Naive left fibrations vs. covariant families
@@ -428,6 +574,29 @@ We prove that the total space of a covariant family over a Segal type is a Segal
 type. We split the proof into intermediate steps. Let `A` be a type and a type
 family `#!rzk C : A → U`.
 
+### Category theoretic proof
+
+For every covariant family `C : A → U`, the projection `Σ A, C → A`
+is an left 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-space-covariant-family-is-segal-base uses (naiveextext)
+  ( A : U)
+  ( C : A → U)
+  ( is-covariant-C : is-covariant A C)
+  : is-segal A → is-segal (total-type A C)
+  :=
+    is-segal-domain-inner-fibration-is-segal-codomain
+      ( total-type A C) A (\ (a,_) → a)
+      ( is-inner-fibration-is-left-fibration (total-type A C) A (\ (a,_) → a)
+          ( is-left-fibration-is-naive-left-fibration
+              ( total-type A C) A (\ (a,_) → a)
+              ( is-naive-left-fibration-is-covariant A C is-covariant-C)))
+```
+
+### Type theoretic proof
+
 We examine the fibers of the horn restriction on the total space of `C`. First
 note we have the equivalences:
 
@@ -483,32 +652,6 @@ the proof of Theorem 8.8 in RS17. The following maps will be packed into some
   := \ ( f,μ ) → ( ( \ t → f t, \ t → μ t  ), refl )
 ```
 
-### Segal types vs naive left fibrations
-
-We give an alternative proof using the calculus of homotopy cartesian squares.
-
-We aim to prove that for any naive left fibration `α : A' → A`,
-if `A` is a Segal type, then so is `A'`.
-
-```rzk title="RS17, Theorem 8.8, categorical version"
-#section is-segal-is-naive-left-fibration-is-segal
-
-#variables A' A : U
-#variable α : A' → A
-
-#variable is-orth-0-Δ¹-α
-  : is-right-orthogonal-to-shape 2 Δ¹ ( \ t → t ≡ 0₂) A' A α
-#variable has-ue-Λ-Δ²-A
-  : has-unique-extensions (2 × 2) Δ² (\ (t, s) → s ≡ 0₂ ∨ t ≡ 1₂) A
-
-#def is-homotopy-cartesian-Δ¹-Δ¹×Δ¹-α uses (naiveextext is-orth-0-Δ¹-α)
-  : is-right-orthogonal-to-shape (2 × 2) (Δ¹×Δ¹) (\ (t,s) → s ≡ 0₂) A' A α
-  := is-right-orthogonal-to-shape-× naiveextext
-       A' A α 2 Δ¹ 2 Δ¹ (\ s → s ≡ 0₂) is-orth-0-Δ¹-α
-
-#end is-segal-is-naive-left-fibration-is-segal
-```
-
 ## Representable covariant families
 
 If `A` is a Segal type and `a : A` is any term, then `hom A a` defines a

From 755e5882de1fe9b05bb99ef60f899a72a2154851 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 6 Oct 2023 00:17:38 +0200
Subject: [PATCH 6/8] minor edit

---
 src/simplicial-hott/08-covariant.rzk.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 4d865fb8..2e7369d3 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -337,7 +337,8 @@ to deduce that the pair `left-leg-of-Λ ⊂ Λ` is left orthogonal.
 ```
 
 Furthermore, we observe that the pair `left-leg-of-Δ ⊂ Δ¹×Δ¹`
-is the product of `Δ¹` with the pair `{0} ⊂ Δ¹`.
+is the product of `Δ¹` with the left orthogonal pair `{0} ⊂ Δ¹`,
+hence left orthogonal itself.
 
 ```rzk
 #def is-right-orthogonal-to-left-leg-of-Λ-Δ¹×Δ¹-is-inner-fibration

From 94f0477d2f68e223b43a8ad3daa3aa97bf345d05 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 6 Oct 2023 00:26:54 +0200
Subject: [PATCH 7/8] minor edit

---
 src/simplicial-hott/08-covariant.rzk.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 2e7369d3..69d55879 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -222,7 +222,7 @@ As a sanity check we unpack the definition of `is-naive-left-fibration`.
   := refl
 ```
 
-### Naive left fibrations via right `{0}⊂Δ¹`-orthogonality
+### 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} ⊂ Δ¹`.

From 6c71811c19f57ee373bc2a406590b31826064224 Mon Sep 17 00:00:00 2001
From: Tashi Walde <twalde@Tashis-MacBook-Air.local>
Date: Fri, 6 Oct 2023 11:15:33 +0200
Subject: [PATCH 8/8] fix mislabeling and add
 is-naive-left-fibration-is-inner-fibration

---
 src/simplicial-hott/05-segal-types.rzk.md |  2 +-
 src/simplicial-hott/08-covariant.rzk.md   | 40 ++++++++++++++++++-----
 2 files changed, 32 insertions(+), 10 deletions(-)

diff --git a/src/simplicial-hott/05-segal-types.rzk.md b/src/simplicial-hott/05-segal-types.rzk.md
index f742d10a..b1dea1ea 100644
--- a/src/simplicial-hott/05-segal-types.rzk.md
+++ b/src/simplicial-hott/05-segal-types.rzk.md
@@ -99,7 +99,7 @@ Slices and coslices can also be defined directly as extension types:
 
 #def coslice'
   : U
-  := ( t : Δ¹) → A[t ≡ 0₂ ↦ a]
+  := ( t : Δ¹) → A [t ≡ 0₂ ↦ a]
 
 #def coslice'-coslice
   : coslice A a → coslice'
diff --git a/src/simplicial-hott/08-covariant.rzk.md b/src/simplicial-hott/08-covariant.rzk.md
index 69d55879..5bf60aa6 100644
--- a/src/simplicial-hott/08-covariant.rzk.md
+++ b/src/simplicial-hott/08-covariant.rzk.md
@@ -242,7 +242,6 @@ This notion agrees with that of a naive left fibration.
 
 ```rzk
 #def is-left-fibration-is-naive-left-fibration
--- TODO : prove converse
   ( is-nlf : is-naive-left-fibration A A' α)
   : is-left-fibration
   :=
@@ -258,6 +257,30 @@ This notion agrees with that of a naive left fibration.
         ( is-equiv-coslice-coslice' A (α (a' 0₂)))
         ( is-nlf (a' 0₂))
 
+#def is-naive-left-fibration-is-left-fibration
+  ( is-lf : is-left-fibration)
+  : is-naive-left-fibration A A' α
+  :=
+    \ a' →
+      is-equiv-equiv-is-equiv'
+        ( coslice' A' a') (coslice' A (α a'))
+        ( \ σ' t → α (σ' t))
+        ( coslice A' a') (coslice A (α a'))
+        ( coslice-fun A' A α a')
+        ( ( coslice-coslice' A' a', coslice-coslice' A (α a')),
+          \ _ → refl)
+        ( is-equiv-coslice-coslice' A' a')
+        ( is-equiv-coslice-coslice' A (α a'))
+        ( is-lf (\ t → a'))
+
+#def is-naive-left-fibration-iff-is-left-fibration
+  : iff
+      ( is-naive-left-fibration A A' α)
+      ( is-left-fibration)
+  :=
+    ( is-left-fibration-is-naive-left-fibration,
+      is-naive-left-fibration-is-left-fibration)
+
 #end is-left-fibration
 ```
 
@@ -385,17 +408,17 @@ 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-inner-fibration-is-segal-codomain uses (naiveextext)
+#def is-segal-domain-left-fibration-is-segal-codomain uses (naiveextext)
   ( A' A : U)
   ( α : A' → A)
-  ( is-inner-fib-α : is-inner-fibration 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-domain-right-orthogonal-is-local-type-codomain
         ( 2 × 2) Δ² ( \ ts → Λ ts) A' A α
-        ( is-inner-fib-α)
+        ( is-inner-fibration-is-left-fibration A' A α is-left-fib-α)
         ( is-local-horn-inclusion-is-segal A is-segal-A))
 ```
 
@@ -588,12 +611,11 @@ It immediately follows that if `A` is Segal, then so is `Σ A, C`.
   ( is-covariant-C : is-covariant A C)
   : is-segal A → is-segal (total-type A C)
   :=
-    is-segal-domain-inner-fibration-is-segal-codomain
+    is-segal-domain-left-fibration-is-segal-codomain
       ( total-type A C) A (\ (a,_) → a)
-      ( is-inner-fibration-is-left-fibration (total-type A C) A (\ (a,_) → a)
-          ( is-left-fibration-is-naive-left-fibration
-              ( total-type A C) A (\ (a,_) → a)
-              ( is-naive-left-fibration-is-covariant A C is-covariant-C)))
+        ( is-left-fibration-is-naive-left-fibration
+            ( total-type A C) A (\ (a,_) → a)
+            ( is-naive-left-fibration-is-covariant A C is-covariant-C))
 ```
 
 ### Type theoretic proof