[Agda] More universe polymorphism

[Guillaume Brunerie]

(1) Why are you using this complicated f instead of \ i -> Set i, is
it supposed to be bigger somehow? But anyway yes, it’s a function
whose type is big, so what?

(2) Yes, Agda’s universe polymorphism is more expressive than MLTT
with countably many universes. But as I said above you can see such
large types and terms as living in the meta-level. In MLTT with
countably many universes you can still define your f as an external
macro (or notational convention), but in Agda this is actually part of
the language.

(3) How do you derive a contradiction if the type of f has a type?
Because in the extension of universe polymorphism I’m proposing, the
type of f would have a type (Set \omega, for \omega the sup of the
omega first universe levels) so I would be interested if you can prove
that this system is inconsistent.

> You see, how can you formulate a type system to derive f if the type of f is not derivable?

I don’t understand what you mean.
I think we both agree that we cannot have both a type of universe
levels and the property that every type belongs to some universe. You
want to get rid of the type of universe levels but I would rather get
rid of the fact that every type belongs to some universe.
In particular a type can be derivable without belonging to any
universe and there is nothing forbidding you to inhabit such large
types. The type of f is {l : Level} (n : ℕ {l}) → Set(newlife n) which
is a correct type (using the framework-level Pi, which is not a Pi
inside any universe) and you can inhabit it via lambda-abstraction and
large elimination.

> In fact, I pose this as an open problem: formulate the correct Agda terms (in particular, types) in a deductive system `a la Martin-Lof.

What is the open problem more precisely? I guess you want a consistency proof?

Guillaume

2013/6/29 Martin Escardo <m.escardo at cs.bham.ac.uk>:
>
> Actually, I sympathize with almost everything you say below,
> particularly understanding what is going on with universe levels. It
> did help me too to work with explicit universe levels (sort of,
> actually). But once you understand it, typical ambiguity is easier to
> work with.
>
> However, I yet have to see a precise formal definition of MLTT with
> countably many universes and a *type* of universe levels. I haven't
> ever seen such a thing, and I don't think it is possible, even if you
> extend the cardinality of the indices for universes:
>
>  (1) What about my function f such that
>
>      f(n+1) = Set_n -> ... Set_0 -> N
>
>      This is far too big for the universes Agda can currently cope
>      with, yet you can write it down and have it accepted.
>
>  (2) In MLTT with countably many universes, f cannot be written
>      down. So Agda is extrapolating. Fine with me if you like
>      extrapolations, but the fact remains that both Agda has countably
>      many universes (only) and the type of f cannot have a type in
>      Agda.
>
>  (3) I believe that if you formulate precisely a version of type
>      theory with universes and a type of universe type-levels, you
>      will be able to derive the Burali-Forti paradox. I actually could
>      have done that in Agda if the type of f had a type (this is what
>      I was aiming for). You see, how can you formulate a type system
>      to derive f if the type of f is not derivable? In fact, I pose
>      this as an open problem: formulate the correct Agda terms (in
>      particular, types) in a deductive system `a la Martin-Lof. I
>      don't think this can be done with a type of universe levels
>      (prove me wrong).
>
> Best,
> Martin
>
>
>
> On 29/06/13 01:00, Guillaume Brunerie wrote:
>>
>> 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
>>
>