Are definitional and propositional extenionality on top of intensional type theory equivalent?

Question

I am reading the article about extensional type theory on n-lab and it mentions two ways to make intensional type theory extensional.

1. Definitional: Add rule p:Id(x,y) => x===y
2. Propositional: Add one of the following to the type theory
   • axiom UIP
   • axiom K
   • axiom stating Id((a,b_1),(a,b_2)) => Id(b_1,b_2) where (a,b_1) and (a,b_2) are both dependent pairs
   • add unconstrained pattern matching as in original Agda

My question is are these two ways equivalent?

Specifically, if so, can one derive p:Id(x,y) => x===y from axiom K or UIP?

Answer 1

The n-lab take on what it means for a type theory to be extensional is fairly peculiar. It makes sense though if you are mostly interested in whether the Id type can be extended with univalence, which is not the case if you have UIP.

(1) does imply (2) (using the numbers from the question), so it's not consistent with univalence.

(1) is the rule that more traditional sources would associate with the name "extensional type theory".

However (2) does not imply (1), as canonicity for the Id type for a theory like Agda would show that any proof of Id in an empty context is reflexivity, while (1) implies function extensionality.