The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello.

Le 18/04/2012 16:07, Andrej Bauer a écrit :
> Consider the following example:
>
> Parameter A : Type.
> Definition cow (P : forall (x : A), A ->  Type) := forall x y : A, P x y.
> Inductive Q (x : A) : A ->  Type := horn : Q x x.
The "problem" seems to be here already since, for Coq, Q has type 
A->A->Prop instead of A->A->Type as written explicitly.

And, if you have two constructors, then you get Set which is at the 
bottom of the Type hierarchy:

Inductive Q'(x:A):A->Type:=h1:Q' x x|h2:Q' x x.

Coq < Check Q'.
Q'
     : A -> A -> Set

Therefore, I guess that this is related to the fact that there is only 
one constructor. I believe that there is a special treatment in this 
case. It allows for instance elimination on well-foundedness proofs.

Frederic.

> Definition q := cow Q.
> Definition r := forall x y : A, Q x y.
>
> r is just q expanded out by hand, but q is in Type and r is in Prop.
> This seems awfully wrong. Can someone convince me that it is not a
> bug? It destroys homotopy type theory in Coq, where we want to keep
> things in Type.
>
> With kind regards,
>
> Andrej