The Coq mailing list

[Carlos Simpson <Carlos.Simpson AT unice.fr>]

Dear Vladimir,
  It may be an interesting theoretical question to try to understand
what happens if we try to make all definitions parametric over universes.
Of course each time you make a new definition this introduces possibly many
new universe indices. It could have something to do with quantum mechanics
in that the ``universes'' which occur here might be related to the 
``universes'' in the many-universe interpretation of quantum mechanics.
---Carlos Simpson


Selon Vladimir Voevodsky 
<vladimir AT ias.edu>:

> Uhhh-uhh. I see. I got so used working with fixed universes that I forgot
> about this behavior. Thanks! V.
> 
> On Apr 15, 2011, at 7:24 PM, Tom Prince wrote:
> 
> > On 2011-04-15, Vladimir Voevodsky wrote:
> >> In the following example:
> >> 
> >> File 1 (ex1.v) :
> >> 
> >> Definition dneg (X:Type) := ((X -> Empty_set) -> Empty_set).
> >> 
> >> 
> >> File 2 (ex2.v):
> >> 
> >> Require Export ex1.
> >> Variable X:Set.
> >> Check (dneg X).
> >> Check ((X -> Empty_set)-> Empty_set).
> >> 
> >> 
> >> Coq responds that (dneg X) is in Type while ((X -> Empty_set)-> 
> >> Empty_set)
> is in Set. This does not look right.
> > 
> > This is expected. Everything in Set is also in type, so
> > 
> > Check ((X -> Empty_set)-> Empty_set) : Type.
> > 
> > Unfortunately, coq doesn't currently support looking through the
> > definition of dneg to see that (dneg X) is convertible with a term of
> > sort Set.
> > 
> > There is limited support for doing this with paramaters of inductives,
> > but nothing else.
> > 
> >  Tom
> 
> 
>