The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

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