Require Export Arith.
Require Export ZArith.

Set Implicit Arguments.

(************************ PARAMETERS AND AXIOMS ************************)

(*** interpret types as being classical sets ***)
Definition E := Type.

(*** elements of a set are themselves sets ***)
(***) Parameter R : (x:E)x -> E.  
(***) Axiom R_inj : (x:E; a,b:x)(R a) == (R b) -> a == b.

Definition inc := [x,y:E](exT ? [a:y](R a) == x).

Definition sub := [a,b:E](x:E)(inc x a) -> (inc x b).


(*** a set is determined by its elements ****)
(***) Axiom extensionality : (a,b:E)(sub a b) -> (sub b a) -> a == b.


Inductive nonemptyT [t:Type] : Prop := 
nonemptyT_intro : t -> (nonemptyT t).

(*** the axiom of choice on the type level *********************
WARNING: !!!!!!!!!!! this version of choice is contradictory with 
the impredicativity of Set; when using things like nat : Set, be careful
not to invoke the impredicativity of Set !!!!!!!!!!!!!! *********)
(***) Parameter chooseT :(t:Type; p: t-> Prop)(nonemptyT t) -> t.
(***) Axiom chooseT_pr : (t:Type; p: t-> Prop; ne: (nonemptyT t))
(exT ? p)-> (p (chooseT p ne)).


(*** the replacement axiom: images of a set are again sets *********)
(***) Parameter IM : (x:E)(x -> E) -> E.
(***) Axiom IM_exists : (x:E; f:x -> E; y:E)(inc y (IM f)) -> (exT ? [a:x](f a) == y).
(***) Axiom IM_inc : (x:E; f:x -> E; y:E)(exT ? [a:x](f a) == y) ->
(inc y (IM f)). 

(*** the following actually follow from the above as was shown in the
standard library but we write them as axioms for brevity **************)
(***) Axiom excluded_middle : (P:Prop)(not (not P)) -> P.
(***) Axiom proof_irrelevance : (P:Prop; q,p:P)p==q.

(********* END OF PARAMETERS AND AXIOMS *********************************************)

Definition neq := [x,y:E]~(x == y).




Lemma sub_trans : (a,b,c:E)(sub a b) -> (sub b c) -> (sub a c).
Unfold sub. EAuto. Save. 



Lemma inc_nonempty : (x,y:E)(inc x y) -> (nonemptyT y).
Intros. Unfold inc in H. NewInduction H. Apply nonemptyT_intro. Assumption.
Save.

Lemma R_inc : (x:E; a:x)(inc (R a) x).
Intros. Unfold inc. EApply exT_intro with a. Trivial.
Save.

Definition B := [x,y:E; hyp : (inc x y)]
(chooseT [a:y](R a) == x (inc_nonempty hyp)).

Lemma B_eq : (x,y:E; hyp : (inc x y))(R (B hyp)) == x.
Intros. Unfold B.
Pose (chooseT_pr 2![a:y](R a) == x).
Apply e. Assumption.
Save.

Definition empty := [x:E](y:E)~(inc y x). 

Lemma nonemptyT_not_empty : (x:E)(nonemptyT x) -> ~(empty x).
Intros. NewInduction H. Unfold not. Unfold empty. Intros. Unfold not in H.
Apply H with (R X). Apply R_inc. Save. 



Lemma not_empty_nonemptyT : (x:E)~(empty x) -> (nonemptyT x).
Intros. Apply excluded_middle. Unfold  not. Intros. Unfold not in H. 
Apply H. Unfold empty. Unfold not. Intros. Apply H0. Apply nonemptyT_intro. 
Exact (B H1). Save. 

Inductive nonempty : E -> Prop := 
nonempty_intro : (x,y:E)(inc y x) -> (nonempty x).

Inductive emptyset : E := .

Lemma emptyset_empty : (x:E)~(inc x emptyset).
Unfold not. Intros.
Pose (B H).
Elim e.
Save.



Syntactic Definition E1 := E -> E.
Syntactic Definition E2 := E -> E1.
Syntactic Definition E3 := E -> E2.
Syntactic Definition E4 := E -> E3.
Syntactic Definition E5 := E -> E4.
Syntactic Definition E6 := E -> E5.
(** thus for example E3 = E -> E -> E -> E **)

Syntactic Definition EP := E -> Prop.
Syntactic Definition E2P := E -> EP.
Syntactic Definition E3P := E -> E2P.
Syntactic Definition E4P := E -> E3P.


Definition A := and.


Recursive Tactic Definition Deconj :=
Match Context With
[|- (A ?  ?)] -> Unfold A; Apply conj; [Idtac |Deconj]
|
[|- (and ?  ?)] -> Apply conj; [Idtac |Deconj]
|
[|-  ? /\ ?] -> Apply conj; [Idtac |Deconj]

|
[|- ?]  -> Idtac.

Tactic Definition UnfoldDeconj d := (Unfold d); Deconj.






Recursive Tactic Definition Expand := 
Match Context With 
[id1 : (A ?1 ?2) |- ?] -> (Unfold A in id1); NewInduction id1; Expand
|
[id1 : (and ?1 ?2) |- ?] -> NewInduction id1; Expand
|
[id1 : (?1 /\ ?2) |- ?] -> NewInduction id1; Expand
|
[|- ?] -> Idtac.



(*** we write a tactic which is like Pose but which is anonymous ***)
Tactic Definition Recall u := 
Pose recalx := u;
Match Context With
[recalx : ?1 |- ? ] -> (Assert ?1; [Exact recalx | Clear recalx]).


Definition strict_sub := [a,b:E]
(A (neq a b)
   (sub a b)
).

