  We prove a conservativity result for extensional type theories over
propositional ones, i.e. dependent type theories with propositional computation
rules, using insights from homotopy type theory. The argument exploits a notion
of canonical homotopy equivalence between contexts, and uses the notion of a
type-category to phrase the semantics of theories of dependent types.
Informally, our main result asserts that, for judgements essentially concerning
h-sets, reasoning with extensional or propositional type theories is
equivalent.
