Reorganize proof that discrete types are Segal

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 α →

src/simplicial-hott/04-right-orthogonal.rzk.md

@@ -12,7 +12,6 @@ Some of the definitions in this file rely on extension extensionality or
 function extensionality:
 
 ```rzk
-#assume naiveextext : NaiveExtExt
 #assume extext : ExtExt
 #assume funext : FunExt
 ```
@@ -327,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)
@@ -344,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))
@@ -364,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)))
@@ -383,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)
@@ -432,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)
@@ -459,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)
@@ -1247,7 +1246,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)
@@ -1263,7 +1262,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 )
@@ -1346,8 +1345,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 extext)
+#def is-weak-anodyne-pushout-product-for-shape uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )
@@ -1367,8 +1365,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 extext)
+#def is-weak-anodyne-pushout-product-for-shape' uses (extext)
   ( I : CUBE)
   ( ψ : I → TOPE )
   ( ϕ : ψ → TOPE )

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

src/simplicial-hott/07-discrete.rzk.md

@@ -358,7 +358,181 @@ Every contractible type is automatically discrete.
 
 ## Discrete types are Segal types
 
-Discrete types are automatically Segal types.
+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)
+  ( α : 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, 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 `Λ`.
+
+```rzk
+#def is-left-anodyne-1-right-leg-of-Λ
+  : is-left-anodyne ( 2 × 2)
+    (\ ts → right-leg-of-Λ ts) ( \ (_,s) → s ≡ 0₂)
+  :=
+  \ A' A α →
+  is-right-orthogonal-to-shape-isomorphism A' A α
+  ( 2 × 2) (\ ts → right-leg-of-Λ ts) (\ (t , s) → t ≡ 1₂ ∧ s ≡ 0₂)
+  ( 2) (Δ¹) (\ t → t ≡ 0₂)
+  ( functorial-isomorphism-0-Δ¹-1-right-leg-of-Λ)
+```
+
+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 anodyne.
+
+```rzk
+#def left-leg-of-Λ : Λ → TOPE
+  := \ (t, s) → s ≡ 0₂
+
+#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-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 anodyne pair `{0} ⊂ Δ¹`, hence left anodyne itself.
+
+```rzk
+#def is-left-anodyne-left-leg-of-Λ-Δ¹×Δ¹ uses (extext)
+  : is-left-anodyne ( 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₂)
+```
+
+Next, we use the left cancellation of left anodyne shape inclusions to deduce
+that `Λ ⊂ Δ¹×Δ¹` is left anodyne.
+
+```rzk
+#def is-left-anodyne-Λ-Δ¹×Δ¹ uses (extext)
+  : is-left-anodyne ( 2 × 2)
+    ( \ ts → Δ¹×Δ¹ ts) ( \ ts → Λ ts)
+  :=
+  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 anodyne shape inclusion `Λ ⊂ Δ²`.
+
+```rzk
+#def is-left-anodyne-Λ-Δ² uses (extext)
+  : is-left-anodyne (2 × 2)
+    Δ² (\ t → Λ t)
+  :=
+  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-Λ-Δ¹×Δ¹)
+```
+
+which we can unpack to get the desired implication
+
+```rzk
+#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
+
+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
@@ -961,7 +1135,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