nLab simplicial type theory

Idea

Simplicial type theory is a cohesive homotopy type theory which is used to represent the internal logic of cohesive locally cartesian closed $(\infty,1)$-categories of simplicial objects in a locally cartesian closed $(\infty,1)$-category. One can think of simplicial type theory as a synthetic theory of simplicial anima, since the cohesive (infinity,1)-topos $\mathrm{Ani}^{\Delta^\op}$ of simplicial anima is the characteristic example of a cohesive locally cartesian closed $(\infty,1)$-category of simplicial objects in a locally cartesian closed $(\infty,1)$-category.

Simplicial type theory is used to construct various geometric shapes internally, such as Segal types (i.e. Segal space-types), Rezk types (i.e. Rezk category-types), and covariant fibrations.

Definition

Simplicial type theory is a cohesive homotopy type theory: that is, a modal type theory with a sharp modality, flat modality, and shape modality adjoint triple

$$\esh \dashv \flat \dashv \sharp$$

• The shape modality $\esh A$ represents localization at the simplicial interval $L_\mathbb{I}(A)$ for simplicial anima.

• The flat modality $\flat A$ represents the global sections (infinity,1)-functor which takes a simplicial anima and returns its core discrete anima.

• The sharp modality $\sharp A$ represents the complete graph (infinity,1)-functor which takes a simplicial anima and returns its codiscrete anima, which has the same objects as $A$ but where every hom-type in $\sharp A$ is contractible. This is a higher inductive-inductive type that is generated by a type $\sharp A$, a function $A \to \sharp A$, and a type family $(\mathrm{hom}_{\sharp A}(x, y))_{(x:\sharp A, y:\sharp A)}$ such that each $\mathrm{hom}_{\sharp A}(x, y)$ is equivalent to the cone type $\mathrm{Cone}(\mathrm{hom}_{A}(x, y))$.

There are also two other modalities

• the op modality $A^\op$ which reverses all (higher) morphisms in a type. This modality is an involution on types (i.e. $(A^\op)^\op \simeq A)$), and types have the same core as its opposite $\flat A^\op \simeq \flat A$. The op modality represents the opposite simplicial anima (infinity,1)-functor.

• the twisted arrow modality $A^\mathrm{tw}$ which represents the twisted arrow construction (infinity,1)-functor in simplicial anima.

In addition, simplicial type theory comes with a designated bounded total order $\mathbb{I}$ called a directed interval, such that

• there is an equivalence of types $\neg:\mathbb{I}^op \simeq \mathbb{I}$ which swaps $0$ for $1$ and $\max$ for $\min$,

• the booleans are the global points of $\mathbb{I}$: i.e. the unique endpoints-preserving monotonic function from the boolean domain $\mathbb{2}$ to $\mathbb{I}$ is an embedding of types and the unique endpoints-preserving monotonic function from $\mathbb{2}$ to $\flat \mathbb{I}$ is an equivalence of types,

• the axiom of simplicial cohesion: for all crisp types $A$, the $\flat$-counit $\flat(-):\flat A \to A$ is an equivalence of types if and only if the function $\mathrm{const}_{A, \mathbb{I}}$ which takes elements of $A$ to constant functions $\mathbb{I} \to A$ is an equivalence of types.

• the interval exhibits the cohesion of types: the shape modality is equivalent to localization at $\mathbb{I}$, $\esh A \simeq L_\mathbb{I}(A)$,

• $n$-cubes detect continuity: for every crisp function $f::A \to B$, $f$ is $\sharp$-modal if and only if it lifts up against the $\flat$-counit $\flat(-):\flat(\mathrm{Fin}(n) \to \mathbb{I}) \to (\mathrm{Fin}(n) \to \mathbb{I})$ for all crisp natural numbers $n::\mathbb{N}$, where $\mathrm{Fin}(n) \coloneqq \sum_{i:\mathbb{N}} i \lt n$ is the crisp standard finite set with $n$ elements.

• $\mathbb{I}$ is tiny: the heterogeneous path space modality $\prod_{i:\mathbb{I}} (-)(i)$ has an amazing right adjoint $(-)^{1/\mathbb{I}}$.

• a Kock-Lawvere-esque duality axiom: let $A$ be a finitely presented $\mathbb{I}$-algebra, in the sense that $A$ is a distributive lattice equivalent to the quotient of $\mathbb{I}[x_1 \ldots x_n]$ by finitely many relations, and let $\mathrm{hom}_{\mathbb{I}\mathrm{Alg}}(A, \mathbb{I})$ be the type of $\mathbb{I}$-algebra homomorphisms. Then the following function is an equivalence of types

