Propositional vs Definitional extentionality in type theory

Question

There are essentially two ways to impose extentionality on a type theory (I know, it is not very fashionable to impose extentionality these days, but please, bear with me) you can either have a "propositional extentionality axiom" like UIP (uniqueness of identity proof) which says that every two inhabitant of Id(x,y) are propositionally equals, or a "reflexion rules" which says that if you have an inhabitant $a:Id(x,y)$ then $x=y$ and $a=r(x)$. (and if you do it for all types you might not even it to ask that $a=r(x)$)

One expect that the two are equivalent in some precise sens: clearly the reflexion principle implies UIP, so if you can prove something using UIP you can also prove it using the reflection principle, but the converse is a bit harder and one only expect that if we are able to proves that x=y using the reflection principle then one can prove that there is an inhabitant of Id(x,y) using UIP.

I assume it can be formalized by somehow quotienting types & terms using the equivalence relation defined by $\exists v \in Id(x,y)$ but I would be interested to see it done concretely.

So I would be interested by any references making some cases of this into rigorous theorem (for various kind of type theory). If it exists I'm also interested in situation where you only impose UIP/Reflection on some types and not on all types.

(and I don't really care about the specific form of the axioms used to impose extentionality other than the distinction between definitional and propositional)

Answer 1

Martin Hofmann proves in his thesis (theorem 3.2.5) that whenever we have a type $\Gamma \vdash A$ in intensional type theory (ITT) and a term $|\Gamma| \vdash a : |A|$ in ETT there is a term $\Gamma \vdash a' : A$ such that $|\Gamma| \vdash |a'| \equiv a : |A|$. In particular, this implies that whenever some statement is provable in ETT it is also provable in ITT.

This is related to the question that I'm working on, so let me discuss it if you don't mind. Hofmann's theorem implies that ITT and ETT are equivalent in some precise sense. We can define a notion of weak equivalences between type theories (of course, we need to define a category of type theories first) either as a map with some syntactic properties similar to the one described above or as a map that induces (Quillen) equivalence of categories of models (these definitions are equivalent). There are many natural examples of weak equivalences between type theories. This is a work in progress and will be a part of my thesis.