The Coq mailing list

["Carlos.SIMPSON" <carlos AT math1.unice.fr>]

This axiom is a consequence of the axiom:

Axiom Extensionality_Ensembles:
   (A,B: Ensemble) (Same_set A B) -> A == B.

to be found in the standard library
Module Coq.Sets.Ensembles.

Here is the code:

Require Ensembles.

Inductive U : Type := u:U.

Definition prop_ens :Prop -> (Ensemble U) := [P:Prop; u:U]P.

Lemma iff_implies_eqT : (P,Q:Prop)(P<->Q)->(P==Q).
Intros.
Assert (prop_ens P) == (prop_ens Q).
Apply Extensionality_Ensembles.
Unfold Same_set.
Apply conj.
Unfold Included.
Intros.
Unfold In.
Unfold prop_ens.
Apply (proj1 ? ? H).
Exact H0.
Unfold Included.
Intros.
Unfold In.
Unfold prop_ens.
Apply (proj2 ? ? H).
Exact H0.
Change (prop_ens P u) == (prop_ens Q u).
Rewrite H0.
Trivial.
Save.


As to whether it is consistent to add the axiom
Extensionality_Ensembles,
one assumes that people think it is consistent since it is in the
standard library;
however it is not totally clear that anybody has really proven this
(???).
It would definitely seem to be ok if one stays away from the problem of
the impredicativity of the sort Set (there is an article by Coquand
where
he explains  how to do this by making a variant of the standard
set-theoretic
interpretation of Type and Prop).  On the other hand, consistency of
this
axiom with the impredicative sort Set would seem to be a nontrivial
theorem.

Actually I have a sort of recollection that this was already discussed
on the list
but I don't find it in the archives....

Finally, my own experience was that this type of assumption seemed very
useful
when starting out, but after a while one realizes that it probably isn't
really necessary.

----Carlos