The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

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