wip

Author: 5HT

doc/anders.tex

@@ -17,7 +17,7 @@
 \end{CCSXML}
 
 \ccsdesc[300]{Theory of computation~Lambda calculus}
-\keywords{Homotopy Type Theory, Differential Geometry, Modal Type Theory, Cohesive Type Theory}
+\keywords{Homotopy Type Theory, Differential Geometry, Cohesive Type Theory, Simplicial Type Theory}
 
 \nolinenumbers
 \hideLIPIcs

library/foundations/modal/stt.anders

@@ -1,27 +1,30 @@
--- Simplicial Type Theory (STT) Core Verification
+--- Simplicial Type Theory (STT) Core Verification
 
 import library/foundations/modal/flat
 import library/foundations/modal/sharp
 import library/foundations/modal/twisted
 
--- Modal Pi Types (Π (x :_μ A), B)
--- tracked via modal annotations μ ∈ {id, ♭, ♯, tw, ...}
+--- Modal Pi Types (Π (x :_μ A), B)
+--- tracked via modal annotations μ ∈ {id, ♭, ♯, tw, ...}
 
--- Reality Check: Huber Equations (Transport) for Modal Pi
--- transpⁱ (Π (x :_μ A), B) φ u₀ v = transpⁱ B[x/w] φ (u₀ w(i/0))
-def trans-ModalPi-is-correct (A : I -> U) (B : (i : I) -> A i -> U) (phi : I) (u0 : (x :_♭ A 0) -> B 0 x) :
-  Path ((x :_♭ A 1) -> B 1 x) (transp (<i> (x :_♭ A i) -> B i x) phi u0)
-       (\(v : A 1) -> transp (<i> B i (tFill A phi v i)) phi (u0 (tFill A phi v 0)))
+--- Reality Check: Huber Equations (Transport) for Modal Pi
+--- transpⁱ (Π (x :_μ A), B) φ u₀ v = transpⁱ B[x/w] φ (u₀ w(i/0))
+def trans-ModalPi-is-correct (A : I -> U) (B : (i : I) -> A i -> U)
+    (phi : I) (u0 : (x :_♭ A 0) -> B 0 x)
+  : Path ((x :_♭ A 1) -> B 1 x) (transp (<i> (x :_♭ A i) -> B i x) phi u0)
+          (\(v : A 1) -> transp (<i> B i (tFill A phi v i)) phi (u0 (tFill A phi v 0)))
   := refl ((x :_♭ A 1) -> B 1 x) (\(v : A 1) -> transp (<i> B i (tFill A phi v i)) phi (u0 (tFill A phi v 0)))
 
--- Reality Check: Huber Equations (Composition) for Modal Pi
--- hcompⁱ (Π (x :_μ A), B) [φ ↦ u] u₀ v = hcompⁱ B[x/v] [φ ↦ u v] (u₀ v)
-def hcomp-ModalPi-is-correct (A : U) (B : A -> U) (phi : I) (u : I -> (x :_♭ A) -> B x) (u0 : (x :_♭ A) -> B x) :
-  Path ((x :_♭ A) -> B x) (hcomp (<i> (x :_♭ A) -> B x) [ (phi=1) -> <i> u i ] u0)
-       (\(v : A) -> hcomp (<i> B v) [ (phi=1) -> <i> u i v ] (u0 v))
-  := refl ((x :_♭ A) -> B x) (\(v : A) -> hcomp (<i> B v) [ (phi=1) -> <i> u i v ] (u0 v))
+--- Reality Check: Huber Equations (Composition) for Modal Pi
+--- hcompⁱ (Π (x :_μ A), B) [φ ↦ u] u₀ v = hcompⁱ B[x/v] [φ ↦ u v] (u₀ v)
+def hcomp-ModalPi-is-correct (A : U) (B : A -> U) (phi : I)
+    (u : I -> (x :_♭ A) -> B x) (u0 : (x :_♭ A) -> B x)
+  : Path ((x :_♭ A) -> B x) (hcomp (<i> (x :_♭ A) -> B x) [ (phi=1) -> <i> u i ] u0)
+         (\(v : A) -> hcomp (<i> B v) [ (phi=1) -> <i> u i v ] (u0 v))
+ := refl ((x :_♭ A) -> B x) (\(v : A) -> hcomp (<i> B v) [ (phi=1) -> <i> u i v ] (u0 v))
+
+--- Uniqueness (η-rule) for Modal Pi
+def ModalPi-Eta (A : U) (B : A -> U) (f : (x :_♭ A) -> B x)
+  : Path ((x :_♭ A) -> B x) f (\(x :_♭ A) -> f x)
+ := <p> f
 