Lemma strict_sub_trans1 : (a,b,c:E)(strict_sub a b) -> (sub b c) -> 
(strict_sub a c).
Unfold strict_sub. Unfold neq. Unfold not. Intros. 
Deconj. Expand. Intros. Apply H. Apply extensionality. 
Assumption. Rewrite H2. Assumption. Expand. 
Apply sub_trans with b; Auto. Save. 



Lemma strict_sub_trans2 : (a,b,c:E)(sub a b) -> (strict_sub b c) -> 
(strict_sub a c).
Unfold strict_sub. Unfold neq. Unfold not. Intros. 
Deconj. Expand. Intros. Apply H0. Apply extensionality. 
Assumption. Rewrite <- H2. Assumption. Expand. 
Apply sub_trans with b; Auto. Save. 




Inductive exists [p:E -> Prop]: Prop :=
exists_intro : (x:E)(p x) -> (exists p).
Definition exists_unique := [p:E->Prop]
(A (exists p)
   (x,y:E)(p x) -> (p y) -> x == y
).

Lemma exT_exists : (p:E-> Prop)(exT ? [x:E](p x)) -> (exists p).
Intros.
NewInduction H.
Pose exists_intro.
EAuto.
Save.




Lemma p_or_not_p : (P:Prop)P \/ (not P).
Intros.
EApply excluded_middle.
Unfold not.
Intros.
Assert P; Apply excluded_middle; Unfold not; Auto.
Save.




Definition choose : (E -> Prop) -> E.
Intros.
EApply chooseT.
Assumption.
EApply nonemptyT_intro.
Exact Prop.
Defined.


Lemma choose_pr : (p:E -> Prop)(exists p) -> (p (choose p)).
Intros.
Unfold choose.
EApply chooseT_pr.
NewInduction H.
Apply exT_intro with x.
Assumption.
Save.


Definition rep := [x:E](choose [y:E](inc y x)). 

Lemma nonempty_rep : (x:E)(nonempty x) -> (inc (rep x) x). 
Intros. NewInduction H. Unfold rep. Apply choose_pr.
Apply exists_intro with y. 
Assumption. Save. 





Definition by_cases_pr:= [T:Type; P:Prop; a:P -> T; b:(not P) -> T; x:T]
(A (p:P)(a p) == x
   (q:(not P))(b q) == x
).

Lemma by_cases_exists : (T:Type; P:Prop; a:P -> T; b:(not P) -> T)
(exT ? [x:T](by_cases_pr a b x)).
Intros. Assert (P \/ (not P)). Apply p_or_not_p. NewInduction H.
EApply exT_intro with (a H). Unfold by_cases_pr. Deconj.
Intros. Assert H==p. Apply proof_irrelevance. Rewrite H0. Trivial.
Intros. Pose (q H). Elim f.
EApply exT_intro with (b H). Unfold by_cases_pr. Deconj.
Intros. Pose (H p). Elim f.
Intros. Assert H == q. Apply proof_irrelevance. Rewrite H0. Trivial.
Save.

Lemma by_cases_nonempty : (T:Type; P:Prop; a:P -> T; b:(not P) -> T)
(nonemptyT T).
Intros.
Intros. Assert (P \/ (not P)). Apply p_or_not_p. NewInduction H.
EApply nonemptyT_intro. Exact (a H).
EApply nonemptyT_intro. Exact (b H).
Save.



Definition by_cases := [T:Type; P:Prop; a:P -> T; b:(not P) -> T]
(chooseT [x:T](by_cases_pr a b x) (by_cases_nonempty a b)).


Lemma by_cases_property : (T:Type; P:Prop; a:P -> T; b:(not P) -> T)
(by_cases_pr a b (by_cases a b)).
Intros.
Recall '(by_cases_exists a b).
Recall '(by_cases_nonempty a b).
Recall '(chooseT_pr H0 H).
Unfold by_cases.
Assert (by_cases_nonempty a b) == H0.
Apply proof_irrelevance.
Rewrite H2.
Assumption.
Save.

Lemma by_cases_unique : (T:Type; P:Prop; a:P -> T; b:(not P) -> T; x:T)
(by_cases_pr a b x) -> (by_cases a b) == x.
Intros.
Recall '(by_cases_property a b).
Intros. Assert (P \/ (not P)). Apply p_or_not_p. NewInduction H1.
Unfold by_cases_pr in H.  Unfold by_cases_pr in H0.  Expand.
Transitivity (a H1). Symmetry. Auto. Auto.
Unfold by_cases_pr in H.  Unfold by_cases_pr in H0.  Expand.
Transitivity (b H1). Symmetry. Auto. Auto.
Save.


Lemma by_cases_if  : (T:Type; P:Prop; a:P -> T; b:(not P) -> T; p:P)
(by_cases a b) == (a p).
Intros. EApply by_cases_unique.
Unfold by_cases_pr. Deconj.
Intros. Assert p == p0. Apply proof_irrelevance. Rewrite H. Trivial.
Intros. Recall '(q p). Elim H.
Save.



Lemma by_cases_if_not :  (T:Type; P:Prop; a:P -> T; b:(not P) -> T; q : (not P))
(by_cases a b) == (b q).
Intros. EApply by_cases_unique.
Unfold by_cases_pr. Deconj.
Intros.
Recall '(q p). Elim H.
Intros. Assert q == q0. Apply proof_irrelevance. Rewrite H. Trivial.
Save.



Lemma exists_proof : (p:E->Prop)(not (x:E)(not (p x))) -> (exists p).
Intros. Unfold not in H. EApply excluded_middle. Unfold not.
Intros. Apply H. Intros. Apply H0. EApply exists_intro with x.
Assumption. 
Save.

Lemma not_exists_pr : (p:E-> Prop)(not (exists p)) <-> ((x:E)(not (p x))).
Intros. Unfold iff. Apply conj. Intros. Unfold not. Unfold not in H.
Intros. Apply H. Apply exists_intro with x. Assumption.
  Intros. Unfold not. Unfold not in H. Intros. NewInduction H0.
