The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

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.