The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

I believe that this goes under the name of "universe polymorphism".  I
think a version of it is implemented in Agda (turned on by a flag),
where there is a builtin type called something like "Level", and given
i:Level one writes "Set i" to mean the i-th universe.

The homotopy type theorists have been pushing for something like this
too.  As you say, it would help a lot with universe inconsistencies;
not just in tracking them, but in avoiding them altogether by the
ability to define an object polymorphically over multiple universes.
But I suppose it is quite a nontrivial thing to implement.

On Mon, Apr 30, 2012 at 02:19, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> Hi all, I was wondering if that could be some nice stuff to have types
> which depend on universe(s).
>
> More precisely, imagine the following code:
>
> Record Category : Type :=
> { object : Type
> ; morphism : object -> object -> Type
> ; id : forall O, morphism O O
> ; ...
> }.
>
> Record Functor (A B : Category) : Type :=
> { fmap : morphism A -> morphism B
> ; ...
> }
>
> Then, we cannot (of course!) define the category of categories, due to
> the universe system.
>
> Definition categories : Category :=
> {| object := Category
>  ; morphism := Functor
>  ; ...
> |}.
>
> But now if we could write:
>
> Record Category<U> : Type<U+1> :=
> { object : Type<U>
> ; morphism : object -> object -> Type<U>
> ; id : forall O, morphism O O
> ; ...
> }.
>
> Record Functor<U> (A B : Category<U>) : Type<U+1> :=
> { fmap : morphism A -> morphism B
> ; ...
> }
>
> Definition categories<U> : Category<U+1> :=
> {| object := Category<U>
>  ; morphism := Functor<U>
>  ; ...
> |}.
>
> I don't really know if that is very relevant to have such a system, so
> I am asking on the list if there would be some inconsistancies or stuff
> like that.
>
> Of course, whether the type system would have to be changed (to support
> universe annotations), whether such defined types should always be
> applied to its universe, so that "Category" wouldn't be typed, but
> "Category<Set>" would be (and its type would be Type<Set+1>).
>
> I used the same notations between bra and ket as the one given by the
> "Show Universe Level" directive.
>
> I think this could also be usefull to track universe inconsistencies.