Apply H with x. Assumption. 
Save. 

Definition Yy :(P:Prop; f:P-> E)E -> E.
Intros P f x. Apply by_cases with P. Exact f.
Intros. Exact x. Defined. 

Lemma Yy_if : (P:Prop; hyp : P; f:P-> E; x,z:E)(f hyp) == z ->
(Yy f x) == z. 
Intros. Unfold Yy. Pose b := [p:~P]x. 
Rewrite <- H. Apply by_cases_if. Save. 

Lemma Yy_if_not : (P:Prop; hyp : ~P; f:P-> E; x,z:E)x == z ->
(Yy f x) == z. 
Intros. Unfold Yy. Pose b := [p:~P]x.
Transitivity (b hyp). Apply by_cases_if_not. Trivial. 
Save.

Definition Y : Prop -> E -> E -> E.
Intros P x y.
EApply by_cases with P.
Intros. Exact x.
Intros. Exact y.
Defined.

Lemma Y_if : (P:Prop; hyp : P; x,y,z:E) x == z -> (Y P x y) == z.
Intros. Unfold Y. Pose a:= [p:P]x. Pose b := [p:~P]y.
Transitivity (a hyp). Apply by_cases_if. Transitivity x. 
Trivial.
Assumption. Save.

Lemma Y_if_not : (P:Prop; hyp : (not P); x,y,z:E) y == z -> 
(Y P x z) == y.
Intros. Unfold Y. Pose a:= [p:P]x. Pose b := [p:~P]z.
Transitivity (b hyp).  Apply by_cases_if_not. Rewrite H. Trivial.
Save.

Record Rec [x:E; f:x -> E] : E := join {
head : x;
tail : (f head)
}.
Implicits join [1 2].

Definition Z : E -> (E -> Prop) -> E.
Intros x p.
Pose (Rec [a:x](p (R a))).
Exact (IM [t:T](R (head t))).
Defined.

Lemma Z_inc : (x:E; p: E -> Prop; y:E)(inc y x) -> (p y) -> (inc y (Z x p)).
Intros. Unfold Z. EApply IM_inc. Unfold inc in H. NewInduction H.
Assert (p (R x0)). Rewrite H. Assumption.
Pose (join 2![a:x](p (R a)) x0 H1). Apply exT_intro with r. Trivial.
Save.

Lemma Z_sub : (x:E; p: E -> Prop)(sub (Z x p) x).
Intros. Unfold sub. Intros. Pose (IM_exists H).
NewInduction e. Rewrite <- H0. Apply R_inc.
Save.

Lemma Z_pr : (x:E; p: E-> Prop; y:E)(inc y (Z x p)) -> (p y).
Intros. Unfold inc in H. NewInduction H. Unfold Z in x0.
Pose (R_inc x0). Pose (IM_exists i). 
NewInduction e. Pose (tail x1).
Rewrite H0 in p0. Rewrite <- H. Assumption.
Save.


Definition X := [x:E; f: x -> E; y:E]
(Yy [hyp : (inc y x)](f (B hyp)) emptyset). 

Lemma X_eq : (x:E; f: x -> E; y,z: E)
(exT ? [a:x](A (R a) == y (f a) == z)) -> (X f y) == z. 
Intros. NewInduction H. Expand. Unfold X. 
Assert (inc y x). Rewrite <- H. Apply R_inc. 
Apply Yy_if with H1. Assert (B H1) == x0.  
Apply R_inj. Rewrite B_eq. Auto. Rewrite H2. Assumption.
Save. 

Lemma X_rewrite : (x:E; f: x -> E; a:x)
(X f (R a)) == (f a). 
Intros. 
Apply X_eq. Apply exT_intro with a. Deconj.
Trivial. Trivial. Save. 


Definition cut := [x:E; p: x -> Prop]
(Z x [y:E](hyp : (inc y x))(p (B hyp))). 

Lemma cut_sub : (x:E; p: x -> Prop)(sub (cut p) x). 
Intros. Unfold cut. Apply Z_sub. Save. 


Definition cut_to := [x:E; p: x -> Prop; y: (cut p)]
(B ((cut_sub 2!p) ? (R_inc y))). 

Lemma cut_to_R_eq : (x:E; p: x -> Prop; y: (cut p))
(R (cut_to y)) == (R y). 
Intros. Unfold cut_to. Rewrite B_eq. Trivial. Save. 



Lemma cut_pr : (x:E; p: x -> Prop; y:(cut p))(p (cut_to y)).
Intros. Unfold cut_to. Unfold cut in y. 
LetTac k :=  [y:E](hyp:(inc y x))(p (B hyp)). 
Pose (R_inc y). 
Pose (Z_pr i). Pose (k0 (cut_sub (R_inc y))). Assumption.
Save. 


Lemma cut_inc : (x:E; p: x -> Prop; y:x)(p y) -> 
(inc (R y) (cut p)). 
Intros. Unfold cut. Apply Z_inc. Apply R_inc. Intros. 
Assert (B hyp) == y. Apply R_inj. Apply B_eq. Rewrite H0. 
Assumption. Save. 

Module Little.



Inductive one_point : E := point : one_point.

Definition singleton := [x:E](IM [p:one_point]x).

Lemma singleton_inc : (x:E)(inc x (singleton x)).
Intros. Unfold singleton. Apply IM_inc.
Apply exT_intro with point. Trivial. Save.

Lemma singleton_eq : (x,y:E)(inc y (singleton x)) -> y == x.
Intros. Pose (IM_exists H). NewInduction e.
Symmetry. Trivial. Save.


Lemma singleton_inj : (x,y: E)(singleton x) == (singleton y) -> x == y. 
Intros. Assert (inc x (singleton y)). Rewrite <- H.
Apply singleton_inc.
Apply singleton_eq. Assumption. Save.









