  We study the conservativity of extensions by additional strict equalities of
dependent type theories (and more general second-order generalized algebraic
theories). The conservativity of Extensional Type Theory over Intensional Type
Theory was proven by Hofmann. Our goal is to generalize such results to type
theories without the Uniqueness of Identity Proofs principles, such as variants
of Homotopy Type Theory.
  For this purpose, we construct what is essentially the infinity-congruence on
the base theory that is freely generated by the considered equations. This
induces a factorization of any equational extension, whose two factors can be
studied independently. We conjecture that the first factor is always an
equivalence when the base theory is well-behaved. We prove that the second
factor is an equivalence when the infinity-congruence is 0-truncated.
