coq - Burali-Forti 悖论的 Coq 类似物？

Question

刚从CMU HoTT的lectures中了解到，虽然Check Type在Coq中返回的是Type : Type，但是左边的Type和 right 由不同的数字隐式索引，因为如果它们相同，这将导致 Burali-Forti 悖论的类型理论类比。如果你试图实现这样的悖论，Coq 将拒绝编译。

我很好奇这个悖论在 Coq 脚本中是什么样子，但找不到任何代码。一些讨论引用了 B. Barras 的“A formalization of Burali-Forti's paradox in coq”，但链接已断开。这个悖论有 Coq 实现吗？

Answer 1

快速浏览了一下，也没有找到 Barras 的论文。然而，您可以在 Coq 测试套件中找到这个悖论的一些实例。我不知道该套件是否随 Coq 的“打包”版本一起提供，但如果您下载 Coq 源码包，您可以查看 test-suite/failure/universes-buraliforti- redef.v 例如(grep 以查找其他几个事件)。