  We define a notion of equivalence between algebraic dependent type theories
which we call Morita equivalence. This notion has a simple syntactic
description and an equivalent description in terms of models of the theories.
The category of models of a type theory often carries a natural structure of a
model category. If this holds for the categories of models of two theories,
then a map between them is a Morita equivalence if and only if the adjunction
generated by it is a Quillen equivalence.
