The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Would « being extensional is an extensional concept » fit the bill?
If you're talking about predicates on functions then Prop's
impredicativity lets you apply the concept to itself and prove that,
indeed, being extensional is extensional.

=========================
Definition prop_extensional (A B : Type) (P : (A -> B) -> Prop) : Prop :=
  forall f g, (forall (a : A), f a = g a) -> P f -> P g.

Lemma prop_extensional_is_prop_extensional : forall A B,
prop_extensional (A -> B) Prop (prop_extensional A B).
Proof.
intros A B P Q eqPQ Pext f g eqfg.
 do 2 rewrite <- eqPQ.
 apply Pext.
 exact eqfg.
Qed.
=========================

But if you try to play the same game with [P] targetting Type, you end
with a universe inconsistency.

=========================
Definition type_extensional (A B : Type) (P : (A -> B) -> Type) : Type :=
  forall f g, (forall (a : A), f a = g a) -> P f -> P g.

Lemma type_extensional_is_type_extensional : forall A B,
type_extensional (A -> B) Type (type_extensional A B).
Proof.
intros A B P Q eqPQ Pext f g eqfg.
 do 2 rewrite <- eqPQ.
 apply Pext.
 exact eqfg.
Qed. (* Qed. fails *)
=========================

Cheers,

--
guillaume


On 25 July 2012 15:23, Benjamin C. Pierce 
<bcpierce AT cis.upenn.edu>
 wrote:
> What is the most elementary example showing why we want Prop to be 
> impredicative?
>
> Thanks!
>
>     - Benjamin
>