2023/11/30 by Astra Kolomatskaia, Kolomatskaia, Astra, Michael Shulman +1 · 1 citation
Mathematics · #Advanced Topics in Algebra #Algebraic structures and combinatorial models #Category Theory (math.CT) #FOS: Mathematics #Homotopy and Cohomology in Algebraic Topology #Logic (math.LO)
paper · pdf · doi:10.48550/arxiv.2311.18781
openalex publication_date 2023/11/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 ∞-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 SST of semi-simplicial types. Roughly speaking, a semi-simplicial type X consists of a type X0 together with, for each x:X0, 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 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.