nLab
simplicial type theory
Redirected from "simplicial homotopy type theory".
Contents
Context
Directed Type Theory
Contents
Idea
Simplicial type theory (Riehl & Shulman 2017, §3 ) is a homotopy type theory which introduces additional non-fibrant layers on top of Martin-Löf type theory to provide a logical calculus for a directed interval type and with it for geometric shapes , consisting of Segal space -types, Rezk complete -types, and covariant fibrations.
There are many different ways to formalize the directed interval primitive in simplicial type theory:
one could simply postulate via inference rules and axioms a directed interval primitive in a separate layer.
one could use two-level type theory consisting of a non-fibrant layer, and then axiomatise a directed interval primitive in the non-fibrant layer
one could use type theory with shapes consisting of a non-fibrant layer of cubes which is a simple type theory and a non-fibrant layer of topes which is a propositional logic over the cube layer, and then define the directed interval primitive using the cube and tope layers
Two-level type theory
We use Ξ \Xi to represent the context in the non-fibrant layer, and Γ \Gamma to represent the context in the fibrant layer. Type judgments in the non-fibrant layer are represented by A exotype A \; \mathrm{exotype} , while type judgments in the fibrant layer are just represented by A type A \; \mathrm{type} .
Directed interval primitive
The directed interval primitive 𝟚 \mathbb{2} in simplicial type theory is a non-trivial bounded total order . Bounded total orders have many definitions in mathematics, such as a bounded partial order satisfying totality, or a lattice satisfying totality. As such, there are multiple possible sets of inference rules one could use to present the directed interval in the two-level type theory formalization.
The inference rules for the directed interval primitive ( 𝟚 , ≤ ) (\mathbb{2}, \leq) as a partial order in the two-level type theory formalization are as follows:
Ξ ctx Ξ ⊢ 𝟚 exotype Ξ ctx Ξ ⊢ 0 : 𝟚 Ξ ctx Ξ ⊢ 1 : 𝟚 Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ x ≤ y exotype Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ τ ≤ ( x , y ) : isProp ( x ≤ y ) \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash \mathbb{2} \; \mathrm{exotype}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash 0:\mathbb{2}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash 1:\mathbb{2}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash x \leq y \; \mathrm{exotype}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \tau_\leq(x, y):\mathrm{isProp}(x \leq y)} Ξ ctx Ξ , x : 𝟚 ⊢ refl ≤ ( x ) : x ≤ x Ξ ctx Ξ , x : 𝟚 , y : 𝟚 , z : 𝟚 , p : x ≤ y , q : y ≤ z ⊢ trans ≤ ( x , y , z , p , q ) : ( x ≤ z ) \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{refl}_\leq(x):x \leq x} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2}, z:\mathbb{2}, p:x \leq y, q:y \leq z \vdash \mathrm{trans}_\leq(x, y, z, p, q):(x \leq z)} Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ antisym ≤ ( x , y ) : isEquiv ( idtoleqgeq ( x , y ) ) where idtoleqgeq ( x , y ) : ( x = 𝟚 y ) → ( x ≤ y ) × ( y ≤ x ) idtoleqgeq ( x , x ) ( id 𝟚 ( x ) ) ≔ ( refl ≤ ( x ) , refl ≤ ( x ) ) \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{antisym}_\leq(x, y):\mathrm{isEquiv}(idtoleqgeq(x, y))} \quad \mathrm{where} \quad
\begin{array}{l}
idtoleqgeq(x, y):(x =_\mathbb{2} y) \to (x \leq y) \times (y \leq x) \\
idtoleqgeq(x, x)(\mathrm{id}_\mathbb{2}(x)) \coloneqq (\mathrm{refl}_\leq(x), \mathrm{refl}_\leq(x))
\end{array}
Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ totl ≤ ( x , y ) : [ ( x ≤ y ) + ( y ≤ x ) ] Ξ ctx Ξ , x : 𝟚 ⊢ bot ≤ ( x ) : 0 ≤ x Ξ ctx Ξ , x : 𝟚 ⊢ top ≤ ( x ) : x ≤ 1 \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{totl}_\leq(x, y):[(x \leq y) + (y \leq x)]} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{bot}_\leq(x):0 \leq x} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{top}_\leq(x):x \leq 1} Ξ ctx Ξ ⊢ nontriv ≤ : ( 0 = 𝟚 1 ) → 𝟘 \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash \mathrm{nontriv}_\leq:(0 =_\mathbb{2} 1) \to \mathbb{0}}
The inference rules for the directed interval primitive 𝟚 \mathbb{2} as a lattice in the two-level type theory formalization are as follows:
Ξ ctx Ξ ⊢ 𝟚 exotype Ξ ctx Ξ ⊢ τ 0 : isSet ( 𝟚 ) Ξ ctx Ξ ⊢ 0 : 𝟚 Ξ ctx Ξ ⊢ 1 : 𝟚 Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ x ∧ y : 𝟚 Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ x ∨ y : 𝟚 \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash \mathbb{2} \; \mathrm{exotype}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash \tau_0:\mathrm{isSet}(\mathbb{2})} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash 0:\mathbb{2}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash 1:\mathbb{2}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash x \wedge y:\mathbb{2}} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash x \vee y:\mathbb{2}} Ξ ctx Ξ , x : 𝟚 ⊢ idem ∧ ( x ) : x ∧ x = 𝟚 x Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ comm ∧ ( x , y ) : x ∧ y = 𝟚 y ∧ x \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{idem}_\wedge(x):x \wedge x =_{\mathbb{2}} x} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{comm}_\wedge(x, y):x \wedge y =_{\mathbb{2}} y \wedge x} Ξ ctx Ξ , x : 𝟚 , y : 𝟚 , z : 𝟚 ⊢ assoc ∧ ( x , y , z ) : ( x ∧ y ) ∧ z = 𝟚 x ∧ ( y ∧ z ) \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2}, z:\mathbb{2} \vdash \mathrm{assoc}_\wedge(x, y, z):(x \wedge y) \wedge z =_{\mathbb{2}} x \wedge (y \wedge z)} Ξ ctx Ξ , x : 𝟚 ⊢ lunit ∧ ( x ) : 1 ∧ x = 𝟚 x Ξ ctx Ξ , x : 𝟚 ⊢ runit ∧ ( x ) : x ∧ 1 = 𝟚 x \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{lunit}_\wedge(x):1 \wedge x =_{\mathbb{2}} x} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{runit}_\wedge(x):x \wedge 1 =_{\mathbb{2}} x} Ξ ctx Ξ , x : 𝟚 ⊢ idem ∨ ( x ) : x ∨ x = 𝟚 x Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ comm ∨ ( x , y ) : x ∨ y = 𝟚 y ∨ x \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{idem}_\vee(x):x \vee x =_{\mathbb{2}} x} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{comm}_\vee(x, y):x \vee y =_{\mathbb{2}} y \vee x} Ξ ctx Ξ , x : 𝟚 , y : 𝟚 , z : 𝟚 ⊢ assoc ∨ ( x , y , z ) : ( x ∨ y ) ∨ z = 𝟚 x ∨ ( y ∨ z ) \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2}, z:\mathbb{2} \vdash \mathrm{assoc}_\vee(x, y, z):(x \vee y) \vee z =_{\mathbb{2}} x \vee (y \vee z)} Ξ ctx Ξ , x : 𝟚 ⊢ lunit ∨ ( x ) : 0 ∨ x = 𝟚 x Ξ ctx Ξ , x : 𝟚 ⊢ runit ∨ ( x ) : x ∨ 0 = 𝟚 x \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{lunit}_\vee(x):0 \vee x =_{\mathbb{2}} x} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2} \vdash \mathrm{runit}_\vee(x):x \vee 0 =_{\mathbb{2}} x} Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ asorp ∧ ( x , y ) : x ∧ ( x ∨ y ) = 𝟚 x Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ asorp ∨ ( x , y ) : x ∨ ( x ∧ y ) = 𝟚 x \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{asorp}_\wedge(x, y):x \wedge (x \vee y) =_{\mathbb{2}} x} \qquad \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{asorp}_\vee(x, y):x \vee (x \wedge y) =_{\mathbb{2}} x} Ξ ctx Ξ , x : 𝟚 , y : 𝟚 ⊢ totl ( x , y ) : [ ( x ∧ y = 𝟚 x ) + ( x ∧ y = 𝟚 y ) ] Ξ ctx Ξ ⊢ nontriv ≤ : ( 0 = 𝟚 1 ) → 𝟘 \frac{\Xi \; \mathrm{ctx}}{\Xi, x:\mathbb{2}, y:\mathbb{2} \vdash \mathrm{totl}(x, y):[(x \wedge y =_{\mathbb{2}} x) + (x \wedge y =_{\mathbb{2}} y)]} \quad \frac{\Xi \; \mathrm{ctx}}{\Xi \vdash \mathrm{nontriv}_\leq:(0 =_\mathbb{2} 1) \to \mathbb{0}}
Simplices and subshapes
We inductively define the n n -simplices as the following family of non-fibrant types:
The 0 0 -simplex is the unit type in the non-fibrant layer
Δ 0 ≔ 1 \Delta^0 \coloneqq \mathbf{1}
In the non-fibrant layer, let Fin ( n ) ≔ ∑ i : ℕ i < n \mathrm{Fin}(n) \coloneqq \sum_{i:\mathbb{N}} i \lt n be the canonical finite type with n n elements. The n + 1 n+1 -simplex is defined as the type
n : ℕ ⊢ Δ n + 1 ≔ ∑ t : Fin ( n + 1 ) → 𝟚 ∏ i : Fin ( n ) t ( π 1 ( i + 1 ) ) ≤ t ( π 1 ( i ) ) n:\mathbb{N} \vdash \Delta^{n + 1} \coloneqq \sum_{t:\mathrm{Fin}(n + 1) \to \mathbb{2}} \prod_{i:\mathrm{Fin}(n)} t(\pi_1(i + 1)) \leq t(\pi_1(i))
The first few simplicies can be explicitly written as
Δ 1 ≔ 𝟚 \Delta^1 \coloneqq \mathbb{2} Δ 2 ≔ ∑ t : Fin ( 2 ) → 𝟚 t ( 1 ) ≤ t ( 0 ) \Delta^2 \coloneqq \sum_{t:\mathrm{Fin}(2) \to \mathbb{2}} t(1) \leq t(0) Δ 3 ≔ ∑ t : Fin ( 3 ) → 𝟚 ( t ( 2 ) ≤ t ( 1 ) ) × ( t ( 1 ) ≤ t ( 0 ) ) \Delta^3 \coloneqq \sum_{t:\mathrm{Fin}(3) \to \mathbb{2}} (t(2) \leq t(1)) \times (t(1) \leq t(0))
Subshapes of the simplicies could also be defined.
Type theory with shapes
…
See also
References
Emily Riehl , Mike Shulman , A type theory for synthetic ∞-categories , Higher Structures 1 1 (2017) [arxiv:1705.07442 , published article ]
Jonathan Weinberger , A Synthetic Perspective on ( ∞ , 1 ) (\infty,1) -Category Theory: Fibrational and Semantic Aspects [ [ arXiv:2202.13132 ] ]
Jonathan Weinberger , Strict stability of extension types [ [ arXiv:2203.07194 ] ]
Jonathan Weinberger , Generalized Chevalley criteria in simplicial homotopy type theory , arXiv:2403.08190
A talk on synthetic (infinity,1)-category theory in simplicial type theory and infinity-cosmos theory:
A proof assistant implementing simplicial type theory:
Formalization of the
(
∞
,
1
)
(\infty,1)
-Yoneda lemma via simplicial homotopy type theory (in Rzk ):
Last revised on March 14, 2024 at 04:40:53.
See the history of this page for a list of all contributions to it.