  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.
