The Coq mailing list

[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