agda - 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

n-lab 对类型论的外延意义的理解是相当奇特的。Id如果您最感兴趣的是类型是否可以单价扩展，这是有道理的，如果您有 UIP，情况并非如此。

（1）确实暗示了（2）（使用问题中的数字），因此它与单价不一致。

(1) 是更传统的来源与“外延类型理论”这个名称相关联的规则。

然而，(2) 并不意味着 (1)，因为Id像 Agda 这样的理论的类型的规范性表明，Id在空上下文中的任何证明都是自反性，而 (1) 意味着函数可扩展性。