Inductive two_points : E := 
first : two_points | second : two_points.

Definition doubleton_map : (x,y:E)two_points -> E.
Intros x y t. NewInduction t. Exact x. Exact y. Defined.

Definition doubleton := [x,y:E](IM (doubleton_map x y)).

Lemma doubleton_first : (x,y:E)(inc x (doubleton x y)).
Intros. Unfold doubleton. Apply IM_inc. Apply exT_intro with first.
Trivial. Save.


Lemma doubleton_second : (x,y:E)(inc y (doubleton x y)).
Intros. Unfold doubleton. Apply IM_inc. Apply exT_intro with second.
Trivial. Save.



Lemma doubleton_or : (x,y,z:E)(inc z (doubleton x y)) -> (z == x) \/ (z == y).
Intros. Pose (IM_exists H). NewInduction e. NewInduction x0.
Compute in H0.
Intuition.
Compute in H0. Intuition. Save.   


Lemma doubleton_inj : (x,y,z,w:E)(doubleton x y) == (doubleton z w) -> 
(A x == z y == w) \/ (A x == w y == z). 
Intros. Assert (inc x (doubleton z w)). Rewrite <- H. Apply doubleton_first. 
Pose (doubleton_or H0). Assert (inc y (doubleton z w)). 
Rewrite <- H. 
Apply doubleton_second. Pose (doubleton_or H1). NewInduction o.
NewInduction o0. Assert (inc w (doubleton x y)). Rewrite H. 
Apply doubleton_second. Pose (doubleton_or H4). NewInduction o. 
Apply or_introl. Deconj. Assumption. Rewrite H5. Rewrite H2. Assumption.
Apply or_introl. Deconj. Assumption. Rewrite H5. Trivial. 
Apply or_introl. Deconj. Assumption. Assumption. 
NewInduction o0.
Apply or_intror. Deconj. Assumption. Assumption. 
Assert (inc z (doubleton x y)). Rewrite H. Apply doubleton_first. 
Pose (doubleton_or H4). NewInduction o. Apply or_introl. Deconj. Symmetry. 
Assumption. Assumption. Apply or_introl. Deconj. Rewrite H5. Rewrite H3. 
Assumption. Assumption. Save.



End Little.




Module Pair.

Export Little.

Definition pair := [x,y:E]
(doubleton (singleton x) (doubleton emptyset (singleton y))).

Definition is_pair := [u:E](exists [x:E](exists [y:E]u== (pair x y))).

Lemma lem1 : (x,y,z,w:E)(pair x y) == (pair z w) -> x == z.
Intros. Assert (inc (singleton x) (pair z w)). Rewrite <- H.
Unfold pair. Apply doubleton_first. Unfold pair in H0. Pose (doubleton_or H0). 
NewInduction o. Apply singleton_inj. Assumption. Assert (inc emptyset (singleton x)).
Rewrite H1. Apply doubleton_first. Assert (inc (singleton w) (singleton x)). 
Rewrite H1. Apply doubleton_second. Assert emptyset == x. Apply singleton_eq. Assumption.
Assert (singleton w) == x. Apply singleton_eq. Assumption. Assert (inc w emptyset).
Rewrite H4. Rewrite <- H5. Apply singleton_inc. Pose (emptyset_empty H6). 
Elim f. Save. 


Lemma lem2 : (x,y,z,w:E)(pair x y) == (pair z w) -> y == w.
Intros. Assert (inc (doubleton emptyset (singleton y)) (pair z w)). 
Rewrite <- H. Unfold pair. Apply doubleton_second. Unfold pair in H0.
Pose (doubleton_or H0). NewInduction o. Assert (inc emptyset (singleton z)).
Rewrite <- H1. Apply doubleton_first. Assert (inc (singleton y) (singleton z)).
Rewrite <- H1. Apply doubleton_second. Pose (singleton_eq H2).
Pose (singleton_eq H3). Assert (inc y emptyset). Rewrite e. Rewrite <- e0.
Apply singleton_inc. Pose (emptyset_empty H4). Elim f. 
Assert (inc (singleton y) (doubleton emptyset (singleton w))). 
Rewrite <- H1. Apply doubleton_second. Pose (doubleton_or H2). 
NewInduction o. Assert (inc y emptyset). Rewrite<- H3. Apply singleton_inc. 
Pose (emptyset_empty H4). Elim f. Apply singleton_inj. Assumption. Save. 




Definition pr1 := [u:E](choose [x:E](exists [y:E]u== (pair x y))).
Definition pr2 := [u:E](choose [y:E](exists [x:E]u == (pair x y))).

Syntactic Definition J := pair.
Syntactic Definition P := pr1.
Syntactic Definition Q := pr2. 


Definition pair_recovers := [u:E](pair (pr1 u) (pr2 u)) == u.

Lemma pair_recov : (u:E)(is_pair u) -> (pair_recovers u).
Intros. Unfold is_pair in H. Unfold pair_recovers. 
Pose (choose_pr H). Assert (exists [y:E](exists [x:E]
(u == (pair x y)))).
NewInduction e. Apply exists_intro with x. Apply
exists_intro with (pr1 u). Assumption. Pose (choose_pr H0).
NewInduction e. NewInduction e0. Assert u == (pair (pr1 u) x). 
Assumption. Assert u == (pair x0 (pr2 u)). Assumption. 
Assert (pair (pr1 u) x) == (pair x0 (pr2 u)). Rewrite <- H3.
Assumption. Pose (lem1 H5). Rewrite e. Symmetry. Assumption. 
Save. 

Lemma pair_is_pair : (x,y:E)(is_pair (pair x y)). 
Intros. Unfold is_pair. Apply exists_intro with x.
Apply exists_intro with y. Trivial. Save. 


