Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: [coqdev] messy behavior with universes

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: [coqdev] messy behavior with universes


chronological Thread 
  • From: Vladimir Voevodsky <vladimir AT ias.edu>
  • To: Carlos Simpson <Carlos.Simpson AT unice.fr>
  • Cc: Vladimir Aleksandrovich Voevodsky <vladimir AT ias.edu>, Tom Prince <tom.prince AT ualberta.net>, Coq-Club Club <coq-club AT inria.fr>, coqdev AT inria.fr
  • Subject: Re: [Coq-Club] Re: [coqdev] messy behavior with universes
  • Date: Mon, 18 Apr 2011 09:51:01 -0400

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





Archive powered by MhonArc 2.6.16.

Top of Page