The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Dear Carlos,

there is no need to introduce a new universe every time "Type" is mentioned. 
At the beginning of the file one declares the universe structure which one 
wants to work with by something like

Variable UU0 UU1 : Univ.

etc.

(of course currently there is no identifier Univ and also Univ is not a type. 
May be one should use something other than : with Univ.)


Then  one can have a definition like that:

Definition iscontr {U:Univ}(T:U) : U := ....

which is polymorphic or like that

Definition trrr (T:UU0):UU0 :=

which assumes a fixed universe UU0.


Vladimir.




On Apr 16, 2011, at 10:26 AM, Carlos Simpson wrote:

> 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
>> 
>> 
>> 
> 
>