The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Frederic's answer is pretty spot on. The detailed answer goes like this:

• Types that support singleton elimination go in Prop, so Q maps to  Prop, as it does not lose anything (like, no need of squashing).
• Prop is stable by forall, so forall x y, Q x y is in Prop
• cow Q only has type Type
  
• Unfolding cow Q adds possible types, because that's what reductions tends to do.

It's non-trivial that unfolding definition would add some types, though, bullet 3 is non-trivial. The reason would be that cow has type  forall (P:forall (x:A), A->Type_i), Type_i+1 , as Type-s are predicative. So when you pass it a P that maps to Prop, it returns something of type Type_1 (the type of Prop), without realizing that, as Prop is stable by arbitrary forall-s, it could have had a specific typing rule. That's pretty much what you would expect, unless you have some kind of disjunction types.

As far as homotopy type theory goes, as long as you don't mention Prop explicitely (which coerces inductive into doing some kind of squashing, hence going beyond the power of MLTT+univalence), you can ignore Prop safely.


Arnaud

On 18 April 2012 10:32, Frederic Blanqui <frederic.blanqui AT inria.fr> wrote:

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