Can I get the successor of an universe in Coq?

user_9372046 0
Viewed 77

I'm developing a library for googology in Coq. The project is working well so far. However, I have a question: Can I get the successor of an universe in Coq?

I can get the successor of an universe by lsuc in Agda. It seems that Coq has the only operator max(_,_). By the Print command, I can see something like Type@{(Top.9)+1} that includes _+1, but I can't use this notation.

coq
1 Answers

Unfortunately, you cannot write a successor universe in an arbitrary context in Coq. Only certain uses are allowed, such as entering the indices of an inductive definition. This Coq club thread discusses the issue in more detail.

user_16337700
Related