代码之家 › 专栏 › 技术社区 › protossor

内涵式理论的定义性和命题性外延是否等价?

homotopy-type-theory type-theory dependent-type agda

0

protossor · 技术社区 · 7 年前

我正在读一篇关于 extensional type theory 在n-lab中,提出了使内涵式理论具有外延性的两种方法。

定义:添加规则 p:Id(x,y) => x===y
命题:在类型理论中添加以下内容之一
- 公理UIP
- 公理K
- 公理陈述 Id((a,b_1),(a,b_2)) => Id(b_1,b_2) 哪里 (a,b_1) 和 (a,b_2) 都是依赖对
- 添加原始AGDA中的无约束模式匹配

我的问题是,这两种方法是否等效?

具体地说,如果是这样,我们可以得出 p:id(x,y)=>x==y 从AXIOM K还是UIP?

1 回复 | 直到 7 年前

1

3

Saizan 7 年前

n-lab接受了类型理论的外延意义,这是相当特殊的。如果你对 Id 类型可以用univalence扩展,如果您有uip,则不是这样。

(1)并不意味着(2)(使用问题中的数字),因此它与宇宙不一致。

(1)是更传统的来源将与名称“扩展类型理论”联系起来的规则。

但是(2)并不意味着(1),作为 身份证件 像阿格达这样的理论的类型可以证明 身份证件 在空上下文中是自反性的,而(1)意味着函数的扩展性。