Lemma pr1_pair : (x,y:E)(pr1 (pair x y)) == x.
Intros. LetTac u := (pair x y). Assert (is_pair u). 
Unfold u. Apply pair_is_pair. Pose (pair_recov H). 
Unfold pair_recovers in (Type of p). Unfold u in 
(Type of p). Pose (lem1 p). Assumption. Save. 

 

Lemma pr2_pair : (x,y:E)(pr2 (pair x y)) == y.
Intros. LetTac u := (pair x y). Assert (is_pair u). 
Unfold u. Apply pair_is_pair. Pose (pair_recov H). 
Unfold pair_recovers in (Type of p). Unfold u in 
(Type of p). Pose (lem2 p). Assumption. Save. 



End Pair.
Import Pair.

Definition V := [x,f:E](choose [y:E](inc (pair x y) f)).

Lemma V_inc : (x,z,f:E)(exists [y:E](inc (pair x y) f)) -> 
z == (V x f) ->
(inc (pair x z) f). 
Intros. Pose (choose_pr H). Rewrite H0. Assumption. Save. 


Module Image. 

Definition create := [x:E; f: E1](IM [a:x](f (R a))). 

Lemma  incl : (x:E; f:E -> E; a:E)(inc a x) -> 
(inc (f a) (create x f)).
Intros. Unfold create. Apply IM_inc. 
Apply exT_intro with (B H). Pose (B_eq H). Rewrite e. 
Trivial. Save. 


Lemma show_inc : (x:E; f:E -> E; z:E)
(exists [a:E](A (inc a x) (f a) == z)) -> (inc z (create x f)).
Intros. NewInduction H. Expand. Rewrite <- H0. 
Apply incl. Assumption. Save. 

Lemma ex : (x:E; f:E-> E; a:E)(inc a (create x f)) ->
(exists [b:E](A (inc b x) (f b) == a)).
Intros. Pose (IM_exists H). NewInduction e. Apply exists_intro
 with (R x0). Deconj. Unfold inc. Apply exT_intro with x0. 
Trivial. Assumption. Save. 


End Image.

Module Powerset. 

Definition powerset := [x:E](IM [p:x-> Prop](cut p)).


Lemma powerset_inc : (x,y:E)(sub x y) -> (inc x (powerset y)). 
Intros. Unfold powerset. Apply IM_inc. Apply exT_intro with
[b:y](inc (R b) x). Apply extensionality. Unfold sub. Intros. 
Pose (B H0). Pose (B_eq H0). Pose (cut_pr c). Assert 
x0 == (R (cut_to c)). Transitivity (R c). Unfold c. 
Auto. Symmetry. Apply cut_to_R_eq. Rewrite H1. Assumption. 
Unfold sub. Intros. Pose (B H0). Pose (B_eq H0). 
Rewrite <- e. Unfold cut. Apply Z_inc. Apply H. Rewrite e. 
Assumption. Intros. Pose (B_eq hyp). Rewrite e0. 
Rewrite e. Assumption. Save. 


Lemma powerset_sub : (x,y:E)(inc x (powerset y)) -> (sub x y).
Intros. Unfold powerset in H. Pose (IM_exists H). NewInduction e. 
Rewrite <- H0. Apply cut_sub. Save. 

End Powerset. 
Import Powerset. 

Module Union. 

Record  Integral [x:E] : E := {
param : x;
elt : (R param)
}.

Definition union := [x:E](IM [i:(Integral x)](R (!elt x i))).




Lemma union_inc : (x,y,a:E)(inc x y) -> (inc y a) -> 
(inc x (union a)).
Intros. 
Pose (B H0). Assert (R a0) == y. Unfold a0. Apply B_eq. 
Assert (inc x (R a0)). Rewrite H1. Assumption. 
Pose (B H2). Pose (!Build_Integral a a0 r). Unfold union.
Apply IM_inc. Apply exT_intro with i. Change (R r) == x. 
Unfold r. Apply B_eq. Save. 



Lemma union_exists : (x,a:E)(inc x (union a)) -> 
(exists [y:E](A (inc x y) (inc y a))).
Intros. Unfold union in H. Pose (IM_exists H). 
NewInduction e. Apply exists_intro with (R (param x0)). 
Deconj. Rewrite <- H0. Apply R_inc. Apply R_inc. Save. 

Definition union2 := [x,y:E](union (doubleton x y)). 


Lemma union2_or : (x,y,a:E)(inc a (union2 x y)) -> 
((inc a x) \/ (inc a y)).
Intros. Unfold union2 in H. Pose (union_exists H). 
NewInduction e. Expand. Pose (doubleton_or H1). 
NewInduction o. Rewrite H2 in H0. Intuition. 
Rewrite H2 in H0; Intuition. Save. 


Lemma union2_first : (x,y,a:E)(inc a x)-> (inc a (union2 x y)).
Intros. Unfold union2. Apply union_inc with x. Assumption.
Apply doubleton_first. Save. 

Lemma union2_second : (x,y,a:E)(inc a y)-> (inc a (union2 x y)).
Intros. Unfold union2. Apply union_inc with y. Assumption.
Apply doubleton_second. Save. 


End Union. 

Import Union. 

Module Intersection. 


Definition intersection := [x:E](Z (rep x) [y:E]
(z:E)(inc z x) -> (inc y z)). 

Lemma intersection_inc : (x,a:E)(nonempty x) -> 
((y:E)(inc y x) -> (inc a y)) -> (inc a (intersection x)). 
Intros. Unfold intersection. Apply Z_inc. 
Pose (nonempty_rep H). Apply H0. Assumption. Assumption. 
Save. 

Lemma intersection_forall : (x,a,y:E) 
(inc a (intersection x)) -> (inc y x) -> (inc a y). 
Intros. Unfold intersection in H0. 
Pose (Z_pr H). Apply i. Assumption. Save.


