The groupoid model refutes uniqueness of identity proofs

The groupoid model refutes uniqueness of identity proofs
复制标题

DOI：
10.1109/lics.1994.316071
复制
发表时间：
1994-07
期刊：
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
通讯作者：
M. Hofmann;T. Streicher
M. Hofmann;T. Streicher
中科院分区：
其他
文献类型：
--
作者：
M. Hofmann;T. Streicher

文献摘要

被引文献

相似文献

我们给出了一个基于群形和群形纤维化的内涵马丁-洛夫类型理论模型，其中恒等类型可能包含两个不同的元素，甚至在介词上都不相等。这表明身份证明唯一性原则在语法中是不可推导的。>
We give a model of intensional Martin-Lof type theory based on groupoids and fibrations of groupoids in which identity types may contain two distinct elements which are not even prepositionally equal. This shows that the principle of uniqueness of identity proofs is not derivable in the syntax.>