The Coq mailing list

[Ali Assaf <ali.assaf AT inria.fr>]

Hi James,

There are several things going on here and I am not sure which one your 
question is about.

First, you are using an implicit argument {A : Set} in the first definition, 
which is why you get the ?9 in the output. If you replace it by an explicit 
argument (x : Set) you get forall A : Set, (A -> Prop) -> Set.

Second, you are checking AProp and checking {A : Set} (Q : A -> Prop) (x : 
A), Q x. These are different things because AProp is a function that takes 
two arguments and returns a type, equivalent to fun (A : Set) => fun (Q : A 
-> Prop) => forall x : A, Q x, while the second is a type itself, of type 
Prop.

Third, if you were wondering why AProp is in Set while Q has type A -> Prop, 
the answer is that Prop is included in Set, that is any term of type Prop 
also has type Set. This property is called cumulativity and can be seen in 
the subtyping rules of Coq 
(https://coq.inria.fr/distrib/current/refman/Reference-Manual006.html#sec171).
 Note that it is not the same as saying that Prop has type Set.

Hope this helps,

Ali

----- Original Message -----
> From: "James Tyler" 
> <jameskatyler AT gmail.com>
> To: 
> coq-club AT inria.fr
> Sent: Thursday, December 18, 2014 9:16:00 PM
> Subject: [Coq-Club] Prop-Set interactions of an unfamiliar kind
> 
> I am not sure why this is valid:
> 
>    Definition AProp {A : Set} (Q : A -> Prop) : Set :=
>      forall x : A, Q x.
>    Check AProp.
>    (* Output : (?9 -> Prop) -> Set *)
>    Check forall {A : Set} (Q : A -> Prop) (x : A), Q x.
>    (* Output : Prop *)
> 
> Does this have something to do with Definitions being opaque? According
> to the triplets on Pg. 92 of Coq'Art, I shouldn't be allowed to do this.
> I stumbled upon this and I'm not entirely sure why one would want to do
> it either. Thoughts?
>