--- Uniqueness (η-rule) for Modal Pi
-def ModalPi-Eta (A : U) (B : A -> U) (f : (x :_♭ A) -> B x) :
-  Path ((x :_♭ A) -> B x) f (\(x :_♭ A) -> f x)
-  := <p> f

library/foundations/modal/twisted.anders

@@ -1,21 +1,25 @@
--- Twisted Modality (tw) for Simplicial Type Theory
+--- Twisted Modality (tw) for Simplicial Type Theory
 
--- Definitions
+--- Definitions
 def Twisted (A : U) : U := tw A
 def TwistedUnit (A : U) (a : A) : tw A := tw-unit a
-def TwistedInd (A : U) (C : tw A -> U) (f : (x : A) -> C (tw-unit x)) (z : tw A) : C z := ind-tw A C f z
+def TwistedInd (A : U) (C : tw A -> U) (f : (x : A) -> C (tw-unit x)) (z : tw A) : C z
+ := ind-tw A C f z
 
--- Uniqueness (η-rule)
-def TwistedEta (A : U) (x : tw A) : Path (tw A) x (tw-unit (ind-tw A (\_ -> A) (\a -> a) x)) := <p> x
+--- Uniqueness (η-rule)
+def TwistedEta (A : U) (x : tw A) : Path (tw A) x (tw-unit (ind-tw A (\_ -> A) (\a -> a) x))
+ := <p> x
 
--- Reality Check: Huber Equations (Transport)
--- transpⁱ (tw A) φ (tw-unit a) = tw-unit (transpⁱ A φ a)
+--- Reality Check: Huber Equations (Transport)
+--- transpⁱ (tw A) φ (tw-unit a) = tw-unit (transpⁱ A φ a)
 def trans-tw-is-correct (A : I -> U) (phi : I) (u0 : A 0) :
-  Path (tw (A 1)) (transp (<i> tw (A i)) phi (tw-unit u0)) (tw-unit (transp (<i> A i) phi u0))
-  := refl (tw (A 1)) (tw-unit (transp (<i> A i) phi u0))
+    Path (tw (A 1)) (transp (<i> tw (A i)) phi (tw-unit u0)) (tw-unit (transp (<i> A i) phi u0))
+ := refl (tw (A 1)) (tw-unit (transp (<i> A i) phi u0))
 
--- Reality Check: Huber Equations (Composition)
--- hcompⁱ (tw A) [φ ↦ tw-unit u] (tw-unit u₀) = tw-unit (hcompⁱ A [φ ↦ u] u₀)
+--- Reality Check: Huber Equations (Composition)
+--- hcompⁱ (tw A) [φ ↦ tw-unit u] (tw-unit u₀) = tw-unit (hcompⁱ A [φ ↦ u] u₀)
 def hcomp-tw-is-correct (A : U) (phi : I) (u : I -> A) (u0 : A) :
-  Path (tw A) (hcomp (<i> tw A) [ (phi=1) -> <i> tw-unit (u i) ] (tw-unit u0)) (tw-unit (hcomp (<i> A) [ (phi=1) -> <i> u i ] u0))
-  := refl (tw A) (tw-unit (hcomp (<i> A) [ (phi=1) -> <i> u i ] u0))
+    Path (tw A) (hcomp (<i> tw A) [ (phi=1) -> <i> tw-unit (u i) ] (tw-unit u0))
+                (tw-unit (hcomp (<i> A) [ (phi=1) -> <i> u i ] u0))
+ := refl (tw A) (tw-unit (hcomp (<i> A) [ (phi=1) -> <i> u i ] u0))
+