Theorem 8.8

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))
+
+```

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'
@@ -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-unpacked
   ( 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
@@ -1605,7 +1610,6 @@ Interchange law
 ## Inner anodyne maps
 
 ```rzk title="RS17, Definition 5.19"
-
 #def is-inner-anodyne
   (I : CUBE)
   (ψ : I → TOPE)
@@ -1773,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.

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
@@ -220,6 +222,206 @@ As a sanity check we unpack the definition of `is-naive-left-fibration`.
   := refl
 ```
 
+### 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} ⊂ Δ¹`.
+
+```rzk
+#section is-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
+  :=
+    \ 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₂))
+
+#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
+```
+
+### 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 left orthogonal pair `{0} ⊂ Δ¹`,
+hence left orthogonal itself.
+
+```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-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-domain-right-orthogonal-is-local-type-codomain
+        ( 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))
+```
+
 ### Naive left fibrations vs. covariant families
 
 We aim to prove that a type family `#!rzk C : A → U`, is covariant if and only
@@ -396,6 +598,28 @@ 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-left-fibration-is-segal-codomain
+      ( 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: