The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Loic Pottier wrote:
> Inductive paths (T:Type)(t:T): T -> Type :=   idpath: paths _ t t.
> Check (forall X:Type, paths _ X X).
>
> returns
>
> forall X : Type, paths Type X X
>      : Prop
>
> But I expected Type instead of Prop... where from does this Prop come???

I think this is the simulated universe polymorphism.  Coq detects that 
your definition could just as well be put in [Prop], and doing so only 
increases the set of valid contexts where your type could be used.  
Thus, the change happens automatically.

With more involved type definitions, you'll get different universes 
based on choices of type parameters to the inductive family.  Here, 
there is no such dependency, since you have only defined a single 
constructor with no arguments.