<br />
<b>Deprecated</b>:  The each() function is deprecated. This message will be suppressed on further calls in <b>/home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php</b> on line <b>456</b><br />
(************************************************************************)
(*                      Zermolo Set Theory                              *)
(*                                                                      *)
(*                        Benjamin Werner                               *)
(************************************************************************)


(* This is an encoding of usual Set Theory, simillar to Peter Aczel's work *)
(* in the early 80's. The main difference is that the propositions here    *)
(* live in the impredicative world of "Prop". Thus, priority is given to   *)
(* expressivity against constructivity.                                    *)

(* Since the definition of Sets is the same for both approaches, I added   *) 
(* most  of Aczel's encoding of CZF at the end of the file. Many           *)
(* definitions are common to both aproaches.                               *)


(* The type representing sets  (Ensemble = french for set) *)

Inductive Ens : Type :=
 sup : (A:Type)(A->Ens)->Ens.

(* Existential quantification *)

Inductive EX [P:Type; Q:P->Prop]: Prop :=
 EXi : (x:P)(Q x)->(EX P Q).

(* Cartesian product in Type *)

Inductive prod_t [A,B:Type] : Type :=
 pair_t : A->B->(prod_t A B).


(* Existential on the Type level *)

Inductive depprod [A:Type; P : A->Type] : Type :=
 dep_i : (x:A)(P x)->(depprod A P).


(* Recursive Definition of the extentional equality on sets *)

Definition EQ : Ens -> Ens -> Prop.
Induction 1; Intros A f eq1.
Induction 1; Intros B g eq2.
Apply and.
Exact (x:A)
        (EX ? [y:B](eq1 x (g y))).
Exact (y:B)
        (EX ? [x:A](eq1 x (g y))).
Save.

Transparent EQ.

(* Membership on sets *)

Definition IN: Ens -> Ens -> Prop :=
[E1,E2:Ens]
  Cases E2 of
    (sup A f) => (EX ? [y:A](EQ E1 (f y)))
 end.
Transparent IN.


(* INCLUSION *)

Definition INC : Ens -> Ens -> Prop.
Intros E1 E2.
Exact (E:Ens)(IN E E1)->(IN E E2).
Save.
Transparent INC.


(* EQ is an equivalence relation  *)

Theorem EQ_refl : (E:Ens)(EQ E E).
Induction E.
Intros A f HR.
Simpl.
(Split; Intros).
(Exists  x; Auto).

(Exists  y; Auto).
Save.

Theorem EQ_tran : (E1,E2,E3:Ens)(EQ E1 E2)->(EQ E2 E3)->(EQ E1 E3).
Induction E1; Intros A1 f1 r1; Induction E2; Intros A2 f2 r2; 
      Induction E3; Intros A3 f3 r3; Simpl; Intros e1 e2.
Split; (Elim e1;Intros I1 I2 ;Elim e2;Intros I3 I4).
Intros a1;Elim (I1 a1); Intros a2.
Elim (I3 a2); Intros a3.
Exists a3.
Apply r1 with (f2 a2); Auto.
Intros a3; Elim (I4 a3); Intros a2; Elim (I2 a2); Intros a1; Exists a1.
Apply r1 with (f2 a2); Auto.
Save.

Theorem EQ_sym : (E1,E2:Ens)(EQ E1 E2)->(EQ E2 E1).
Induction E1; Intros A1 f1 r1;
        Induction E2; Intros A2 f2 r2; Simpl; 
                Induction 1; Intros e1 e2; Split.
Intros a2;Elim (e2 a2); Intros a1 H1; Exists a1; Auto.
Intros a1; Elim (e1 a1); Intros a2 H2; Exists a2; Auto.
Save.

Theorem EQ_INC : (E,E':Ens)(EQ E E')->(INC E E').
Induction E; Intros A f r;
        Induction E'; Intros A' f' r'; 
              Simpl; Induction 1; Intros e1 e2; Unfold INC; Simpl.
Intros C; Induction 1; Intros a ea; Elim (e1 a); Intros a' ea'; Exists a'.
Apply EQ_tran with (f a); Assumption.
Save.

Hint EQ_sym EQ_refl EQ_INC.

(* easy lemma *)

Theorem INC_EQ : (E,E':Ens)(INC E E')->(INC E' E)->(EQ E E').
Induction E; Intros A f r;
        Induction E'; Intros A' f' r';
Unfold INC; Simpl; Intros I1 I2; Split.
Intros a; Apply I1.
Exists a; Auto.
Intros a'; Cut (EX A [x:A](EQ (f' a')(f x))).
Induction 1; Intros a ea; Exists a; Auto.
Apply I2; Exists a'; Auto.
Save.

Hint INC_EQ.


(* Membership is extentional (i.e. is stable w.r.t. EQ)   *)

Theorem IN_sound_left : 
                (E,E',E'':Ens)
                  (EQ E E')->(IN E E'')->(IN E' E'').
Induction E''; Intros A'' f'' r'' e; Simpl; 
        Induction 1; Intros a'' p;
        Exists a''; Apply EQ_tran with E; Auto.
Save.

Theorem IN_sound_right :
                (E,E',E'':Ens)
                   (EQ E' E'')->(IN E E')->(IN E E'').
Induction E'; Intros A' f' r'; 
        Induction E''; Intros A'' f'' r'';
        Simpl; Induction 1; Intros e1 e2;
        Induction 1; Intros a' e';
        Elim (e1 a'); Intros a'' e''; 
        Exists a''; Apply EQ_tran with (f' a'); Assumption.

Save.

(* Inclusion is reflexive, transitive, extentional *)

Theorem INC_refl : (E:Ens)(INC E E).
Unfold INC; Auto.
Save.

Theorem INC_tran : (E,E',E'':Ens)(INC E E')->(INC E' E'')->(INC E E'').
Unfold INC; Auto.
Save.


Theorem INC_sound_left :
               (E,E',E'':Ens)
                  (EQ E E')->(INC E E'')->(INC E' E'').
Induction E''; Unfold INC; Simpl; Intros A f HR e H1 E0 i; Apply H1.
Apply IN_sound_right with E'; Auto.
Save.

Theorem INC_sound_right :                
               (E,E',E'':Ens)
                 (EQ E' E'')->(INC E E')->(INC E E'').
Induction E'; Induction E''; Unfold INC; Simpl; Intros.
Elim (H2 E0); Try Assumption; Intros.
Elim H1; Intros HA HB; Elim (HA x); Intros.
Exists x0; Apply EQ_tran with (e x); Auto.
Save.


(* Useful types (actually top and bottom)   *)

Inductive Set Un := void : Un.

Inductive Set F := .

(* The empty set  (vide = french for empty)   *)

Definition Vide : Ens :=
 (sup F
      [f:F]<Ens>Cases f of 
   end).

Transparent Vide.

(* The axioms of the empty set *)

Theorem Vide_est_vide : (E:Ens)(IN E Vide)->F.
Unfold Vide; Simpl; Intros E H; Cut False.
Induction 1.
Elim H; Intros x; Elim x.
Save.


Theorem tout_vide_est_Vide : (E:Ens)((E':Ens)(IN E' E)->F)->(EQ E Vide).
 Unfold Vide; Induction E; Simpl; Intros; Split.
Intros; Elim (H0 (e x)); Auto.
Exists x; Auto.
Induction y.
Save.

(* Pair *)

Definition Paire : (E,E':Ens)Ens.
Intros.
Apply (sup bool).
Induction 1.
Exact E.
Exact E'.
Save.

Transparent Paire.

(* The pair construction is extentional *)

Theorem Paire_sound_left : (A,A',B:Ens)
                        (EQ A A')->(EQ (Paire A B)(Paire A' B)).
Unfold Paire .
Simpl.
(Intros; Split).
Induction x.
(Exists  true; Auto).

(Exists  false; Auto).

(Induction y; Simpl).
(Exists  true; Auto).

(Exists  false; Auto).
Save.

Theorem Paire_sound_right : (A,B,B':Ens)
                (EQ B B')->(EQ (Paire A B)(Paire A B')).
Unfold Paire; Simpl; Intros; Split.
Induction x.
(Exists true; Auto).
Exists false; Auto.
Induction y.
(Exists true; Auto).
Exists false; Auto.
Save.

Hint Paire_sound_right Paire_sound_left.

(* The axioms of the pair *)

Theorem IN_Paire_left : (E,E':Ens)(IN E (Paire E E')).
Unfold Paire; Simpl; Exists true; Simpl; Auto.
Save.

Theorem IN_Paire_right : (E,E':Ens)(IN E' (Paire E E')).
Unfold Paire; Simpl; Exists false; Simpl; Auto.
Save.

Theorem Paire_IN : (E,E',A:Ens)(IN A (Paire E E'))->(EQ A E)\/(EQ A E').
Unfold Paire; Simpl.
Induction 1; Intros b; Elim b; Simpl; Auto.
Save.

Hint IN_Paire_left IN_Paire_right Vide_est_vide.

(* The singleton set  *)
(* Note that we could define it directly using the base type Un *)

Definition Sing := [E:Ens](Paire E E).
Transparent Sing.


(* The axioms  *)

Theorem IN_Sing : (E:Ens)(IN E (Sing E)).
Unfold Sing; Auto.
Save.

Theorem IN_Sing_EQ : (E,E':Ens)(IN E (Sing E'))->(EQ E E').
Unfold Sing; Intros E E' H; Elim (Paire_IN E' E' E); Auto.
Save.


Hint IN_Sing IN_Sing_EQ.

Theorem Sing_sound : (A,A':Ens)(EQ A A')->(EQ (Sing A)(Sing A')).
Unfold Sing; Intros; Apply EQ_tran with (Paire A A'); Auto.
Save.

Hint Sing_sound.

Theorem EQ_Sing_EQ : (E1,E2:Ens)(EQ (Sing E1)(Sing E2))->(EQ E1 E2).
Intros; Cut (IN E1 (Sing E2)).
Intros; Auto.
Apply IN_sound_right with (Sing E1); Auto.
Save.

Hint EQ_Sing_EQ.


(* We here need sigma types -- i.e. computational existentials *)

Inductive sig [A:Type;P:A->Prop] : Type := exist : (x:A)(P x)->(sig A P).


(* The set obtained by the comprehension (or separation) axiom *)

Definition Comp : (E:Ens)(P:Ens->Prop)Ens.
Induction E; Intros A f fr P.
Apply (sup {x:A|(P (f x))}).
Induction 1; Intros x p; Exact (f x).
Save.

Transparent Comp.

(* The comprehension/separation axioms *)

Theorem Comp_INC : (E:Ens)(P:Ens->Prop)(INC (Comp E P) E).
Unfold Comp INC; Induction E; Simpl; Intros.
Elim H0; Induction x; Intros; Exists x0; Auto.
Save.

Theorem IN_Comp_P : 
           (E,A:Ens)
               (P:Ens->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
                  (IN A (Comp E P))->(P A).
Induction E; Simpl; Intros B f Hr A P H i; Elim i; Intros c; Elim c; Simpl;
Intros x q e; Apply H with (f x); Auto.
Save.

Theorem IN_P_Comp :
     (E,A:Ens)
        (P:Ens ->Prop)((w1,w2:Ens)(P w1)->(EQ w1 w2)->(P w2))->
                (IN A E)->(P A)->(IN A (Comp E P)).
Induction E; Simpl; Intros B f HR A P H i; Elim i; Simpl; Intros.
Cut (P (f x)).
Intros Pf.
Exists (exist B [x:B](P (f x)) x Pf); Simpl; Auto.
Apply H with A; Auto.
Save.

(* Again, extentionality is not stated, but easy *)


(* Projections of a set: *)
(*  1: its base type     *)

Definition pi1 : Ens -> Type.
Induction 1.
Intros A f r.
Exact A.
Save.

Transparent pi1.

(*  2: the function      *)

Definition pi2 : (E:Ens)(pi1 E)->Ens.
Induction E.
Intros A f r.
Exact f.
Save.

Transparent pi2.

(* The Union set   *)

Definition Union : (E:Ens)Ens.
Induction 1; Intros A f r.
Apply (sup (depprod A [x:A](pi1 (f x)))).
Induction 1; Intros a b.
Exact (pi2 (f a) b).
Save.

Transparent Union.

Theorem EQ_EX : (E,E':Ens)
        (EQ E E')
         ->(a:(pi1 E))
            (EX (pi1 E') [b:(pi1 E')](EQ (pi2 E a) (pi2 E' b))).
Induction E; Intros A f r; Induction E'; Intros A' f' r'; 
        Simpl; Induction 1; Intros e1 e2 a.
Apply e1.
Save.

Transparent EQ_EX.

Theorem IN_EX: (E,E':Ens)(IN E' E)->
                        (EX (pi1 E) [a:(pi1 E)](EQ E' (pi2 E a))).
(Induction E; Simpl).
Intros A f r.
(Induction 1; Simpl).
Intros.
(Exists  x; Auto).
Save.

(* The union axioms *)

Theorem IN_Union : (E,E',E'':Ens)
                (IN E' E)->(IN E'' E')->(IN E'' (Union E)).

(Induction E; Intros A f r).
Intros.
Simpl.
Elim (IN_EX (sup A f) E' H).
Intros x e.
(Cut (EQ (pi2 (sup A f) x) E'); Auto).
Intros e1.
Cut (IN E'' (pi2 (sup A f) x)).
Intros i1.
Elim (IN_EX ? ? i1).
Intros x0 e2.
Simpl in x0.
Exists  (dep_i A [x:A](pi1 (f x)) x x0).
Simpl.
Exact e2.
(Apply IN_sound_right with E'; Auto).
Save.


Theorem IN_INC_Union : (E,E':Ens)(IN E' E)->(INC E' (Union E)).
Unfold INC ; 
        Induction E; Intros A f r; Unfold Union .
Intros E' i E'' i'; Simpl; Elim (IN_EX (sup A f) E' i).
Intros a e; Simpl in a; Simpl in e.
Elim (IN_EX E' E'' i').
Cut (IN E'' (f a)).
Intros i'' a' e''; Elim (IN_EX ? ? i''); Simpl; Intros aa ee.
Exists  (dep_i A [x:A](pi1 (f x)) a aa); Auto.
Apply IN_sound_right with E'; Auto.
Save.

Theorem Union_IN : (E,E':Ens)(IN E' (Union E))->
                                (EX ? [E1:Ens](IN E1 E)/\(IN E' E1)).
(Induction E; Unfold Union ; Simpl; Intros A f r).
Induction 1.
Induction x.
(Intros a b; Simpl).
Intros.
Exists  (f a).
Split.
(Exists  a; Auto).

(Apply IN_sound_left with (pi2 (f a) b); Auto).
Simpl.
(Generalize b ; Elim (f a); Simpl).
Intros.
(Exists  b0; Auto).
Save.


(* extentionality of union  *)

Theorem Union_sound
     : (E,E':Ens)(EQ E E')->(EQ (Union E) (Union E')).
Unfold Union; 
        Induction E; Intros A f r; 
        Induction E'; Intros A' f' r';
        Simpl; Induction 1; Intros e1 e2; Split.
Intros x; Elim x; Intros a aa; Elim (e1 a); Intros a' ea.
Elim (EQ_EX (f a)(f' a') ea aa); Intros aa' eaa.
Exists (dep_i A' [x:A'](pi1 (f' x)) a' aa'); Simpl; Auto.
Intros c'; Elim c'; Intros a' aa'; Elim (e2 a'); Intros a ea.
Cut (EQ (f' a')(f a)).
2 : Auto.
Intros ea'; Elim (EQ_EX (f' a')(f a) ea' aa'); Intros aa eaa.
Exists (dep_i A [x:A](pi1 (f x)) a aa); Auto.

Save.


(* The union construction is monotone w.r.t. inclusion   *)

Theorem Union_mon : (E,E':Ens)(INC E E')->(INC (Union E)(Union E')).
Unfold INC ; Intros E E' IEE E'' IEE''.
Elim (Union_IN E E'' ).
Intros E'''; Induction 1; Intros I1 I2.
Apply IN_Union with E'''; Auto.
Auto.

Save.


(* The  Intersection set   *)

Definition Inter : (E:Ens)Ens:=
[E:Ens]
  Cases E of 
        (sup A f) =>
          (sup ?
               [c:(depprod ? 
                   [a:A](depprod ?
                                [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b)(f x))))]
                Cases c of
                   (dep_i a (dep_i b p)) => (pi2 (f a) b)
                 end)
 end.
           
Transparent Inter.

(* the axioms *)

Theorem IN_Inter_all : (E,E':Ens)
                        (IN E' (Inter E))->
                                (E'':Ens)(IN E'' E)->(IN E' E'').

Induction E; Intros A f r; Simpl; Intros E'.
Induction 1; Intros c; Elim c; Intros a ca; Elim ca; Intros aa paa; Simpl.
Intros e E'' e''.
Elim e''; Intros a1 ea1.
Apply IN_sound_right with (f a1); Auto.
Apply IN_sound_left with (pi2 (f a) aa); Auto.
Save.

Theorem all_IN_Inter : (E,E',E'':Ens)
                         (IN E'' E)->
                            ((E'':Ens)(IN E'' E)->(IN E' E''))->
                                (IN E' (Inter E)).
(Induction E; Intros A f r).
Intros E' E'' i H.
Elim (IN_EX (sup A f) E'' i).
(Intros a e; Simpl in a).
Simpl in e.
(Cut (IN E' E''); Auto).
Intros i'.
(Cut (IN E' (f a)); Auto).
Intros i0.
Elim (IN_EX (f a) E' i0).
Intros b e'.
Simpl.
Cut (x:A)(IN (pi2 (f a) b) (f x)).
Intros.
Exists  (dep_i A
          [a:A]
           (depprod (pi1 (f a))
             [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)))
          a
          (dep_i (pi1 (f a))
            [b:(pi1 (f a))](x:A)(IN (pi2 (f a) b) (f x)) b H0)).
Simpl.
Auto.
Auto.
Intros.
Apply IN_sound_left with E'.
Auto.
Apply H.
Auto.
Simpl.
(Exists  x; Auto).
(Apply IN_sound_right with E''; Auto).
Save.


(*  The powerset and its axioms   *)

Definition Power : Ens->Ens:=
[E:Ens]
 Cases E of
  (sup A f) =>
     (sup ?
          [P:A->Prop]
              (sup ?
                   [c:(depprod A [a:A](P a))]
                       Cases c of
                          (dep_i a p) => (f a)
                        end))
  end.

Transparent Power.


Theorem IN_Power_INC : (E,E':Ens)(IN E' (Power E))->(INC E' E).
Induction E.
Intros A f r; Unfold INC ; Simpl.
Intros E'; Induction 1; Intros P.
Elim E'; Simpl.
Intros A' f' r'.
Induction 1; Intros HA HB.
Intros E''; Induction 1; Intros a' e.
Elim (HA a').
Induction x; Intros a p.
Intros; Exists  a.
Auto.
Apply EQ_tran with (f' a'); Auto.
Save.


Theorem INC_IN_Power : (E,E':Ens)(INC E' E)->(IN E' (Power E)).
(Induction E; Intros A f r; Unfold INC ; Simpl).
(Induction E'; Intros A' f' r' i).
Exists  [a:A](IN (f a) (sup A' f')).
Simpl.
Split.
Intros.
(Elim (i (f' x)); Auto).
Intros a e.
(Cut (EQ (f a) (f' x)); Auto).
Intros e1.
Exists  (dep_i A [a:A](EX A' [y:A'](EQ (f a) (f' y))) a
          (EXi A' [y:A'](EQ (f a) (f' y)) x e1)).
Simpl.
Auto.

Auto.
Simpl.
(Exists  x; Auto).

(Induction y; Simpl).
(Induction 1; Intros).
(Exists  x0; Auto).
Save.

Theorem Power_mon : (E,E':Ens)(INC E E')->(INC (Power E)(Power E')).
Intros.
(Unfold INC ; Intros).
Apply INC_IN_Power.
Cut (INC E0 E).
(Unfold INC ; Unfold INC  in H; Intros; Auto).
Apply IN_Power_INC; Auto.
Save.

Theorem Power_sound : (E,E':Ens)(EQ E E')->(EQ (Power E)(Power E')).
Intros E E' e.
Apply INC_EQ; Unfold INC.
Intros A i.
Cut (INC A E').
Intros; Apply INC_IN_Power; Assumption.
Cut (INC A E); Intros.
Apply INC_sound_right with E; Auto.
Apply IN_Power_INC; Assumption.
Intros A i.
Cut (INC A E).
Intros; Apply INC_IN_Power; Assumption.
Cut (INC A E'); Intros.
Apply INC_sound_right with E'; Auto.
Apply IN_Power_INC; Assumption.
Save.


(* small lemma *)

Theorem not_EQ_Sing_Vide : (E:Ens)(EQ (Sing E) Vide)->F.
Intros E e; Cut False.
Induction 1.
Cut (IN E Vide).
Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
Apply IN_sound_right with (Sing E); Auto.
Save.


Theorem not_EQ_Vide_Sing : (E:Ens)(EQ Vide (Sing E))->F.
Intros E e; Cut False.
Induction 1.
Cut (IN E Vide).
Simpl; Induction 1; Intros xx; Elim xx; Induction 1.
Apply IN_sound_right with (Sing E); Auto.
Save.


(* The cartesian product and its properties *)


(* This definition of the ordered pair is slightly different from *)
(* the usual one, since we want it to work in an intuisionistic   *)
(* setting. Works the same, neitherless. The soundness proofs are *)
(* unpleasant.                                                    *)


Definition Couple := [E,E':Ens](Paire (Sing E) (Paire Vide (Sing E'))).

Theorem Couple_inj_left : (A,A',B,B':Ens)
                (EQ (Couple A A')(Couple B B'))->(EQ A B).
(Unfold Couple ; Simpl).
Induction 1.
(Intros HA HB; Elim (HA true)).
Intros x; Elim x; Simpl; Induction 1; Intros H3 H4; Elim (H3 true); 
 Simpl; Intros xx; Elim xx; Simpl; Auto.
Elim (H4 false); Simpl.
Induction x; Simpl.
Intros.
Cut (EQ (Sing B') Vide).
Simpl.
Induction 1.
Intros yy; Elim (yy true).
Induction x.

(Apply EQ_tran with A; Auto).

Intros;Cut (EQ (Sing B') Vide).
Simpl.
Induction 1.
Intros yy; Elim (yy true).
Induction x.

(Apply EQ_tran with A; Auto).

Intros yy.
Elim (HB true); Simpl.
Induction x.
Change (EQ (Sing A)(Sing B))->(EQ A B); Intros EE.
Apply IN_Sing_EQ.
Apply IN_sound_right with (Sing A); Auto.
Change (EQ (Paire Vide (Sing A'))(Sing B))->(EQ A B).
Intros zz.
Cut F.
Induction 1.
Apply (not_EQ_Sing_Vide A').
Apply EQ_tran with B.
Apply IN_Sing_EQ.
Apply IN_sound_right with (Paire Vide (Sing A')); Auto.
Apply EQ_sym; Apply IN_Sing_EQ; 
        Apply IN_sound_right with (Paire Vide (Sing A')); 
Auto.

Save.


Theorem Couple_inj_right :  (A,A',B,B':Ens)
                (EQ (Couple A A')(Couple B B'))->(EQ A' B').
Unfold Couple; Simpl.
Induction 1; Intros H1 H2.
Elim (H1 false).
Intros bb1; Elim bb1.
Intros HF.
Change (EQ (Paire Vide (Sing A'))(Sing B)) in HF.
Cut F.
Induction 1.
Apply (not_EQ_Vide_Sing A').
Apply EQ_tran with B.
Apply IN_Sing_EQ; Apply IN_sound_right with (Paire Vide (Sing A')); Auto.
Apply EQ_sym; Apply IN_Sing_EQ; 
        Apply IN_sound_right with (Paire Vide (Sing A')); Auto.
Change (EQ (Paire Vide (Sing A'))(Paire Vide (Sing B')))->(EQ A' B').
Intros HP; Cut (EQ (Sing A') (Sing B')).
Intros; Auto.
Cut (IN (Sing A')(Paire Vide (Sing B'))).
Intros HI; Elim (Paire_IN Vide (Sing B')(Sing A') HI).
Intros; Cut F.
Induction 1.
Apply not_EQ_Sing_Vide with A'; Assumption.
Trivial.
Apply IN_sound_right with (Paire Vide (Sing A')); Auto.

Save.


(* Here we cheat. It is easier to define the cartesian product using    *)
(* the type theoretical product, i.e. we here use non set-theoretical   *)
(* constructions. We could however use the usual definitions.           *)


Definition Prod : Ens->Ens->Ens:=
[E,E':Ens]
 Cases E E' of
   (sup A f) (sup A' f')=>
     (sup ?
          [c:(prod_t A A')]
               Cases c of
                 (pair_t a a') => (Couple (f a)(f' a'))
                end)
  end.
Transparent Prod.


Hint Paire_sound_left Paire_sound_right.


Theorem Couple_sound_left :
        (A,A',B:Ens)(EQ A A')->(EQ (Couple A B)(Couple A' B)).
 Unfold Couple;Intros; Auto.
Save.

Theorem Couple_sound_right:
        (A,B,B':Ens)(EQ B B')->(EQ (Couple A B)(Couple A B')).
 Unfold Couple;Intros; Auto.
Save.


Theorem Couple_IN_Prod : (E1,E2,E1',E2':Ens)
                (IN E1' E1)->(IN E2' E2)->
                        (IN (Couple E1' E2')(Prod E1 E2)).
(Induction E1; Intros A1 f1 r1; Induction E2; Intros A2 f2 r2).
Intros E1' E2' i1 i2.
Elim (IN_EX (sup A1 f1) E1').
(Intros x e1; Simpl in x).
Elim (IN_EX (sup A2 f2) E2').
(Intros x0 e2; Simpl in x).
(Apply IN_sound_left with (Couple (pi2 (sup A1 f1) x)
                            (pi2 (sup A2 f2) x0));
 Auto).
(Apply EQ_tran with (Couple (pi2 (sup A1 f1) x) E2'); Auto).
Apply Couple_sound_right.
Auto.

(Apply Couple_sound_left; Auto).

Simpl.
Simpl.
Exists  (pair_t ? ? x x0).
Simpl.
Split.
(Induction x1; Simpl).
(Exists  true; Simpl).
Split.
(Induction x0; Simpl).
(Exists  true; Auto).

(Exists  true; Auto).

(Induction y; Exists  true; Auto).

(Exists  false; Simpl).
Split.
Induction x.
(Exists  true; Simpl; Auto).
Split.
Induction x.

Induction y.

(Exists  false; Auto).

(Induction y; Simpl).
(Exists  true; Auto).

(Exists  false; Auto).

(Induction y; Simpl).
(Exists  true; Auto).

(Exists  false; Auto).

Auto.

Auto.
Save.


Theorem Couple_Prod_IN :  (E1,E2,E1',E2':Ens)
                (IN (Couple E1' E2')(Prod E1 E2))->
                        (IN E1' E1)/\(IN E2' E2).
(Induction E1; Intros A1 f1 r1; Induction E2; Intros A2 f2 r2).
Intros E1' E2' i.
Elim (IN_EX (Prod (sup A1 f1) (sup A2 f2)) (Couple E1' E2') i).
Intros xx; Elim xx; Intros a1 a2 e.
Change (EQ (Couple E1' E2') (Couple (f1 a1) (f2 a2))) in e.
Cut (EQ E1' (f1 a1)).
Cut (EQ E2' (f2 a2)).
Intros e1 e2.
Split.
Apply IN_sound_left with (f1 a1); Auto; Simpl; Exists  a1; Auto.
Apply IN_sound_left with (f2 a2); Auto; Simpl; Exists  a2; Auto.
Apply Couple_inj_right with A:=E1' B:=(f1 a1); Auto.
Apply Couple_inj_left with E2' (f2 a2); Auto.
Save.


Theorem IN_Prod_EX : (E,E',E'':Ens)(IN E'' (Prod E E'))->
        (EX ? [A:Ens](EX ? [B:Ens](EQ (Couple A B) E''))).
(Induction E; Intros A f r; Induction E'; Intros A' f' r').
Intros; Elim (IN_EX (Prod (sup A f) (sup A' f')) E'').
Induction x.
Intros; Exists  (f y); Exists  (f' y0); Auto.
Auto.
Save.


(* Ordinals *)

Definition Succ := [E:Ens](Union (Paire E (Sing E))).
Transparent Succ.


Inductive Ord : Ens -> Prop :=
  Oo : (Ord Vide)
| So : (E:Ens)(Ord E)->(Ord (Succ E))
| Lo : (E:Ens)((e:Ens)(IN e E)->(Ord e))->(Ord (Union E))
| Eo : (E,E':Ens)(Ord E)->(EQ E E')->(Ord E').

Hint Oo So Lo.

Definition Nat : nat ->Ens.
Induction 1; Intros.
Exact Vide.
Exact (Succ X).
Save.
Transparent Nat.

Theorem Nat_Ord : (n:nat)(Ord (Nat n)).
Induction n; Simpl; Auto.
Save.

Definition Omega : Ens :=
  (sup nat Nat).

Theorem IN_Succ :  (E:Ens)(IN E (Succ E)).
Intros E; Unfold Succ; Unfold Sing; Apply IN_Union with (Paire E E); Auto.
Save.


Theorem INC_Succ : (E:Ens)(INC E (Succ E)).
(Unfold INC ; Unfold Succ ).
Intros.
(Apply IN_Union with E; Auto).
Save.

Hint IN_Succ INC_Succ.


Theorem IN_Succ_or : (E,E':Ens)(IN E' (Succ E))->(EQ E E')\/(IN E' E).
Intros E E' i.
Unfold Succ  in i.
Elim (Union_IN (Paire E (Sing E)) E' i).
Intros E1; Induction 1; Intros i1 i2.
Elim (Paire_IN E (Sing E) E1 i1).
Intros; Right; Apply IN_sound_right with E1; Auto.
Intros; Left; Cut (IN E' (Sing E)).
Auto.
Apply IN_sound_right with E1; Auto.

Save.


Theorem E_not_IN_E : (E:Ens)(IN E E)->F.
Induction E; Intros A f r i.
Cut False.
Induction 1.
Elim (IN_EX (sup A f) (sup A f) i); Intros a e.

Simpl in a.
Change (EQ (sup A f) (f a)) in e.
Elim (r a).
Apply IN_sound_right with (sup A f); Auto.
Exists a; Auto.
Save.


Theorem Nat_IN_Omega : (n:nat)(IN (Nat n) Omega).
Intros; Simpl; Exists n; Auto.
Save.
Hint Nat_IN_Omega.


Theorem IN_Omega_EX : (E:Ens)(IN E Omega)->(EX ? [n:nat](EQ (Nat n) E)).
(Simpl; Induction 1).
Intros n e.
(Exists  n; Auto).
Save.

Theorem IN_Nat_EX : (n:nat)(E:Ens)(IN E (Nat n))->(EX ? [p:nat](EQ E (Nat p))).
Induction n.
Simpl.
Induction 1.
Induction x.

Intros.
Change (IN E (Succ (Nat n0))) in H0.
Elim (IN_Succ_or (Nat n0) E H0).
(Intros; Exists  n0).
Auto.

Intros.
(Elim (H E); Auto).
Save.


Theorem Omega_EQ_Union : (EQ Omega (Union Omega)).
(Apply INC_EQ; Unfold INC ).
Intros.
(Elim (IN_Omega_EX E H); Intros n e).
Apply IN_Union with (Nat (S n)).
Auto.

Apply IN_sound_left with (Nat n).
Auto.

Auto.
(Change (IN (Nat n) (Succ (Nat n))); Auto).

Intros.
Elim (Union_IN Omega E H).
Intros e h.
Elim h.
Intros i1 i2.
Elim (IN_Omega_EX e i1).
Intros n e1.
Cut (IN E (Nat n)).
Intros.
(Elim (IN_Nat_EX n E H0); Intros).
(Apply IN_sound_left with (Nat x); Auto).

(Apply IN_sound_right with e; Auto).
Save.


Theorem Omega_Ord : (Ord Omega).

Apply Eo with (Union Omega).
Apply Lo.
Intros.
Elim (IN_Omega_EX e H).
Intros n ee.
Apply Eo with (Nat n); Auto.
Elim n.
Auto.
Auto.
Intros.
Change (Ord (Succ (Nat n0))); Auto.
Apply EQ_sym; Auto.
Apply Omega_EQ_Union.

Save.


Definition Alpha : (E:Ens)Ens.
(Induction E; Intros A f r).
Apply Union.
Apply (sup A).
Intros a.
Exact (Power (r a)).

Save.
Transparent Alpha.


(* A Type-theoretical axiom of choice gives us the collection axiom  *)


Definition collection :=
 (P:Ens->Ens->Prop)
  ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
   ((E:Ens)(EX ? (P E)))->
       (E:Ens)(EX ? [A:Ens](x:Ens)(IN x E)->(EX ? [y:Ens](IN y A)/\(P x y))).


Definition choice := 
 (A,B:Type)(P:A->B->Prop)
   ((a:A)(EX ? [b:B](P a b)))->
       (EX ? [f:A->B]((a:A)(P a (f a)))).


Theorem Choice_Collection : choice -> collection.
Unfold collection; Intro; Intros P comp G E.
Cut (EX ? [f:Ens->Ens](B:Ens)(P B (f B))).
Induction 1; Intros f pf.
Elim E; Intros A g hr; Intros.
Exists (sup A [a:A](f (g a))).
Simpl; Intros X i.
Elim i; Intros a ea.
Exists (f (g a)).
Split.
Exists a; Auto.
Apply comp with (g a); Auto.
Unfold choice in H.
Apply H; Intros.
Elim (G a); Intros b hb; Exists b; Auto.
Save.


(* If we also assume the excluded middle, we can derive         *)
(* the usual replacement schemata.                              *)

Definition functional :=
        [P:Ens->Ens->Prop](x,y,y':Ens)
                (P x y)->(P x y')->(EQ y y').

Definition replacement :=
   (P:Ens->Ens->Prop)
        (functional P)->
        ((x,y,y':Ens)(EQ y y')->(P x y)->(P x y'))->
        ((x,x',y:Ens)(EQ x x')->(P x y)->(P x' y))->
       (X:Ens)(EX ? [Y:Ens](y:Ens)
                            (((IN y Y)->(EX ? [x:Ens](IN x X)/\(P x y)))
                            /\((EX ? [x:Ens](IN x X)/\(P x y))->(IN y Y)))).


Theorem classical_Collection_Replacement : 
 ((S:Prop)S\/(S->False))->
        collection ->
                replacement.

Unfold replacement; Intros EM Collection P fp comp_r comp_l X.
Cut (EX ? [Y:Ens](y:Ens)((EX ? [x:Ens](IN x X)/\(P x y))->(IN y Y))).
Induction 1; Intros Y HY.
Exists (Comp Y [y:Ens](EX ? [x:Ens](IN x X)/\(P x y))).
Intros y; Split.
Intros HC.
Apply (IN_Comp_P Y y [y0:Ens](EX Ens [x:Ens](IN x X)/\(P x y0))); Auto.
Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
Exists x; Split; Auto.
Apply comp_r with w1; Auto.
Intros He.
Apply IN_P_Comp.

Intros w1 w2; Induction 1; Intros x; Induction 1; Intros Ix Px e.
Exists x; Split; Auto.
Apply comp_r with w1; Auto.
Apply HY; Auto.
Auto.

Elim (Collection [x,y:Ens]((P x y)\/(((y':Ens)(P x y')->False)/\(EQ y Vide)))) 
        with X.
Intros Y HY.
Elim (EM (EX ? [x:Ens](IN x X)/\(P x Vide))).
Intros Hvide; Elim Hvide; Intros xv Hxv; Exists Y.
Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
Elim (HY x Hx1).
Intros y'; Induction 1; Intros Hy'1 Hy'2.
Elim Hy'2.
Intros Hy'3; Apply IN_sound_left with y'; Auto.
Apply fp with x; Auto.
Induction 1; Intros Hy'3 Hy'4.
Elim (Hy'3 y Hx2).
Intros HP; Exists (Comp Y [y:Ens]((EQ y Vide)->False)).
Intros y; Induction 1; Intros x; Induction 1; Intros Hx1 Hx2.
Apply IN_P_Comp.
Intros w1 w2 Hw1 Hw Hw2; Apply Hw1; Apply EQ_tran with w2; Auto.
Elim (HY x).
Intros y'; Induction 1; Intros Hy'1 Hy'2.
Elim Hy'2; Intros Hy'3.
Apply IN_sound_left with y'; Auto.
Apply fp with x; Auto.
Elim Hy'3; Intros Hy'4 Hy'5.
Elim (Hy'4 y); Auto.
Assumption.
Intros e; Apply HP; Exists x; Split; Auto; 
        Apply comp_r with y; Auto; Apply fp; Auto.
Intros x x' y e Hx; Elim Hx; Intros Hx1.
Left; Apply comp_l with x; Auto.
Right; Elim Hx1; Intros Hx2 Hx3; Split.
2 : Assumption.
Intros y' Hy'; Apply (Hx2 y'); Apply comp_l with x'; Auto.
Intros x; Elim (EM (EX ? [y:Ens](P x y))); Intros Hx.
Elim Hx; Intros x0 Hx0; Exists x0; Left; Assumption.
Exists Vide; Right; Split; Auto.
Intros y Hy; Elim Hx; Exists y; Auto.
Save.


(* Peter Aczel's Encoding of CZF *)

(* Using the same definition "Ens" of sets, we can developp Peter Aczel's   *)
(* encoding of "Constructive Type Theory" (CZF).                            *)
(* It is basically a simillar developement, but this time, the propositions *)
(* are objects of type "Type", i.e. are on the same level (resp. above) the *)
(* sets. The advantage is that we can extract the constructive witness of an*)
(* existential proof. The drawbacks are:                                    *)
(*  - no definition of the powerset                                         *)
(*  - complicated difference between bounded and unbounded quantification   *)
(*  - excluded middle is now much more "dangerous"                          *)


Definition EQC : Ens -> Ens -> Type.
Induction 1; Intros A f eq1.
Induction 1; Intros B g eq2.
Apply prod_t.
Exact (x:A)
        (depprod ? [y:B](eq1 x (g y))).
Exact (y:B)
        (depprod ? [x:A](eq1 x (g y))).
Save.
Transparent EQC.


(* APPARTENANCE *)

Definition CIN: Ens -> Ens -> Type.
Induction 2.
Intros.
Exact (depprod ? [y:A](EQC X (e y))).
Save.
Transparent CIN.


(* INCLUSION *)

Definition CINC : Ens -> Ens -> Type.
Intros E1 E2.
Exact (E:Ens)(CIN E E1)->(CIN E E2).
Save.
Transparent CINC.


(* EQ EST UNE RELATION D'EQUIVALENCE *)

Theorem EQC_refl : (E:Ens)(EQC E E).
Induction E.
Intros A f HR.
Simpl.
(Split; Intros).
(Exists  x; Auto).

(Exists  y; Auto).
Save.

Theorem EQC_tran : (E1,E2,E3:Ens)(EQC E1 E2)->(EQC E2 E3)->(EQC E1 E3).
Induction E1; Induction E2; Induction E3; Simpl; Intros.
Split; (Elim X2;Intros;Elim X3;Intros).
Elim (y x); Intros.
Elim (y1 x0); Intros.
Exists x1.
Apply X with (e0 x0); Auto.
Elim (y3 y1); Intros.
Elim (y0 x); Intros.
Exists x0.
Apply X with (e0 x); Auto.
Save.

Theorem EQC_sym : (E1,E2:Ens)(EQC E1 E2)->(EQC E2 E1).
Induction E1; Induction E2; Simpl; Intros.
Elim X1; Intros; Split; Intros.
Elim (y0 x); Intros.
Exists x0; Auto.
Elim (y y1); Intros; Exists x; Auto.
Save.

Theorem EQC_INC : (E,E':Ens)(EQC E E')->(CINC E E').
Induction E; Induction E'; Simpl; Intros; Unfold CINC; Simpl.
Elim X1; Intros.
Elim X2; Intros.
Elim (y x); Intros.
Exists x0; Apply EQC_tran with (e x); Auto.
Save.

Hint EQC_sym EQC_refl EQC_INC.

Theorem CINC_EQC : (E,E':Ens)(CINC E E')->(CINC E' E)->(EQC E E').
Induction E; Induction E'; Unfold CINC; Simpl; Intros; Split; Intros.
Apply X1.
Exists x; Auto.
Cut (depprod A [x:A](EQC (e0 y)(e x))); 
        Try (Induction 1; Intros x p; Exists x; Auto).
Apply X2; Exists y; Auto.
Save.

Hint CINC_EQC.


Theorem CIN_sound_left : 
                (E,E',E'':Ens)
                  (EQC E E')->(CIN E E'')->(CIN E' E'').
Induction E''; Simpl; Intros.
Elim X1; Intros y p; Exists y.
Apply EQC_tran with E; Auto.
Save.

Theorem CIN_sound_right :
                (E,E',E'':Ens)
                   (EQC E' E'')->(CIN E E')->(CIN E E'').
Induction E'; Induction E''; Simpl; Intros.
Elim X1; Intros Xl Xr; Elim X2; Intros y p; Elim (Xl y); Intros y0 p0;
Exists y0; Apply EQC_tran with (e y); Auto.
Save.

Theorem CINC_refl : (E:Ens)(CINC E E).
Unfold CINC; Auto.
Save.

Theorem CINC_tran : (E,E',E'':Ens)(CINC E E')->(CINC E' E'')->(CINC E E'').
Unfold CINC; Auto.
Save.


Theorem CINC_sound_left :
               (E,E',E'':Ens)
                  (EQC E E')->(CINC E E'')->(CINC E' E'').
Induction E''; Unfold CINC; Simpl; Intros A f XR e X1 E0 i; Apply X1.
Apply CIN_sound_right with E'; Auto.
Save.

Theorem CINC_sound_right :                
               (E,E',E'':Ens)
                 (EQC E' E'')->(CINC E E')->(CINC E E'').
Induction E'; Induction E''; Unfold CINC; Simpl; Intros.
Elim (X2 E0); Try Assumption; Intros.
Elim X1; Intros XA XB; Elim (XA x); Intros.
Exists x0; Apply EQC_tran with (e x); Auto.
Save.


Theorem tout_vide_est_VideC : (E:Ens)((E':Ens)(CIN E' E)->F)->(EQC E Vide).
 Unfold Vide; Induction E; Simpl; Intros; Split.
Intros; Elim (H (e x)); Auto.
Exists x; Auto.
Induction y.
Save.


Theorem Paire_sound_leftC : (A,A',B:Ens)
                        (EQC A A')->(EQC (Paire A B)(Paire A' B)).
Unfold Paire .
Simpl.
(Intros; Split).
Induction x.
(Exists  true; Auto).

(Exists  false; Auto).

(Induction y; Simpl).
(Exists  true; Auto).

(Exists  false; Auto).
Save.

Theorem Paire_sound_rightC : (A,B,B':Ens)
                (EQC B B')->(EQC (Paire A B)(Paire A B')).
Unfold Paire; Simpl; Intros; Split.
Induction x.
(Exists true; Auto).
Exists false; Auto.
Induction y.
(Exists true; Auto).
Exists false; Auto.
Save.


Theorem CIN_Paire_left : (E,E':Ens)(CIN E (Paire E E')).
Unfold Paire; Simpl; Exists true; Simpl; Auto.
Save.

Theorem CIN_Paire_right : (E,E':Ens)(CIN E' (Paire E E')).
Unfold Paire; Simpl; Exists false; Simpl; Auto.
Save.

Inductive sum_t [A,B:Type] : Type := 
    inl_t : A->(sum_t A B) | inr_t : B->(sum_t A B).
Hint inl_t inr_t.

Theorem Paire_CIN : (E,E',A:Ens)(CIN A (Paire E E'))->
                                        (sum_t(EQC A E)(EQC A E')).
Unfold Paire; Simpl; Induction 1; Intros b; Elim b; Simpl; Auto.
Save.

Hint CIN_Paire_left CIN_Paire_right.

(* Singleton *)

Theorem CIN_Sing : (E:Ens)(CIN E (Sing E)).
Unfold Sing; Auto.
Save.

Theorem CIN_Sing_EQ : (E,E':Ens)(CIN E (Sing E'))->(EQC E E').
Unfold Sing; Intros E E' H; Elim (Paire_CIN E' E' E); Auto.
Save.


Theorem EQC_EQ : (E,E':Ens)(EQC E E')->(EQ E E').
Induction E ; Intros A f ra ; Induction E'; Intros B g rb; Simpl; 
        Induction 1; Intros H1 H2; Split.
Intros a; Elim (H1 a); Intros b; Intros; Exists b; Auto.
Intros b; Elim (H2 b); Intros a; Intros; Exists a; Auto.
Save.


Theorem CIN_IN : (E,E':Ens)(CIN E E')->(IN E E').
Induction E ; Intros A f ra ; Induction E'; Intros B g rb; 
                Induction 1; Intros a; Unfold IN; Exists a; Auto.
Apply EQC_EQ; Auto.
Save.


Theorem EQC_EX : (E,E':Ens)
        (EQC E E')
         ->(a:(pi1 E))
            (depprod (pi1 E') [b:(pi1 E')](EQC (pi2 E a) (pi2 E' b))).
(Induction E; Induction E'; Simpl).
Intros.
(Elim X1; Intros).
(Elim (y a); Intros).
(Exists  x; Auto).

Save.

Transparent EQC_EX.

Theorem CIN_EX: (E,E':Ens)(CIN E' E)->
                        (depprod (pi1 E) [a:(pi1 E)](EQC E' (pi2 E a))).
(Induction E; Simpl).
Intros A f r.
(Induction 1; Simpl).
Intros.
(Exists  x; Auto).
Save.

Theorem CIN_Union : (E,E',E'':Ens)
                (CIN E' E)->(CIN E'' E')->(CIN E'' (Union E)).

(Induction E; Intros A f r).
Intros.
Simpl.
Elim (CIN_EX (sup A f) E' X).
Intros x e.
(Cut (EQC (pi2 (sup A f) x) E'); Auto).
Intros e1.
Cut (CIN E'' (pi2 (sup A f) x)).
Intros i1.
Elim (CIN_EX ? ? i1).
Intros x0 e2.
Simpl in x0.
Exists  (dep_i A [x:A](pi1 (f x)) x x0).
Simpl.
Exact e2.
(Apply CIN_sound_right with E'; Auto).
Save.


Theorem CIN_CINC_Union : (E,E':Ens)(CIN E' E)->(CINC E' (Union E)).
(Unfold CINC ; Induction E; Intros A f r).
Unfold Union .
Intros.
Simpl.
Elim (CIN_EX (sup A f) E' X).
Intro.
Simpl in x.
Intros.
Simpl in y.
Elim (CIN_EX E' E0 X0).
Cut (CIN E0 (f x)).
Intros.
Elim (CIN_EX ? ? X1).
Simpl.
Intros.
(Exists  (dep_i A [x:A](pi1 (f x)) x x1); Auto).

(Apply CIN_sound_right with E'; Auto).
Save.

(* idem depprod *)

Inductive depprod' [A:Type;P:A->Type] : Type := 
    dep_i' : (x:A)(P x)->(depprod' A P).

Theorem Union_CIN : (E,E':Ens)(CIN E' (Union E))->
                                (depprod' ? 
                                    [E1:Ens](prod_t (CIN E1 E)(CIN E' E1))).
(Induction E; Unfold Union ; Simpl; Intros A f r).
Induction 1.
Induction x.
(Intros a b; Simpl).
Intros.
Exists  (f a).
Split.
(Exists  a; Auto).

(Apply CIN_sound_left with (pi2 (f a) b); Auto).
Simpl.
(Generalize b ; Elim (f a); Simpl).
Intros.
(Exists  b0; Auto).
Save.


Theorem Union_soundC
     : (E,E':Ens)(EQC E E')->(EQC (Union E) (Union E')).
Unfold Union .
Simpl.
(Induction E; Intros A f r; Induction E'; Intros A' f' r').
Simpl.
Intros.
(Elim X; Intros).
Split.
Induction x.
Intros.
Elim (y x0).
Intros.
Elim (EQC_EX (f x0) (f' x1) y2 y1).
Intros.
Exists  (dep_i A' [x:A'](pi1 (f' x)) x1 x2).
Simpl.
Auto.

(Induction y; Intros).
(Elim (y0 x); Intros).
(Cut (EQC (f' x) (f x0)); Auto).
Intros e.
(Elim (EQC_EX (f' x) (f x0) e y2); Intros).
Exists  (dep_i A [x0:A](pi1 (f x0)) x0 x1).
(Simpl; Auto).
Save.

Theorem Union_monC : (E,E':Ens)(CINC E E')->(CINC (Union E)(Union E')).
(Unfold CINC ; Intros).
(Elim (Union_CIN E E0 X0); Intros).
Apply CIN_Union with x; Elim y; Intros; Auto.
Save.


(* surprinsingly, the predicative and impredicative definitions of the   *)
(* intersection do not seem equivalent.                                  *)
(* to be checked...                                                      *)


(* This is a step towards inaccessible cardinals                *)
(* We can define "small" sets, using the Type's hierarchy       *)
(* Since Coq does not support universe polymorphism, we need    *)
(* to duplicate some definitions here.                          *)


(* The small sets  *)

Inductive Ens' : Type :=
 sup' : (A:Type)(A->Ens')->Ens'.

(* Existential quantification *)

Inductive EX' [P:Type; Q:P->Prop]: Prop :=
 EXi : (x:P)(Q x)->(EX' P Q).

(* Cartesian product in Type *)

Inductive prod_t' [A,B:Type] : Type :=
 pair_t : A->B->(prod_t' A B).


(* Existential on the Type level *)

Inductive depprod'' [A:Type; P : A->Type] : Type :=
 dep_i'' : (x:A)(P x)->(depprod'' A P).


(* Recursive Definition of the extentional equality on sets *)

Definition EQ' : Ens' -> Ens' -> Prop.
Induction 1; Intros A f eq1.
Induction 1; Intros B g eq2.
Apply and.
Exact (x:A)
        (EX' ? [y:B](eq1 x (g y))).
Exact (y:B)
        (EX' ? [x:A](eq1 x (g y))).
Save.

Transparent EQ'.


(* small sets can be injected into big sets             *)

Definition inj : Ens'->Ens.
Induction 1; Intros A f fr.
Exact (sup A fr).
Save.
Transparent inj.

Theorem inj_sound : (E1,E2:Ens')(EQ' E1 E2)->(EQ (inj E1)(inj E2)).
(Induction E1; Intros A1 f1 fr1; Induction E2; Intros A2 f2 r2; Simpl).
(Induction 1; Intros HR1 HR2; Split).
(Intros a1; Elim (HR1 a1); Intros a2 Ha2; Exists  a2; Auto).
(Intros a2; Elim (HR2 a2); Intros a1 Ha1; Exists  a1; Auto).
Save.


Definition Power' : Ens'->Ens':=
[E:Ens']
 Cases E of
  (sup' A f) =>
     (sup' ?
          [P:A->Prop]
              (sup' ?
                   [c:(depprod'' A [a:A](P a))]
                       Cases c of
                          (dep_i'' a p) => (f a)
                        end))
  end.

Transparent Power'.


Theorem Power_sound_inj : (E:Ens')(EQ (inj (Power' E))(Power (inj E))).
Induction E; Intros A f HR.
Simpl; Split.
Intros P; Exists P; Split.
Intros c; Elim c; Intros a p.
Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto.
Intros c; Elim c; Intros a p.
Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto.
Intros P; Exists P; Split.
Intros c; Elim c; Intros a p.
Exists (dep_i A [a0:A](P a0) a p); Simpl; Auto.
Intros c; Elim c; Intros a p.
Exists (dep_i'' A [a0:A](P a0) a p); Simpl; Auto.
Save.


(* The set of small sets                        *)

Definition Big := (sup Ens' inj).

Theorem Big_is_big : (E:Ens')(IN (inj E) Big).
Intros E; Unfold Big; Simpl; Exists E; Auto.
Save.

Theorem IN_Big_small : (E:Ens)(IN E Big)->(EX' ? [E':Ens'](EQ E (inj E'))).
Unfold Big; Simpl; Induction 1; Intros E' HE'; Exists E'; Auto.
Save.


Theorem IN_small_small : (E:Ens)(E':Ens')(IN E (inj E'))->
                (EX' ? [E1:Ens'](EQ E (inj E1))).
Induction E'; Intros A' f' HR'; Simpl; 
        Induction 1; Intros a' e'; Exists  (f' a'); Auto.
Save.


Theorem Big_closed_for_power : (E:Ens)(IN E Big)->(IN (Power E) Big).
Unfold Big; Simpl; Intros E; Induction 1; Intros E' HE'; Exists (Power' E').
Apply EQ_tran with (Power (inj E')).
Apply Power_sound; Assumption.
Apply EQ_sym; Apply Power_sound_inj.
Save.


(* Just for fun : a proof that there is no set of all sets, using       *)
(* Russell's paradox construction                                       *)
(* There, of course, are other proofs (foundation, etc)                 *)

Theorem Russell : (E:Ens)((E':Ens)(IN E' E))->False.
Intros U HU.
Cut ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
Intros HR.
Apply HR.
(Apply IN_P_Comp; Auto).
(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto;
 Apply IN_sound_right with w2; Auto).
Intros H.
Cut (IN (Comp U [x:Ens](IN x x)->False) (Comp U [x:Ens](IN x x)->False)).
Change ([x:Ens](IN x x)->False (Comp U [x:Ens](IN x x)->False)).
Cut (w1,w2:Ens)((IN w1 w1)->False)->(EQ w1 w2)->(IN w2 w2)->False.
Intros ww.
Exact (IN_Comp_P U (Comp U [x:Ens](IN x x)->False)
        [x:Ens](IN x x)->False ww H).
(Intros w1 w2 HF e i; Apply HF; Apply IN_sound_left with w2; Auto;
 Apply IN_sound_right with w2; Auto).
Assumption.

Save.