  Simplicial type theory extends homotopy type theory with a directed path type
which internalizes the notion of a homomorphism within a type. This concept has
significant applications both within mathematics -- where it allows for
synthetic (higher) category theory -- and programming languages -- where it
leads to a directed version of the structure identity principle. In this work,
we construct the first types in simplicial type theory with non-trivial
homomorphisms. We extend simplicial type theory with modalities and new
reasoning principles to obtain triangulated type theory in order to construct
the universe of discrete types $\mathcal{S}$. We prove that homomorphisms in
this type correspond to ordinary functions of types i.e., that $\mathcal{S}$ is
directed univalent. The construction of $\mathcal{S}$ is foundational for both
of the aforementioned applications of simplicial type theory. We are able to
define several crucial examples of categories and to recover important results
from category theory. Using $\mathcal{S}$, we are also able to define various
types whose usage is guaranteed to be functorial. These provide the first
complete examples of the proposed directed structure identity principle.
