## Definition ## A simplicial type is a type family $X:\Delta^\op \to \mathcal{U}$ from the [[opposite category]] of the [[simplex category]] to the universe $\mathcal{U}$. The type of simplicial types in a [[universe]] provide an internal model of [[cohesive homotopy type theory]]. ## See also ## * [[simplex category]] * [[cohesive homotopy type theory]]