[Agda] More universe polymorphism

[Guillaume Brunerie]

Martin Escardo wrote:
> I show below that, in the presense of universe levels, there is an
> Agda type that doesn't have any Agda type.
> [...]
> Indeed, there is something fishy about having a type of universe
> levels,
> [...]
> I would rather have typical ambiguity in Agda,

There is a much shorter example of a type that doesn’t have a type:

-- Works
x : (i : Level) -> Set (lsucc i)
x = \ i -> Set i

-- Fails
X' : ?
X' = (i : Level) -> Set (lsucc i)

But I don’t see a problem with that, I’m perfectly happy with the fact
that not every type is small. I would even say that it would seem
fishy to me if everything was small.
Moreover, when I started using Agda I already knew a bit of Coq, and I
found Agda’s explicit universe polymorphism much easier to understand
than Coq’s typical ambiguity. It’s more painful to use, but at least
you understand what you’re doing.
To give a concrete example, here are three mathematical theorems (most
likely formalizable in type theory)

1) The category of sets is complete
2) Every *small* complete category is a preorder
3) The category of sets is not a preorder

In a system with typical ambiguity, the smallness condition is
completely invisible so instead of 2) you can only state and prove the
following:

2') Every complete category is a preorder

Of course, 1) + 2') + 3) looks inconsistent, but it’s only when you
try to prove false from them that you get the "Universe inconsistency"
error.
With explicit universe polymorphism, you can express smallness so
there is no problem, nothing looks inconsistent.
If you look closely at the HoTT book, you will find a few places where
we switch back to explicit universe management because typical
ambiguity is not precise enough.

> I think the notion of universe level is (or ought to be) a meta-level
> concept. At least this is so in Coq, in Homotopy Type Theory, and in
> the patched version of Coq for Homotopy Type Theory.

Just to make sure there are no misconceptions, it’s not correct to say
that the notion of universe level is a meta-level concept in homotopy
type theory. We indeed decided to use typical ambiguity in the HoTT
book, but we could just as well have used Agda-style universe
polymorphism. Homotopy type theory has nothing to do with universe
management.

Also if you prefer you can call "type" every Agda term whose Agda type
is Set i for some i : Level, and "metatype", or "framework type" for
every other Agda type. Then call "term" every Agda term whose Agda
type is a "type" and "template", or "macro" every Agda term whose Agda
type is a "framework type".

So universe management is still somehow part of the meta-level, except
that one layer of this meta-level is also implemented in Agda.

> Moreover, ignoring the above, explicit universe levels as in Agda are
> painful

I think that what makes universe management painful in Agda is not the
explicit universe polymorphism but rather the lack of cumulativity.
For instance when you define Sigma-types in the most polymorphic way,
you need two different universe levels and the Sigma-type ends up in
the max of the two levels. With cumulativity you could have only one
level.
Similarly, if you have a module where you don’t have to raise any
universe level, you could just parametrize your module by a universe
level `i` and use `Set i` everywhere. That’s not more painful than
--type-in-type and you have the added bonus that you can express
smallness conditions when you need to.

> (Moreover, how can one be sure that adding a type of universe levels
> doesn't lead to logical inconsistency? What is shown below is not an
> inconsistency, but I think is close to one.)

It seems pretty straightforward to give a set-theoretic model of MLTT
+ Agda’s explicit universe polymorphism.
In what follows I’m working in ZFC + enough inaccessible cardinals.

There are two different kind of things: types and terms (not every
type being a term of some universe).
Every type is interpreted as a family of sets (parametrized by the
context) and every term as an dependent element of the interpretation
of its type.
The type of universe levels is interpreted as the set of natural numbers N.
The operations lzero, lsucc, lmax as interpreted in the obvious way.
The type family (i : Level) |- Set i  is interpreted as the sequence
(V_{\kappa_n})_{n\in N} where \kappa_n is the nth inaccessible
cardinal.
Everything else is interpreted as usual.
Note that there is a notion of Pi-type in every fixed universe but
there is also a notion of Pi-type for a not necessarily small family
of types (this is necessary for the type (i : Level) -> Set (lsucc i)
to make sense).
Semantically they are both interpreted in the obvious way.

In this model, a type is small when its rank is < sup(\kappa_n). But
for instance the type (i : Level) -> Set (lsucc i) is interpreted as a
set of rank sup(\kappa_n), so it’s a type which is not small, but
there is no problem.

One can also get a similar hand-waving model for the kind of universe
polymorphism I was sketching in my first message.

Let’s assume that there is a 1-inaccessible cardinal L (that means
that L is the L-th inaccessible cardinal).
The type of universe levels is interpreted as L.
The type family (i : Level) |- Set i is interpreted as above, as
(V_{\kappa_\alpha})_{\alpha\in L} where \kappa_\alpha is the \alpha-th
inaccessible cardinal.
The operations lzero, lsucc and lsup are interpreted in the obvious
way. Note that a small type is of rank < \kappa_L = L, hence of
cardinality < L. Hence any small collection of elements of L has a sup
in L, so lsup is well-defined. Also, the type of universe levels
cannot be small.
Everything else is interpreted as usual.

This is really sketchy but maybe it’s enough to convince you that
there should not be any inconsistency.

Guillaume