Definition intersection2 : E -> E -> E 
:= [x,y:E](intersection (doubleton x y)).

Lemma intersection2_inc : (x,y,a:E)(inc a x) -> 
(inc a y) ->(inc a (intersection2 x y)).
Intros.
Unfold intersection2.
Apply intersection_inc.
Apply nonempty_intro with x.
Apply doubleton_first.
Intros.
Recall '(doubleton_or H1).
NewInduction H2.
Rewrite H2.
Assumption.
Rewrite H2.
Assumption.
Save.

Lemma intersection2_first : (x,y,a:E)(inc a (intersection2 x y)) -> (inc a x).
Intros.
Unfold intersection2 in H.
EApply intersection_forall with (doubleton x y).
Assumption.
Apply doubleton_first.
Save.




Lemma intersection2_second : (x,y,a:E)(inc a (intersection2 x y)) -> (inc a y).
Intros.
Unfold intersection2 in H.
EApply intersection_forall with (doubleton x y).
Assumption.
Apply doubleton_second.
Save.


End Intersection.

Import Intersection. 





Module Transposition.

Definition create := [i,j,a:E]
(Y (a == i) j
(Y (a == j) i
   a
)).



Lemma not_i_not_j : (i,j,a:E)(not a==i) -> (not a==j) -> (create i j a) == a.
Intros. Unfold create. Apply (Y_if_not H). Symmetry. 
Apply (Y_if_not H0). Trivial. 
Save.

Lemma i_j_j_i : (i,j,a:E)(create i j a) == (create j i a).
Intros. Unfold create. Apply by_cases with a==i. Intros. 
Apply (Y_if H). Symmetry. Apply by_cases with a == j. 
Intros. Apply (Y_if H0). Rewrite <- H. Assumption. 
Intros. Apply (Y_if_not H0). Symmetry. Apply (Y_if H). 
Trivial. Intros. Apply (Y_if_not H). Apply by_cases with a== j. 
Intros. Apply (Y_if H0). Symmetry. Apply (Y_if H0). 
Trivial. 
Intros. Apply (Y_if_not H0). Apply (Y_if_not H0). 
Apply (Y_if_not H). Trivial. Save. 


Lemma i_j_i : (i,j : E)(create i j i) == j.
Intros. Unfold create. Assert i==i; Trivial. Apply (Y_if H). 
Trivial. 
Save.

Lemma i_j_j : (i,j : E)(create i j j) == i.
Intros. Rewrite i_j_j_i. Apply i_j_i. Save. 




Lemma i_i_a : (i,a:E)(create i i a) == a.
Intros. Apply by_cases with a == i. Intros. Rewrite H. 
Apply i_j_j. Intros. Unfold create. Apply (Y_if_not H). 
Symmetry. Apply (Y_if_not H). Trivial. 
Save.



Lemma surj : (i,j,a:E)(exists [b:E](create i j b) == a).
Intros.
Apply by_cases with a==i.
Intros. Apply exists_intro with j. Rewrite H. Apply i_j_j. 
Intros. Apply by_cases with a==j. Intros. 
Apply exists_intro with i. Rewrite H0. Apply i_j_i. 
Intros. 
Apply exists_intro with a. Apply not_i_not_j. 
Assumption. Assumption. 
Save.


Lemma involutive : (i,j,a:E)(create i j (create i j a)) == a. 
Intros. Apply by_cases with a==i. Intros. 
Rewrite H. Rewrite i_j_i. Apply i_j_j. 
Apply by_cases with a==j. Intros. Rewrite H. Rewrite i_j_j. 
Apply i_j_i. Intros. Pose (not_i_not_j H0 H). 
Rewrite e. Assumption. Save. 

Lemma inj : (i,j,a,b:E)(create i j a) == (create i j b) -> a == b.
Intros. Transitivity (create i j (create i j a)). 
Symmetry; Apply  involutive. Rewrite H. Apply involutive. 
Save. 



End Transposition.


Module Function.

Definition axioms :=  [f:E] 
(A (x:E)(inc x f) -> (pair (pr1 x) (pr2 x)) == x
   (x,y:E)(inc x f) -> (inc y f) -> (pr1 x) == (pr1  y) -> x == y
).

Definition domain [f:E] := (Image.create f pr1).
Definition range [f:E] := (Image.create f pr2).

Definition defined := [f,x:E]
(A (axioms f)
   (inc x (domain f))
).


Lemma sub_axioms : (f,g:E)(axioms g) -> (sub f g) -> (axioms f).
Intros. 
NewInduction H. 
Unfold sub in H0. 
UnfoldDeconj axioms.
Intros. 
Auto. 
Intros. 
Auto.
Save.

Lemma sub_domain : (f,g:E)(sub f g) -> (sub (domain f) (domain g)).
Intros. 
Unfold sub. 
Unfold domain. 
Unfold sub in H.
Intros. 
LetTac K := (Image.ex H0). 
NewInduction K. 
NewInduction H1.
Rewrite <- H2. 
Apply Image.incl. 
Auto.
Save.

Lemma sub_range : (f,g:E)(sub f g) -> (sub (range f) (range g)).
Intros. 
Unfold sub. 
Unfold range. 
Unfold sub in H. 
Intros.
LetTac K:= (Image.ex H0). 
NewInduction K. 
NewInduction H1.
Rewrite <- H2. 
Apply Image.incl. 
Auto.
Save.


Lemma range_inc : (f,z:E)(axioms f)-> (exists [y:E](A (inc y (domain f))
(V y f) == z)) -> (inc z (range f)). 
Intros. NewInduction H0. Expand. Unfold range. 
Apply Image.show_inc. Apply exists_intro with (pair x z).
Deconj. Apply V_inc. 
Unfold domain in H0.
Pose (Image.ex H0). NewInduction e; Expand. 
Apply exists_intro with (pr2 x0). 
Rewrite <- H3. Unfold axioms in H. Expand. 
Rewrite H. Assumption. Assumption. Auto. Apply pr2_pair. 
Save. 

