Abstract: We revisit Martin Hofmann's now-classical result on the relationship between extensional and intensional type theories by building on insights from homotopy type theory and leveraging the structure of left semi-model category on the category of models of type theory. Specifically, we demonstrate that extensional type theory (ETT) and intensional type theory (ITT) extended by the axiom of uniqueness of identity proofs (UIP) are equivalent in both a logical and a homotopy-theoretic sense. Whereas Hofmann's original proof was focused on initial, or syntactic, models, our approach generalizes to all cofibrant extensions of the base theories, encompassing types, terms, and propositional equalities. In doing so, this result unifies the verification of the analogue of Hofmann's result for all possible new extensions of intensional type theory at once.