$$\lambda a.\lambda f.f(a):A \to (\mathrm{hom}_{\mathbb{I}\mathrm{Alg}}(A, \mathbb{I}) \to \mathbb{I})$$

Formalising the bounded total order

There are many different ways to formalize the bounded total order in simplicial type theory:

• one could simply postulate in vanilla dependent type theory via inference rules and axioms a bounded total order, as in Gratzer, Weinberger, & Buchholtz 2024 and Gratzer, Weinberger, & Buchholtz 2025.

• one could use two-level type theory consisting of a non-fibrant layer, and then axiomatise a bounded total order 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 bounded total order using the cube and tope layers, as in Riehl & Shulman 2017.

The first approach is simpler to define, while the latter two are easier to work with, since the equalities in the interval type are judgmental equalities rather than identifications, so one doesn’t have to deal with transport hell.

In the latter two approaches, the function type $\mathbb{I} \to A$ used in the axiom of cohesion is usually defined as an extension type, while the dependent function type $\prod_{i:\mathbb{I}} A(i)$ is usually defined as a dependent extension type.

Simplicial anima theory and $(\infty,1)$-category theory

Morphisms

The morphisms between elements $x:A$ and $y:A$ in a type $A$ are defined in simplicial type theory as a tuple consisting of a function $f:\mathbb{I} \to A$ and two identifications $p_0:f(0) = x$ and $p_1:f(1) = y$. The type of morphisms is called a hom-type and is defined as the dependent sum type

$$\mathrm{hom}_A(x, y) \coloneqq \sum_{f:\mathbb{I} \to A} (f(0) = x) \times (f(1) = y)$$

Given an element $x:A$, the hom-type $\mathrm{hom}_A(x, x)$ has an identity morphism given by the tuple consisting of the constant function from $\mathbb{I}$ to $A$ at $x$ and two witnesses that $f(0) = x$ and $f(1) = x$ both derivable from the typal computation rules for function types.

$$\mathrm{id}_A(x) \coloneqq (\lambda t.x, \beta_{\mathbb{I} \to A}^{t.x}(0), \beta_{\mathbb{I} \to A}^{t.x}(1)):\mathrm{hom}_A(x, x)$$

Given a type $A$, the hom-types of $\sharp A$ are contractible for all $x:\sharp A$ and $y:\sharp A$:

$$\prod_{x:\sharp A} \prod_{y:\sharp A} \mathrm{isContr}(\mathrm{hom}_{\sharp A}(x, y))$$

Functors

Given two types $A$ and $B$, every function $f:A \to B$ induces a function

$$f_{x, y}:\mathrm{hom}_A(x, y) \to \mathrm{hom}_B(f(x), f(y))$$

by postcomposition which takes a function $h:\mathbb{I} \to A$ to $f \circ h:\mathbb{I} \to B$ and by the action on identifications which take identifications $p_0:h(0) = x$ to $\mathrm{ap}_f(p_0):f(h(0)) = f(x)$ and $p_1:h(1) = x$ to $\mathrm{ap}_f(p_1):f(h(1)) = f(y)$.

As a result, functions can also be called functors. A contravariant functor $F$ from type $A$ to type $B$ is a function $F:A^\op \to B$ from the opposite type of $A$ to $B$.

Diagrams

Diagrams in simplicial type theory can be defined in an arbitrary type, rather than just the Segal types. Diagrams include:

• pair of composable morphisms

• composite of morphisms

• span in simplicial type theory

• cospan in simplicial type theory

• isomorphism in simplicial type theory

Limits and colimits

Limits and colimits in simplicial type theory can be defined in an arbitrary type, rather than just the Segal types.

Limits include:

• terminal object in simplicial type theory

• (infinity,1)-product

• (infinity,1)-equalizer

• (infinity,1)-pullback

Colimits include:

• initial object in simplicial type theory

• (infinity,1)-coproduct

• (infinity,1)-coequalizer

• (infinity,1)-pushout

Types

Types include

• simplicially discrete type

• Segal type

• univalent type

• Rezk type

• skeletal type

• gaunt type

• finitely complete type

• finitely cocomplete type

Heterogeneous morphisms and covariant type families

Given a type $A$, elements $x:A$ and $y:A$, a function $f:\mathbb{I} \to A$, identifications $p_0:f(0) =_A x$ and $p_1:f(1) =_A y$ a type family $x:A \vdash B(x)$, and elements $u:B(x)$ and $v:B(y)$, a heterogeneous morphism is a tuple consisting of a dependent function $g:\prod_{i:\mathbb{I}} B(f(i))$ and two indexed heterogeneous identifications

