我能否在Coq中获得宇宙的继任者？

Question

我正在Coq开发一个用于Googology的库。到目前为止，该项目运行良好。但是，我有一个问题：能否在Coq中获得宇宙的后继者？

我可以在阿格达lsuc中获得宇宙的后继者。似乎Coq具有唯一的运算符max(_,_)。通过Print命令，我可以看到包含Type@{(Top.9)+1}的类似_+1的内容，但是我无法使用此表示法。

Answer 1

[遗憾的是，您无法在Coq中的任意上下文中编写后继Universe。仅允许某些用途，例如输入归纳定义的索引。 This Coq club thread更详细地讨论了该问题。