The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Yours is a typical use-case for "universe polymorphism" which will be
available in the next version of Coq (8.5).

(See http://www.emn.fr/z-info/ntabareau/papers/universe_polymorphism.pdf )

I know a few people have formalized category-theory in Coq; they
probably have other approaches to suggest to avoid universe-level
trouble.

On Thu, Jan 22, 2015 at 9:23 AM, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:
> Gabriel,
>
> Thank you. Yep, "Top" is little bit confusing :)
>
> Am I right that we still can't instantiate this definition of Category to
> "category of small categories"?
> I mean that these variables are not "flexible" enough. Is it true?
>
> Sincerely,
> Kirill Taran
>
> On Thu, Jan 22, 2015 at 11:05 AM, Gabriel Scherer
> <gabriel.scherer AT gmail.com>
>  wrote:
>>
>> The toplevel variables are not usually fixed but flexible (akin to
>> unification variable, although their state evolve by comparison
>> constraints rather than unification only). Top.14 and Top.8 denote
>> such variables that are not fully-determined yet. They contain the
>> name Top because you test from the toplevel; put this code in Foo.v
>> and you'll see something like Foo.3 and Foo.4 instead.
>>
>> (I agree that "Top" is somewhat confusing as one thinks first of the
>> top element of a lattice. It's just the toplevel.)
>>
>> On Thu, Jan 22, 2015 at 8:39 AM, Kirill Taran 
>> <kirill.t256 AT gmail.com>
>> wrote:
>> > Hello,
>> >
>> > I am playing with "Set Printing Universes". Some types has universe
>> > level
>> > like "Top.14" or "Top.8". What does it mean? Is it fixed level or
>> > variable?
>> >
>> > For instance,
>> >     Set Printing Universes.
>> >     Record Category : Type := {
>> >       Ob : Type;
>> >       Hom : Ob -> Ob -> Type
>> >     }.
>> >     Check Category.
>> > gives output:
>> >     Category : Type (* max ((Top.14)+1, (Top.15)+1) *)
>> >
>> > Sincerely,
>> > Kirill Taran
>
>