Burali-Forti 悖论的 Coq 类似物？
A Coq analogue of the Burali-Forti paradox?
刚从CMU HoTT的lectures上了解到，虽然Coq中的Check Type returns Type : Type，左右两边的Type隐式索引为不同的数字，因为如果它们相同，则会导致 Burali-Forti 悖论的类型理论模拟。如果你试图实现这样的悖论，Coq 将拒绝编译。
我很好奇这个悖论在 Coq 脚本中是什么样子，但找不到任何代码。一些讨论参考了 B. Barras 的 "A formalisation of Burali-Forti's paradox in coq"，但它的 link 已损坏。这个悖论有 Coq 实现吗？
快速浏览了一下，也没有找到巴拉斯的论文。但是，您可以在 Coq 测试套件中找到此悖论的一些实例。我不知道该套件是否随 "packaged" 版本的 Coq 一起提供，但是如果您下载 Coq 源码包，您可以查看 test-suite/failure/universes-buraliforti-redef.v 例如（grep 到找到其他几个事件）。
我在 Coq 中编写了 Per Martin-Loef 版本的证明，以及描述证明的相当详细的 blog post。
刚从CMU HoTT的lectures上了解到，虽然Coq中的Check Type returns Type : Type，左右两边的Type隐式索引为不同的数字，因为如果它们相同，则会导致 Burali-Forti 悖论的类型理论模拟。如果你试图实现这样的悖论，Coq 将拒绝编译。
我很好奇这个悖论在 Coq 脚本中是什么样子，但找不到任何代码。一些讨论参考了 B. Barras 的 "A formalisation of Burali-Forti's paradox in coq"，但它的 link 已损坏。这个悖论有 Coq 实现吗？
快速浏览了一下，也没有找到巴拉斯的论文。但是，您可以在 Coq 测试套件中找到此悖论的一些实例。我不知道该套件是否随 "packaged" 版本的 Coq 一起提供，但是如果您下载 Coq 源码包，您可以查看 test-suite/failure/universes-buraliforti-redef.v 例如（grep 到找到其他几个事件）。
我在 Coq 中编写了 Per Martin-Loef 版本的证明，以及描述证明的相当详细的 blog post。