Lemma defined_lem : (f,x:E)(axioms f) -> (defined f x) -> 
(inc (pair x (V x f)) f).
Intros.
Unfold axioms in H.
Unfold defined in H0.
Expand.
Unfold domain in H1.
LetTac K := (Image.ex H1).
NewInduction K.
NewInduction H3.
Assert (exists [y:E](inc (pair x y) f)).
EApply exists_intro with (pr2 x0).
Rewrite <- H4.
Rewrite H.
Assumption.
Assumption.
LetTac K := (choose_pr H5).
Assumption.
Save.

Lemma lem1 : (f,x:E)(axioms f) -> (inc x f) -> x == (pair (pr1 x) (V (pr1 x) f)).
Intros.
Unfold axioms in H.
Expand.
LetTac z := (pr1 x).
Assert (exists [y:E](inc (pair z y) f)).
Apply exists_intro with (pr2 x).
Unfold z.
Rewrite H.
Assumption.
Assumption.
LetTac K := (choose_pr H2).
Assert (inc (pair z (V z f)) f).
Assumption.
Apply H1.
Assumption.
Assumption.
Rewrite pr1_pair.
Trivial.
Save.


Lemma function_sub : (f,g:E)(axioms f) -> (axioms g) ->
((x:E)(defined f x) -> (defined g x)) ->
((x:E)(defined f x) -> (V x f) == (V x g)) ->
(sub f g).
Intros.
Unfold sub.
Intros.
LetTac K := (lem1 H H3).
Assert (defined f (pr1 x)).
UnfoldDeconj defined.
Assumption.
Unfold domain.
Apply Image.incl.
Assumption.
Assert (V (pr1 x) f) == (V (pr1 x) g).
Apply H2.
Assumption.
Rewrite K.
Assert (defined g (pr1 x)).
Apply H1.
Assumption.
Unfold defined in H6.
Expand.
Unfold domain in H7.
LetTac K1 := (Image.ex H7).
NewInduction K1.
NewInduction H8.
Unfold axioms in H0.
LetTac K1 := (lem1 H6 H8).
Rewrite H9 in K1.
Rewrite H5.
Rewrite <- K1.
Assumption.
Save.


Lemma function_extensionality : (f,g:E)(axioms f) -> (axioms g) ->
((x:E)(defined f x) -> (defined g x)) ->
((x:E)(defined g x) -> (defined f x)) ->
((x:E)(defined f x) -> (V x f) == (V x g)) ->
f == g.
Intros.
Apply extensionality.
Apply function_sub; Auto.
Apply function_sub; Auto.
Intros.
Symmetry.
Apply H3.
Apply H2.
Assumption.
Save.


Definition inverse_image := [a,f:E]
(Z (domain f) [x:E](inc (V x f) a)). 


Lemma inverse_image_sub : (a,f:E)
(sub (inverse_image a f) (domain f)).
Intros. Unfold inverse_image. Apply Z_sub. 
Save.

Lemma inverse_image_inc : (a,f,x:E)
(inc x (domain f)) -> (inc (V x f) a) -> 
(inc x (inverse_image a f)). 
Intros. Unfold inverse_image. Apply Z_inc. Assumption.
Assumption. Save. 

Lemma inverse_image_pr : (a,f,x:E)(inc x (inverse_image a f))
-> (inc (V x f) a). 
Intros. Unfold inverse_image in H. Pose (Z_pr H). 
Assumption. Save. 




Definition create := [x:E;p:E -> E]
(Image.create x [y:E](pair y (p y))).


Lemma elt_rewrite : (x:E; p: E -> E; y:E)
(inc y (create x p)) -> y == (pair (pr1 y) (p (pr1 y))).
Intros. Unfold create in H. Pose (Image.ex H).
NewInduction e. Expand. Assert (pr1 y) == x0.
Rewrite <- H1. Apply pr1_pair. Rewrite H2. Auto.
Save. 

Lemma create_axioms : (p:E-> E; x:E)(axioms (create x p)).
Intros. Unfold axioms; Deconj.
Intros. Apply pair_recov. Unfold create in H. 
Pose (Image.ex H). NewInduction e. Expand. 
Rewrite <- H1. Apply pair_is_pair. 
Intros. Unfold create in H. 
Unfold create in H0. Pose (Image.ex H).
Pose (Image.ex H0). NewInduction e. NewInduction e0. 
Expand. Rewrite <- H5. Assert x1 == x2. 
Transitivity (pr1 x0). Rewrite <- H5. 
Symmetry; Apply pr1_pair. Rewrite H1. Rewrite <- H4. 
Apply pr1_pair. Rewrite H6; Assumption. Save. 

Lemma create_inc : (x,y:E; hyp : (inc y x);
p: E -> E; z:E) 
(pair y (p y)) == z -> (inc z (create x p)). 
Intros. Unfold create. Apply Image.show_inc.
Apply exists_intro with y; Deconj; Auto. 
Save. 

Lemma create_domain : (x:E;p:E -> E)(domain (create x p)) == x.
Intros. Unfold domain. Apply extensionality; Unfold sub; Intros.
Pose (Image.ex H); NewInduction e; Expand. 
Unfold create in H0; Pose (Image.ex H0); NewInduction e; Expand.
Rewrite <- H1. Assert (pr1 x1) == x2. 
Rewrite <- H3; Apply pr1_pair. Rewrite H4; Auto. 
Apply Image.show_inc. Apply exists_intro with
(pair x0 (p x0)). Deconj. 
Apply (create_inc H); Auto. Apply pr1_pair. Save.




