Conservativity of Equality Reflection over Intensional Type Theory
Conservativity of Equality Reflection over Intensional Type Theory
复制标题
内涵型理论的等式反映的保守性
DOI：
10.1007/3-540-61780-9_68
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
M. Hofmann
中科院分区：
文献类型：
--
作者：
M. Hofmann
我们研究了 Martin-Lof 类型理论的内涵和外延表述之间的关系。我们展示了两个在内延表述中无法证明的原则：同一性的唯一性和功能外延性。我们表明，外延类型理论相对于这两个原理所扩展的内涵类型理论是保守的，这意味着只要有意义，就会存在相同的类型。该证明是非建设性的，因为它使用集合论商和代表的选择。
We investigate the relationship between intensional and extensional formulations of Martin-Lof type theory. We exhibit two principles which are not provable in the intensional formulation: uniqueness of identity and functional extensionality. We show that extensional type theory is conservative over the intensional one extended by these two principles, meaning that the same types are inhabited, whenever they make sense. The proof is non-constructive because it uses set-theoretic quotienting and choice of representatives.