In "A Unification Algorithm for COQ Featuring Universe Polymorphism and Overloading", Ziliani and Sozeau say:

Terms include variables $x \in \mathcal{V}$, constants $c \in > \mathcal{C}$, inductive type constructors $i \in \mathcal{I}$ and constructors $k \in \mathcal{K}$, these last three being applied to universe instances $\bar{\ell}$ built from universe levels $\ell \in \mathcal{L}\cup 0^-$.

Now, $\mathcal{L}$ I recognize as Gödel's constructible universe, but what's $0^{-}$? And while I'm at it, what does it mean to "apply" a constant to a universe instance - as in $c|\bar\ell|$?


1 Answer 1


$\newcommand{\L}{\mathcal{L}}$It’s just a formal symbol. That is, by $\L \cup 0^-$ they mean the set $\L$ with one extra new element added, and they take $0^-$ as the name for that extra element.

While we’re at it, $\L$ is certainly not Gödel’s constructible universe here. I don’t think they explicitly say so in this paper, but if I understand right, $\L$ is just assumed to be some set of formal symbols used to represent universe levels — just like the set of “variables” that most treatments of syntax assume as a given, but they need a second such set here, to keep universe levels distinct from ordinary variables in their syntax. So it can be any infinite set.

(If you’re thinking of this as happening in a constructive meta-theory — which I am, and I guess Sozeau/Ziliani may well have been — then you will probably need to add the assumption that $\L$ has decidable equality. Again, I’m just copying the standard assumptions made for sets of variables used in syntax.)

  • $\begingroup$ Thanks! While I'm at it, any insight into $c|\bar\ell|$? $\endgroup$ Commented May 15, 2016 at 3:15
  • 1
    $\begingroup$ Again just a formal operation, taking as inputs a “constant” $c$ (i.e. an element of $\mathcal{C}$) and a “universe instance” $\bar{\ell}$ (i.e. an element of $\mathcal{L} \cup 0^-$. That whole definition of syntax is a definition in Backus-Naur Form; this is common in computer-science but unfamiliar to many mathematicians. A more traditional mathematical way to say it would be that the sets of terms, types, etc. are mutually freely generated by various operations; things like $c[\bar{\ell}]$ are then just notations for these operations. $\endgroup$ Commented May 15, 2016 at 3:24

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .