[Agda] More universe polymorphism

[Martin Escardo]

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
>