Displayed Type Theory and Semi-Simplicial Types

TL;DR

The paper introduces Displayed Type Theory (dTT), a multi-modal homotopy type theory with discrete and simplicial modes, enabling the internal definition and semantic generality of semi-simplicial types.

Contribution

It presents a novel multi-modal type theory with display primitives, allowing the internal construction and semantic interpretation of semi-simplicial types in arbitrary ∞-toposes.

Findings

Defined a coinductive type of semi-simplicial types using display primitives.

Provided a semantic model interpreting the theory in ∞-toposes.

Enabled full semantic and syntactic handling of semi-simplicial types.

Abstract

We introduce Displayed Type Theory (dTT), a multi-modal homotopy type theory with discrete and simplicial modes. In the intended semantics, the discrete mode is interpreted by a model for an arbitrary $\infty$-topos, while the simplicial mode is interpreted by Reedy fibrant augmented semi-simplicial diagrams in that model. This simplicial structure is represented inside the theory by a primitive notion of display or dependency, guarded by modalities, yielding a partially-internal form of unary parametricity. Using the display primitive, we then give a coinductive definition, at the simplicial mode, of a type $\mathsf{SST}$ of semi-simplicial types. Roughly speaking, a semi-simplicial type $X$ consists of a type $X_0$ together with, for each $x:X_0$, a displayed semi-simplicial type over $X$. This mimics how simplices can be generated geometrically through repeated cones, and is made possible by the display primitive at the simplicial mode. The discrete part of $\mathsf{SST}$ then yields the usual infinite indexed definition of semi-simplicial types, both semantically and syntactically. Thus, dTT enables working with semi-simplicial types in full semantic generality.