$$q_0:g(0) =_{t.B(t)}^{(f(0), x, p_0)} u \; \mathrm{and} \; q_1:g(1) =_{t.B(t)}^{(f(1), y, p_1)} v$$

where the type $u =_{t.B(t)}^{(x, y, p)} v$ is the indexed heterogeneous identity type over the type family $x:A \vdash B(x)$.

The type of heterogeneous morphisms is called the heterogeneous hom-type and is defined as the dependent sum type

$$\mathrm{hhom}_{t.B(t)}(x, y, f, p_0, p_1, u, v) \coloneqq \sum_{g:\prod_{i:\mathbb{I}} B(f(i))} (g(0) =_{t.B(t)}^{(f(0), x, p_0)} u) \times (g(1) =_{t.B(t)}^{(f(1), y, p_1)} v)$$

A covariant type family is a type family $x:A \vdash B(x)$ such that for all elements $x:A$, $y:A$, $f:\mathrm{hom}_A(x, y)$, and $u:B(x)$, there exists a unique element $v:B(y)$ with a heterogeneous morphism

$$\mathrm{isCovariant}(t:A.B(t)) \coloneqq \prod_{x:A} \prod_{y:A} \prod_{f:\mathrm{hom}_A(x, y)} \prod_{u:B(x)} \exists!v:B(y).\mathrm{hhom}_{t.B(t)}(x, y, f, p_0, p_1, u, v)$$

Amazing covariance and directed univalent universes

A type $A$ is an amazingly covariant type if it satisfies the following predicate

$$\mathrm{isACov}(A) \coloneqq \mathrm{isCov}(i:\mathbb{I}.A^\eta \cdot i)^{1 / \mathbb{I}}$$

Let $(U, T)$ be a univalent Tarski universe. The directed univalent subuniverse $\mathcal{S} \hookrightarrow U$ is defined as the type of $U$-small amazingly covariant types:

$$\mathcal{S} \coloneqq \sum_{X:U} \mathrm{isACov}(T(X))$$

The directed univalent universe $\mathcal{S}$ is a finitely complete and finitely cocomplete Rezk type.

See also

• Reedy model structure

• bisimplicial set

• simplicial anima

• simplicial object in an (infinity,1)-category

• synthetic $(\infty,1)$-category theory

• parametric type theory

• cohesive homotopy type theory

• triangulated type theory

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 $(\infty,1)$-Category Theory: Fibrational and Semantic Aspects $[$arXiv:2202.13132$]$

• Fredrik Bakke, Segal Spaces in Homotopy Type Theory. Master thesis $[$no.ntnu:inspera:99217069:14871483$]$

• César Bardomiano Martínez, Limits and colimits of synthetic $\infty$-categories $[$arXiv:2202.12386$]$

• Jonathan Weinberger, Strict stability of extension types $[$arXiv:2203.07194$]$

• Jonathan Weinberger, Two-sided cartesian fibrations of synthetic $(\infty,1)$-categories $[$arXiv:2204.00938$]$

• Jonathan Weinberger, Internal sums for synthetic fibered $(\infty,1)$-categories $[$arXiv:2205.00386$]$

• David Jaz Myers, Mitchell Riley, Commuting Cohesions [arXiv:2301.13780]

• Mitchell Riley, A Type Theory with a Tiny Object [arXiv:2403.01939]

• Jonathan Weinberger, Generalized Chevalley criteria in simplicial homotopy type theory, arXiv:2403.08190

• C.B. Aberlé, Parametricity via Cohesion [arXiv:2404.03825]

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, The Yoneda embedding in simplicial type theory (arXiv:2501.13229)

A talk on synthetic (infinity,1)-category theory in simplicial type theory and infinity-cosmos theory:

• Emily Riehl, The synthetic theory of infinity-categories vs the synthetic theory of infinity-categories, Homotopy Type Theory Electronic Seminar Talks, 1 March 2018, (video, slides)

A proof assistant implementing simplicial type theory:

• Rzk[github.com/fizruk/rzk]

Formalization of the $(\infty,1)$-Yoneda lemma via simplicial homotopy type theory (in Rzk):

• Nikolai Kudasov, Emily Riehl, Jonathan Weinberger. Formalizing the $\infty$-categorical Yoneda lemma (2023) [arXiv:2309.08340]