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 to represent the context in the non-fibrant layer, and to represent the context in the fibrant layer. Type judgments in the non-fibrant layer are represented by , while type judgments in the fibrant layer are just represented by .
Directed interval primitive
The directed interval primitive 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 as a partial order in the two-level type theory formalization are as follows:
The inference rules for the directed interval primitive as a lattice in the two-level type theory formalization are as follows:
Simplices and subshapes
We inductively define the -simplices as the following family of non-fibrant types:
-
The -simplex is the unit type in the non-fibrant layer
-
In the non-fibrant layer, let be the canonical finite type with elements. The -simplex is defined as the type
The first few simplicies can be explicitly written as
Subshapes of the simplicies could also be defined.
Type theory with shapes
…
See also
References
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 -Yoneda lemma via simplicial homotopy type theory (in Rzk):