Generalizations of Hedberg's Theorem
Generalizations of Hedberg's Theorem
复制标题
海德伯格定理的推广
DOI：
10.1007/978-3-642-38946-7_14
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Thorsten Altenkirch
中科院分区：
文献类型：
--
作者：
Nicolai Kraus;M. Escardó;T. Coquand;Thorsten Altenkirch
正如Hofmann和Streicher的群组解释所表明的，身份证明的唯一性(UIP)是不可证明的。推广了Hedberg的一个定理，给出了满足uIP的类型的新刻画。事实证明，在这种情况下，考虑不变的内函数是很自然的。对于这样的函数，我们可以看看它的不动点的类型。我们证明了这种类型至多有一个元素，在没有uIP的情况下，这是一个非平凡引理。作为一种应用，可以定义匿名存在的新概念。另一个主要结果是，如果每种类型都有一个恒定的内函数，那么所有等式都是可判定的。所有的证明都已在AGDA中正式确定。
As the groupoid interpretation by Hofmann and Streicher shows, uniqueness of identity proofs (UIP) is not provable. Generalizing a theorem by Hedberg, we give new characterizations of types that satisfy UIP. It turns out to be natural in this context to consider constant endofunctions. For such a function, we can look at the type of its fixed points. We show that this type has at most one element, which is a nontrivial lemma in the absence of UIP. As an application, a new notion of anonymous existence can be defined. One further main result is that, if every type has a constant endofunction, then all equalities are decidable. All the proofs have been formalized in Agda.