# Homotopy Type Theory simplicial type > history (Rev #1)

## 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.