  We study the dependent type theory CaTT, introduced by Finster and Mimram,
which presents the theory of weak $\omega$-categories, following the idea that
type theories can be considered as presentations of generalized algebraic
theories. Our main contribution is a formal proof that the models of this type
theory correspond precisely to weak $\omega$-categories, as defined by
Maltsiniotis, by generalizing a definition proposed by Grothendieck for weak
$\omega$-groupoids: Those are defined as suitable presheaves over a
cat-coherator, which is a category encoding structure expected to be found in
an $\omega$-category. This comparison is established by proving the initiality
conjecture for the type theory CaTT, in a way which suggests the possible
generalization to a nerve theorem for a certain class of dependent type
theories
