Merge pull request #126 from TashiWalde/anodyne

Anodyne shape inclusions
rzk-lang · Nov 4, 2023 · 97a439f · 97a439f
2 parents ea04084 + fb202f0
commit 97a439f
Show file tree

Hide file tree

Showing 2 changed files with 302 additions and 51 deletions.
diff --git a/src/simplicial-hott/04-right-orthogonal.rzk.md b/src/simplicial-hott/04-right-orthogonal.rzk.md
@@ -338,17 +338,17 @@ extensionality.
   ( ϕ : ψ → TOPE )
   ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ϕ A' A α)
   : is-right-orthogonal-to-shape
-      ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (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') →
-      ( ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t,s))])
+    \ ( σ' : ( (t , s) : J × I | χ t ∧ ϕ s) → A') →
+      ( ( \ ( τ : ( (t , s) : J × I | χ t ∧ ψ s) → A[ϕ s ↦ α (σ' (t , s))])
             ( t, s) →
           ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
-        , \ ( τ' : ( (t,s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t,s)]) →
+        , \ ( τ' : ( (t , s) : J × I | χ t ∧ ψ s) → A' [ϕ s ↦ σ' (t , s)]) →
             naiveextext
-              ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s)
+              ( J × I) ( \ (t , s) → χ t ∧ ψ s) ( \ (t , s) → χ t ∧ ϕ s)
               ( \ _ → A')
-              ( \ ( t,s) → σ' (t,s))
+              ( \ ( t,s) → σ' (t , s))
               ( \ ( t,s) →
                 ( first (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                   ( \ s' → α (τ' (t, s'))) s)
@@ -361,15 +361,15 @@ extensionality.
                   ( ( second (first (is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                     ( \ s' → τ' (t, s')))
                   ( s)))
-      , ( \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))])
+      , ( \ ( τ : ( (t , s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t , s))])
             ( t, s) →
           ( first (second (is-orth-ψ-ϕ (\ s' → σ' (t, s'))))) ( \ s' → τ (t, s')) s
-        , \ ( τ : ( (t,s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t,s))]) →
+        , \ ( τ : ( (t , s) : J × I | χ t ∧ ψ s) → A [ϕ s ↦ α (σ' (t , s))]) →
             naiveextext
-              ( J × I) ( \ (t,s) → χ t ∧ ψ s) ( \ (t,s) → χ t ∧ ϕ s)
+              ( J × I) ( \ (t , s) → χ t ∧ ψ s) ( \ (t , s) → χ t ∧ ϕ s)
               ( \ _ → A)
-              ( \ (t,s) → α (σ' (t,s)))
-              ( \ (t,s) →
+              ( \ (t , s) → α (σ' (t , s)))
+              ( \ (t , s) →
                 α ( ( first ( second ( is-orth-ψ-ϕ (\ s' → σ' (t, s')))))
                       ( \ s' → τ (t, s')) s))
               ( τ)
@@ -444,17 +444,17 @@ stability under pushout products.
   ( ϕ : ψ → TOPE )
   ( is-orth-ψ-ϕ : is-right-orthogonal-to-shape I ψ ϕ A' A α)
   : is-right-orthogonal-to-shape (J × I)
-    ( \ (t,s) → χ t ∧ ψ s)
-    ( \ (t,s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+    ( \ (t , s) → χ t ∧ ψ s)
+    ( \ (t , s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
     ( A') ( A) ( α)
   :=
     is-right-orthogonal-to-shape-left-cancel A' A α (J × I)
-    ( \ (t,s) → χ t ∧ ψ s)
-    ( \ (t,s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
-    ( \ (t,s) → χ t ∧ ϕ s)
+    ( \ (t , s) → χ t ∧ ψ s)
+    ( \ (t , s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+    ( \ (t , s) → χ t ∧ ϕ s)
     ( is-right-orthogonal-to-shape-pushout A' A α (J × I)
-      ( \ (t,s) → ζ t ∧ ψ s)
-      ( \ (t,s) → χ t ∧ ϕ s)
+      ( \ (t , s) → ζ t ∧ ψ s)
+      ( \ (t , s) → χ t ∧ ϕ s)
       ( is-right-orthogonal-to-shape-product A' A α J ( \ t → ζ t) I ψ ϕ
         (is-orth-ψ-ϕ)))
     ( is-right-orthogonal-to-shape-product A' A α J χ I ψ ϕ
@@ -476,8 +476,8 @@ stability under pushout products.
     ( A') ( A) ( α)
   :=
     is-right-orthogonal-to-shape-transpose A' A α J I
-    ( \ (t,s) → χ t ∧ ψ s)
-    ( \ (t,s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+    ( \ (t , s) → χ t ∧ ψ s)
+    ( \ (t , s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
     ( is-right-orthogonal-to-shape-pushout-product A' A α J χ ζ I ψ ϕ
       ( is-orth-ψ-ϕ))
 ```
@@ -1098,3 +1098,224 @@ every fiber of every map `α : A' → A` also has unique extensions.
     ( is-right-orthogonal-have-unique-extensions I ψ ϕ A' A
       ( has-ue-ψ-ϕ-A') ( has-ue-ψ-ϕ-A) ( α))
 ```
+
+## Anodyne shape inclusions
+
+Fix a shape inclusion `ϕ ⊂ ψ`. We say that another shape inclusion `χ ⊂ ζ` is
+**anodyne for** `ϕ ⊂ ψ`, is every map that is right orthogonal to `ϕ ⊂ ψ` is
+also right orthogonal to `χ ⊂ ζ`.
+
+```rzk
+#section anodyne
+
+#variable I₀ : CUBE
+#variable ψ₀ : I₀ → TOPE
+#variable ϕ₀ : ψ₀ → TOPE
+
+
+#def is-anodyne-for-shape
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( ϕ : ψ → TOPE)
+  : U
+  :=
+    ( ( A' : U) → (A : U) → (α : A' → A)
+    → is-right-orthogonal-to-shape I₀ ψ₀ ϕ₀ A' A α
+    → is-right-orthogonal-to-shape I ψ ϕ A' A α)
+```
+
+Of course every shape inclusion is anodyne for itself.
+
+```rzk
+#def is-anodyne-for-self
+  : is-anodyne-for-shape I₀ ψ₀ ϕ₀
+  := \ _ _ _ is-orth₀ → is-orth₀
+```
+
+All the stability properties above can be seen as implications between
+conditions of being anodyne.
+
+```rzk
+#def is-anodyne-comp-for-shape
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( χ : ψ → TOPE)
+  ( ϕ : χ → TOPE)
+  : is-anodyne-for-shape I ψ χ
+  → is-anodyne-for-shape I (\ t → χ t) (\ t → ϕ t)
+  → is-anodyne-for-shape I ψ (\ t → ϕ t)
+  :=
+    \ f g A' A α is-orth₀ →
+    ( is-right-orthogonal-to-shape-comp A' A α I ψ χ ϕ
+      ( f A' A α is-orth₀)
+      ( g A' A α is-orth₀))
+
+#def is-anodyne-left-cancel-for-shape
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( χ : ψ → TOPE)
+  ( ϕ : χ → TOPE)
+  : is-anodyne-for-shape I (\ t → χ t) (\ t → ϕ t)
+  → is-anodyne-for-shape I ψ (\ t → ϕ t)
+  → is-anodyne-for-shape I ψ χ
+  :=
+    \ f g A' A α is-orth₀ →
+    ( is-right-orthogonal-to-shape-left-cancel A' A α I ψ χ ϕ
+      ( f A' A α is-orth₀)
+      ( g A' A α is-orth₀))
+
+#def is-anodyne-right-cancel-retract-for-shape
+  ( I : CUBE)
+  ( ψ : I → TOPE)
+  ( χ : ψ → TOPE)
+  ( ϕ : χ → TOPE)
+  : is-functorial-shape-retract I ψ χ
+  → is-anodyne-for-shape I ψ (\ t → ϕ t)
+  → is-anodyne-for-shape I (\ t → χ t) (\ t → ϕ t)
+  :=
+    \ r f A' A α is-orth₀ →
+    ( 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)
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  : is-anodyne-for-shape I ψ ϕ
+  → is-anodyne-for-shape (J × I)
+    ( \ (t , s) → χ t ∧ ψ s)
+    ( \ (t , s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+  :=
+    \ f A' A α is-orth₀ →
+    ( 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)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  : is-anodyne-for-shape I ψ ϕ
+  → is-anodyne-for-shape (I × J)
+    ( \ (s , t) → ψ s ∧ χ t)
+    ( \ (s , t) → (ϕ s ∧ χ t) ∨ (ψ s ∧ ζ t))
+  :=
+    \ f A' A α is-orth₀ →
+    ( is-right-orthogonal-to-shape-pushout-product' A' A α I ψ ϕ J χ ζ
+      ( f A' A α is-orth₀))
+```
+
+### Weak anodyne shape inclusions
+
+Instead of an implication with respect to right orthogonality, we ask for a mere
+implication with respect to types with unique extensions.
+
+```rzk
+#def is-weak-anodyne-for-shape
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  : U
+  :=
+    ( (A : U)
+    → has-unique-extensions I₀ ψ₀ ϕ₀ A
+    → has-unique-extensions I ψ ϕ A)
+```
+
+Every anodyne shape inclusion is weak anodyne.
+
+```rzk
+#def is-weak-anodyne-is-anodyne-for-shape uses (weakextext)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  : is-anodyne-for-shape I ψ ϕ
+  → is-weak-anodyne-for-shape I ψ ϕ
+  :=
+    \ f A has-ue₀ →
+    ( has-unique-extensions-is-right-orthogonal-terminal-map I ψ ϕ A
+      ( f A Unit (terminal-map A)
+        ( is-right-orthogonal-terminal-map-has-unique-extensions I₀ ψ₀ ϕ₀ A
+          has-ue₀)))
+```
+
+The inference rules that we saw above for anodyne shape inclusions all have an
+analog fo weak anodyne shape inclusions.
+
+```rzk
+-- add them as you use them
+
+#def is-weak-anodyne-for-self
+  : is-weak-anodyne-for-shape I₀ ψ₀ ϕ₀
+  := \ _ has-ue₀ → has-ue₀
+
+#def implication-has-unique-extension-implication-right-orthogonal
+  uses (weakextext)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  ( impl
+    : (A' : U) → (A : U) → (α : A' → A)
+    → is-right-orthogonal-to-shape I ψ ϕ A' A α
+    → is-right-orthogonal-to-shape J χ ζ A' A α)
+  ( A : U)
+  : has-unique-extensions I ψ ϕ A
+  → has-unique-extensions J χ ζ A
+  :=
+    \ has-ue-ψ-ϕ →
+    has-unique-extensions-is-right-orthogonal-terminal-map J χ ζ A
+    ( impl A Unit (terminal-map A)
+      ( is-right-orthogonal-terminal-map-has-unique-extensions I ψ ϕ A
+        has-ue-ψ-ϕ))
+
+#def is-weak-anodyne-pushout-product-for-shape
+  uses (naiveextext weakextext)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  : is-weak-anodyne-for-shape I ψ ϕ
+  → is-weak-anodyne-for-shape (J × I)
+    ( \ (t , s) → χ t ∧ ψ s)
+    ( \ (t , s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+
+  :=
+    \ f A has-ue₀ →
+    implication-has-unique-extension-implication-right-orthogonal I ψ ϕ
+    ( J × I) ( \ (t , s) → χ t ∧ ψ s) ( \ (t , s) → (ζ t ∧ ψ s) ∨ (χ t ∧ ϕ s))
+    ( \ A'₁ A₁ α₁ →
+      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)
+  ( I : CUBE)
+  ( ψ : I → TOPE )
+  ( ϕ : ψ → TOPE )
+  ( J : CUBE)
+  ( χ : J → TOPE)
+  ( ζ : χ → TOPE)
+  : is-weak-anodyne-for-shape I ψ ϕ
+  → is-weak-anodyne-for-shape (I × J)
+    ( \ (s , t) → ψ s ∧ χ t)
+    ( \ (s , t) → (ϕ s ∧ χ t) ∨ (ψ s ∧ ζ t))
+  :=
+    \ f A has-ue₀ →
+    implication-has-unique-extension-implication-right-orthogonal I ψ ϕ
+    ( I × J) ( \ (s , t) → ψ s ∧ χ t) ( \ (s , t) → (ϕ s ∧ χ t) ∨ (ψ s ∧ ζ t))
+    ( \ A'₁ A₁ α₁ →
+      is-right-orthogonal-to-shape-pushout-product' A'₁ A₁ α₁ I ψ ϕ J χ ζ)
+    ( A) (f A has-ue₀)
+
+#end anodyne
+```