coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
>>
>>
>>
>
>
- [Coq-Club] Impredicative [ Set ], (continued)
- [Coq-Club] Impredicative [ Set ],
Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ],
Gregory Malecha
- Message not available
- Message not available
- Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ], Gregory Malecha
- Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ], Pierre Courtieu
- Message not available
- [Coq-Club] messy behavior with universes, Vladimir Voevodsky
- [Coq-Club] Re: [coqdev] messy behavior with universes, Tom Prince
- [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Carlos Simpson
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky
- Message not available
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Enrico Tassi
- Re: [Coq-Club] Impredicative [ Set ],
Gregory Malecha
- Message not available
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Andreas Abel
- [Coq-Club] THedu'11 at CADE: last call for ext.abstracts, Laurent Théry
- [Coq-Club] Impredicative [ Set ],
Vladimir Voevodsky
- [Coq-Club] an issue with notations, Vladimir Voevodsky
- [Coq-Club] a problem with canonical structures, Vladimir Voevodsky
- Re: [Coq-Club] a problem with canonical structures, Cyril Cohen
- [Coq-Club] Another question, Vladimir Voevodsky
- Re: [Coq-Club] Another question, Vincent Siles
- Re: [Coq-Club] an issue with notations, Hugo Herbelin
- Re: [Coq-Club] an issue with notations, Vladimir Voevodsky
Archive powered by MhonArc 2.6.16.