Displayed type theory and 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 of semi-simplicial types. Roughly speaking, a semi-simplicial type consists of a type together with, for each , a displayed semi-simplicial type over . 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 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.