The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

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.
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