  We present an extensive mechanization of the meta-theory of Martin-L\"of Type
Theory (MLTT) in the Coq proof assistant. Our development builds on
pre-existing work in Agda to show not only the decidability of conversion, but
also the decidability of type checking, using an approach guided by
bidirectional type checking. From our proof of decidability, we obtain a
certified and executable type checker for a full-fledged version of MLTT with
support for $\Pi$, $\Sigma$, $\mathbb{N}$, and identity types, and one
universe. Furthermore, our development does not rely on impredicativity,
induction-recursion or any axiom beyond MLTT with a schema for indexed
inductive types and a handful of predicative universes, narrowing the gap
between the object theory and the meta-theory to a mere difference in
universes. Finally, we explain our formalization choices, geared towards a
modular development relying on Coq's features, e.g. meta-programming facilities
provided by tactics and universe polymorphism.
