universe polymorphism problem

[Vladimir Voevodsky]

Here is a little Coq file that does not compile that shows one of the problems with the current approach to universe polymorphism in Coq:

[Michael Shulman]

It seems to me to compile just fine if you add "Set Universe
Polymorphism." at the top. (Universe polymorphism isn't enabled by
default, you have to turn it on.)

On Fri, Jul 17, 2015 at 2:04 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> Here is a little Coq file that does not compile that shows one of the problems with the current approach to universe polymorphism in Coq:
>

> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>
>
>
> Vladimir.
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.
>

[Vladimir Voevodsky]

If I add “Set Universe Polymorphism” then how can I fix a universe and a variable in that particular universe?

[Michael Shulman]

On Fri, Jul 17, 2015 at 3:17 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> If I add “Set Universe Polymorphism” then how can I fix a universe and a variable in that particular universe?

I would say the point of universe polymorphism is that we don't *need*
to fix particular universes. What are you trying to achieve?

[Vladimir Voevodsky]

I am trying to obtain an answer to the question that I have asked.

[Michael Shulman]

It seems to me that fixing a universe is not something you should need
to do in a universe-polymorphic theory. I don't see any intrinsic
reason why one would want to fix a universe, so I assumed that you
wanted to do it with some more substantive purpose in mind. I thought
that if you explained that purpose, then either we could find a
different way to achieve it in current universe-polymorphic Coq, or
else I would understand why current universe-polymorphic Coq is
insufficient for your needs. So why do you want to fix a particular
universe?

On Fri, Jul 17, 2015 at 3:22 PM, Vladimir Voevodsky <vlad...@ias.edu> wrote:
> I am trying to obtain an answer to the question that I have asked.
>

[Jason Gross]

To answer the technical question, you can do

Monomorphic Definition foo := ...

-Jason

[Vladimir Voevodsky]

Thanks! I now try a much simpler code:

***

Set Universe Polymorphism.

Set Printing All.

Set Printing Universes .

Definition UU' := Type .

Definition UU : UU' := Type .

Variable T : UU .

Type T .

Type T .

****

and at the first printing I am told that T@{Top.6 Top.7}  is in UU@{Top.6 Top.7} and at the second that T@{Top.8 Top.9} is in UU@{Top.8 Top.9}.

What does it mean?

Vladimir.

[Jason Gross]

It means that every time you mention [T], you get fresh universes.  You probably want to make your definitions of UU' and UU monomorphic definitions, and make everything else polymorphic.  Alternatively, you can do something like

Set Universe Polymorphism.
Universes uu uu'.
Definition UU' := Type@{uu'}.
Definition UU : UU' := Type@{uu}.

And then you'll get actual names for your universes (I think you could even call them UU and UU'), since [Universe] declares global universe variables.

-Jason

[Michael Shulman]

I say again, however, that I doubt that this is really what you should
want to do. I would be really interested to hear why you want to fix
particular universes.

On Sat, Jul 18, 2015 at 5:41 PM, Jason Gross <jason...@gmail.com> wrote:
> It means that every time you mention [T], you get fresh universes. You
> probably want to make your definitions of UU' and UU monomorphic
> definitions, and make everything else polymorphic. Alternatively, you can
> do something like
>
> Set Universe Polymorphism.
> Universes uu uu'.

> Definition UU' := Type@{uu'}.

> Definition UU : UU' := Type@{uu}.
>
> And then you'll get actual names for your universes (I think you could even
> call them UU and UU'), since [Universe] declares global universe variables.
>
> -Jason
>

[Vladimir Voevodsky]

And what are the double indexes as in {Top.6 Top.7}?

[Jason Gross]

One is "the universe of UU" and the other is "the universe of UU'"; the constraint enforced is not the UU + 1 = UU', but merely UU < UU'.

-Jason