我能在Coq里找到宇宙的接班人吗？

Question

我正在用Coq开发一个谷歌库。到目前为止，这个项目进行得很顺利。然而，我有一个问题:我能在Coq中得到宇宙的继承者吗？

我可以通过lsuc在Agda中得到宇宙的继承者。Coq似乎是唯一的运算符max(_,_)。通过Print命令，我可以看到类似于Type@{(Top.9)+1}的东西，其中包括_+1，但是我不能使用这个符号。

Answer 1

不幸的是，您不能在Coq中的任意上下文中编写后续宇宙。只允许某些用途，例如输入归纳定义的索引。这个Coq俱乐部螺纹更详细地讨论了这个问题。