Могу ли я получить преемника вселенной в Coq?

Question

Я разрабатываю библиотеку для гугологии в Coq. Пока проект работает хорошо. Однако у меня есть вопрос: могу ли я получить преемника вселенной в Coq?

Я могу получить преемника вселенной в lsuc в Агде. Кажется, что у Coq есть единственный оператор max(_,_). По команде Print я вижу что-то вроде Type@{(Top.9)+1}, которое включает _+1, но я не могу использовать эту запись.

Answer 1

К сожалению, вы не можете написать преемник юниверса в произвольном контексте в Coq. Допускается только определенное использование, например ввод индексов индуктивного определения. Эта ветка Coq club обсуждает проблему более подробно.