Lemma create_V_apply : (x:E; p: E-> E; y,z:E)
(inc y x) -> (p y) == z -> (V y (create x p)) == z.
Intros. Assert (inc (pair y (V y (create x p))) (create x p)).
Apply V_inc. Apply exists_intro with (p y). 
Apply (create_inc H). Trivial. Trivial. 
Assert (axioms (create x p)). Apply create_axioms. 
Unfold axioms in H2; Expand. 
Assert (pair y (V y (create x p))) == (pair y z). 
Apply H3. Apply V_inc. Apply exists_intro with (p y). 
Apply (create_inc H). Trivial. Trivial. 
Apply (create_inc H). Rewrite H0; Trivial. Rewrite pr1_pair.
Rewrite pr1_pair. Trivial. Transitivity (pr2 (pair y z)). 
Rewrite <- H4. Symmetry; Apply pr2_pair. 
Apply pr2_pair. Save. 

Lemma create_V_rewrite : (x:E; p: E -> E; y: E)
(inc y x) -> (V y (create x p)) == (p y). 
Intros. Apply create_V_apply; Auto. Save. 


Lemma create_range : (p:E-> E; x:E)(range (create x p)) ==
(Image.create x p).
Intros. Unfold range. Apply extensionality; Unfold sub; Intros.
Pose (Image.ex H); NewInduction e; Expand. Apply Image.show_inc. 
Unfold create in H0. Pose (Image.ex H0); NewInduction e; Expand.
Apply exists_intro with x2. Deconj. Assumption. 
Rewrite <- H1. Rewrite <- H3. Symmetry; Apply pr2_pair. 
Pose (Image.ex H); NewInduction e; Expand. 
Apply Image.show_inc. Apply exists_intro with (pair x1 x0). 
Deconj. Apply (create_inc H0). Rewrite H1. Trivial. 
Apply pr2_pair. 
Save.

Lemma create_recovers : (f:E)(axioms f) -> 
(create (domain f) [x:E](V x f)) == f.
Intros. Apply function_extensionality. 
Apply create_axioms. Assumption. Intros.. 
Unfold defined in H0. Expand. Unfold defined.
Deconj. Assumption. Rewrite create_domain in H1. Assumption.
Intros. Unfold defined in H0. Expand. 
Unfold defined; Deconj. Apply create_axioms. 
Rewrite create_domain. Assumption. 
Intros. Unfold defined in H0; Expand. Rewrite
create_domain in H1. Apply create_V_apply; Auto. 
Save. 


Lemma create_V_defined : (x:E; p: E -> E; y: E)
(defined (create x p) y) -> (V y (create x p)) == (p y). 
Intros. Apply create_V_apply. Unfold defined in H. 
Expand. Rewrite create_domain in H0. Assumption. 
Trivial. Save. 


Definition composable := [f,g:E]
(A (axioms f)
(A (axioms g)
   (sub (range g) (domain f))
)). 



Definition compose := [f,g:E]
(create (inverse_image (domain f) g) [y:E](V (V y g) f)).

Lemma compose_axioms : (f,g:E)(axioms (compose f g)).
Intros. Unfold compose. 
Apply create_axioms. Save. 


Lemma compose_domain : (f,g:E)
(domain (compose f g)) ==
(inverse_image (domain f) g).
Intros. Unfold compose. 
Rewrite create_domain. Trivial. 
Save.

Lemma composable_domain : (f,g:E)(composable f g) -> 
(domain (compose f g)) == (domain g). 
Intros. Unfold compose. 
Rewrite create_domain. Apply extensionality. 
Apply inverse_image_sub. 
Unfold sub; Intros. Apply inverse_image_inc. Assumption.
Unfold composable in H. Expand. 
Apply H2. Apply range_inc. Assumption. 
Apply exists_intro with x. Deconj; Auto. Save. 



Lemma compose_ev : (x,f,g:E)(inc x (domain (compose f g))) ->
(V x (compose f g)) == (V (V x g) f).
Intros. Unfold compose. 
Unfold compose in H. 
Rewrite create_domain in H. Apply create_V_apply. 
Assumption. Trivial. Save. 



Definition identity [x:E] := (create x [y:E]y).

Lemma identity_domain : (x:E)(domain (identity x)) == x.
Intros; Unfold identity; Rewrite create_domain; Trivial. 
Save. 


Lemma identity_ev : (x,a:E)(inc x a) -> (V x (identity a)) == x.
Intros. Unfold identity. Apply create_V_apply; Auto. 
Save.


End Function.

Syntactic Definition L := Function.create.

Module Notation.

Inductive t : E := 
Objects : t |
Morphisms : t |
Source : t|
Target : t|
Comp : t |
Id : t |
Plus : t |
Times : t.

Definition G := [i:t; x:E](V (R i) x). 

Definition create := [f:t -> E](L t (X f)). 

Lemma get_back : (f:t-> E; i:t)(G i (create f)) ==  (f i). 
Intros. Unfold G. Unfold create. 
Apply Function.create_V_apply. Apply R_inc. 
Apply X_eq. Apply exT_intro with i; Deconj; Auto. 
Save. 


End Notation. 

Export Notation. 

(*** a little section designed to indicate how Notation 
should be used ***)
Module Category. 

Definition objects := [c:E](G Objects c).
Definition morphisms := [c:E](G Morphisms c).
Definition source := [c,u:E](V u (G Source c)). 
Definition target := [c,u:E](V u (G Target c)).
Definition comp := [c,u,v:E](V u (V v (G Comp c))). 
Definition id := [c,x:E](V x (G Id c)).

Definition create := [o,m:E; s,t: E1; c:E2; i: E1]
(Notation.create [a:Notation.t]
Cases a of 
Objects => o |
Morphisms => m |
Source => (L m s) |
Target => (L m t) |
Comp => (L m [u:E](L m [v:E](c u v))) |
Id => (L o i) |
_ => emptyset 
end).

End Category.