Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


chronological Thread 
  • From: Vladimir Voevodsky <vladimir AT ias.edu>
  • To: Tom Prince <tom.prince AT ualberta.net>
  • Cc: Coq-Club Club <coq-club AT inria.fr>, coqdev AT inria.fr
  • Subject: [Coq-Club] Re: [coqdev] messy behavior with universes
  • Date: Sat, 16 Apr 2011 08:43:17 -0400

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