  We study the coherence and conservativity of extensions of dependent type
theories by additional strict equalities. By considering notions of congruences
and quotients of models of type theory, we reconstruct Hofmann's proof of the
conservativity of Extensional Type Theory over Intensional Type Theory. We
generalize these methods to type theories without the Uniqueness of Identity
Proofs principle, such as variants of Homotopy Type Theory, by introducing a
notion of higher congruence over models of type theory. Our definition of
higher congruence is inspired by Brunerie's type-theoretic definition of weak
$\infty$-groupoid. For a large class of type theories, we reduce the problem of
the conservativity of equational extensions to more tractable acyclicity
conditions.
