Require Export set.

Set Implicit Arguments.
Unset Strict Implicit.



Module Function.

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

Definition domain (f : E) := Image.create f P.
Definition range (f : E) := Image.create f Q.

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


Lemma sub_axioms : forall f g : E, axioms g -> sub f g -> axioms f.
ir. 
nin H. 
unfold sub in H0. 
unfold axioms in |- *; xd.
Qed.

Lemma sub_domain : forall f g : E, sub f g -> sub (domain f) (domain g).
ir. 
unfold sub in |- *. 
unfold domain in |- *. 
unfold sub in H.
ir. 
set (K := Image.ex H0) in *. 
nin K. 
nin H1.
rewrite <- H2. 
ap Image.incl. 
au.
Qed.

Lemma sub_range : forall f g : E, sub f g -> sub (range f) (range g).
ir. 
unfold sub in |- *. 
unfold range in |- *. 
unfold sub in H. 
ir.
set (K := Image.ex H0) in *. 
nin K. 
nin H1.
rewrite <- H2. 
ap Image.incl. 
au.
Qed.


Lemma range_inc :
 forall f z : E,
 axioms f ->
 ex (fun y : E => A (inc y (domain f)) (V y f = z)) -> inc z (range f). 
ir. nin H0. xd. unfold range in |- *. 
ap Image.show_inc. apply ex_intro with (pair x z).
xd. ap V_inc. 
unfold domain in H0.
pose (Image.ex H0). nin e; xd. 
apply ex_intro with (pr2 x0). 
rewrite <- H3. unfold axioms in H. xd. 
rewrite H. am. am. au. ap pr2_pair. 
Qed. 




Lemma defined_lem :
 forall f x : E, axioms f -> defined f x -> inc (pair x (V x f)) f.
ir.
unfold axioms in H.
unfold defined in H0.
xd.
unfold domain in H1.
set (K := Image.ex H1) in *.
nin K.
nin H3.
assert (ex (fun y : E => inc (pair x y) f)).
eapply ex_intro with (pr2 x0).
rewrite <- H4.
rewrite H.
am.
am.
set (K := choose_pr H5) in *.
am.
Qed.

Lemma lem1 :
 forall f x : E, axioms f -> inc x f -> x = pair (pr1 x) (V (pr1 x) f).
ir.
unfold axioms in H.
xd.
set (z := pr1 x) in *.
assert (ex (fun y : E => inc (pair z y) f)).
apply ex_intro with (pr2 x).
unfold z in |- *.
rewrite H.
am.
am.
set (K := choose_pr H2) in *.
assert (inc (pair z (V z f)) f).
am.
ap H1.
am.
am.
rewrite pr1_pair.
tv.
Qed.

Lemma lem2 : forall f x : E, axioms f -> inc x f -> inc (pr1 x) (domain f). 
ir. unfold domain in |- *. ap Image.incl. am. 
Qed. 

Lemma pr2_V : forall f x : E, axioms f -> inc x f -> pr2 x = V (pr1 x) f.
ir.
pose (lem1 H H0).
set (a := pr1 x) in *.
rewrite e.
rewrite pr2_pair.
tv.
Qed.

Lemma range_ex :
 forall f y : E,
 axioms f ->
 inc y (range f) -> ex (fun x : E => (inc x (domain f) & V x f = y)). 
ir. unfold range in H0. pose (Image.ex H0); nin e; xd. assert (axioms f).
am. unfold axioms in H; xd.
pose (H x H1). set (a := pr1 x) in *. set (b := pr2 x) in *. 
apply ex_intro with a. xd. unfold a in |- *; ap lem2; au. 
assert (x = pair a (V a f)). unfold a in |- *. ap lem1; au. 
rewrite <- H2. unfold b in |- *. rewrite H5. 
sy; ap pr2_pair. Qed. 

Lemma range_inc_rw : forall f y,
Function.axioms f -> 
inc y (range f) = (exists x, inc x (domain f) & y = V x f).
Proof.
ir. 
ap iff_eq; ir. cp (range_ex H H0). nin H1. 
sh x; xd. nin H0. ee. ap range_inc. am. sh x. 
xd. 
Qed.  

Lemma function_sub :
 forall f g : E,
 axioms f ->
 axioms g ->
 (forall x : E, defined f x -> defined g x) ->
 (forall x : E, defined f x -> V x f = V x g) -> sub f g.
ir.
unfold sub in |- *.
ir.
set (K := lem1 H H3) in *.
assert (defined f (pr1 x)).
unfold defined in |- *; xd.
unfold domain in |- *.
ap Image.incl.
am.
assert (V (pr1 x) f = V (pr1 x) g).
ap H2.
am.
rewrite K.
assert (defined g (pr1 x)).
ap H1.
am.
unfold defined in H6.
xd.
unfold domain in H7.
set (K1 := Image.ex H7) in *.
nin K1.
nin H8.
unfold axioms in H0.
set (K1 := lem1 H6 H8) in *.
rewrite H9 in K1.
rewrite H5.
rewrite <- K1.
am.
Qed.


Lemma function_extensionality :
 forall f g : E,
 axioms f ->
 axioms g ->
 (forall x : E, defined f x -> defined g x) ->
 (forall x : E, defined g x -> defined f x) ->
 (forall x : E, defined f x -> V x f = V x g) -> f = g.
ir.
ap extensionality.
ap function_sub; au.
ap function_sub; au.
ir.
sy.
ap H3.
ap H2.
am.
Qed.


Definition inverse_image (a f : E) :=
  Z (domain f) (fun x : E => inc (V x f) a). 


Lemma inverse_image_sub : forall a f : E, sub (inverse_image a f) (domain f).
ir. unfold inverse_image in |- *. ap Z_sub. 
Qed.

Lemma inverse_image_inc :
 forall a f x : E,
 inc x (domain f) -> inc (V x f) a -> inc x (inverse_image a f). 
ir. unfold inverse_image in |- *. ap Z_inc. am.
am. Qed. 

Lemma inverse_image_pr :
 forall a f x : E, inc x (inverse_image a f) -> inc (V x f) a. 
ir. unfold inverse_image in H. Ztac. 
Qed. 




Definition create (x : E) (p : E1) :=
  Image.create x (fun y : E => pair y (p y)).


Lemma elt_rewrite :
 forall (x : E) (p : E1) (y : E),
 inc y (create x p) -> y = pair (pr1 y) (p (pr1 y)).
ir. unfold create in H. pose (Image.ex H).
nin e. xd. assert (pr1 y = x0).
rewrite <- H1. ap pr1_pair. rewrite H2. au.
Qed. 

Lemma create_axioms : forall (p : E1) (x : E), axioms (create x p).
ir. unfold axioms in |- *; xd.
ir. ap pair_recov. unfold create in H. 
pose (Image.ex H). nin e. xd. 
rewrite <- H1. ap pair_is_pair. 
ir. unfold create in H. 
unfold create in H0. pose (Image.ex H).
pose (Image.ex H0). nin e. nin e0. 
xd. rewrite <- H5. assert (x1 = x2). 
transitivity (pr1 x0). rewrite <- H5. 
sy; ap pr1_pair. rewrite H1. rewrite <- H4. 
ap pr1_pair. rewrite H6; am. Qed. 

Lemma create_axioms_rw : forall p x,
axioms (create x p) = True.
Proof.
ir. app iff_eq; ir. ap create_axioms. 
Qed.

Hint Rewrite create_axioms_rw : aw. 

Lemma create_inc :
 forall (x y : E) (hyp : inc y x) (p : E1) (z : E),
 pair y (p y) = z -> inc z (create x p). 
ir. unfold create in |- *. ap Image.show_inc.
apply ex_intro with y; xd. 
Qed. 

Lemma create_domain : forall (x : E) (p : E1), domain (create x p) = x.
ir. unfold domain in |- *. ap extensionality; unfold sub in |- *; ir.
pose (Image.ex H); nin e; xd. 
unfold create in H0; pose (Image.ex H0); nin e; xd.
rewrite <- H1. assert (pr1 x1 = x2). 
rewrite <- H3; ap pr1_pair. rewrite H4; au. 
ap Image.show_inc. apply ex_intro with (pair x0 (p x0)). xd. 
ap (create_inc H); au. ap pr1_pair. Qed.


Hint Rewrite create_domain : aw. 

Lemma create_V_apply :
 forall (x : E) (p : E1) (y z : E),
 inc y x -> p y = z -> V y (create x p) = z.
ir. assert (inc (pair y (V y (create x p))) (create x p)).
ap V_inc. apply ex_intro with (p y). 
ap (create_inc H). tv. tv. 
assert (axioms (create x p)). ap create_axioms. 
unfold axioms in H2; xd. 
assert (pair y (V y (create x p)) = pair y z). 
ap H3. ap V_inc. apply ex_intro with (p y). 
ap (create_inc H). tv. tv. 
ap (create_inc H). rewrite H0; tv. rewrite pr1_pair.
rewrite pr1_pair. tv. transitivity (pr2 (pair y z)). 
rewrite <- H4. sy; ap pr2_pair. 
ap pr2_pair. Qed. 

Lemma create_V_rewrite :
 forall (x : E) (p : E1) (y : E), inc y x -> V y (create x p) = p y. 
ir. ap create_V_apply; au. Qed. 

Hint Rewrite create_V_rewrite : aw. 

Lemma create_range :
 forall (p : E1) (x : E), range (create x p) = Image.create x p.
ir. unfold range in |- *. ap extensionality; unfold sub in |- *; ir.
pose (Image.ex H); nin e; xd. ap Image.show_inc. 
unfold create in H0. pose (Image.ex H0); nin e; xd.
apply ex_intro with x2. xd.
rewrite <- H1. rewrite <- H3. sy; ap pr2_pair. 
pose (Image.ex H); nin e; xd. 
ap Image.show_inc. apply ex_intro with (pair x1 x0). 
xd. ap (create_inc H0). rewrite H1. tv. 
ap pr2_pair. 
Qed.

Lemma create_recovers :
 forall f : E, axioms f -> create (domain f) (fun x : E => V x f) = f.
ir. ap function_extensionality. 
ap create_axioms. am. ir. 
unfold defined in H0. xd. unfold defined in |- *.
xd. rewrite create_domain in H1. am.
ir. unfold defined in H0. xd. 
unfold defined in |- *; xd. ap create_axioms. 
rewrite create_domain. am. 
ir. unfold defined in H0; xd. rewrite create_domain in H1. ap create_V_apply; au. 
Qed. 


Lemma create_V_defined :
 forall (x : E) (p : E1) (y : E),
 defined (create x p) y -> V y (create x p) = p y. 
ir. ap create_V_apply. unfold defined in H. 
xd. rewrite create_domain in H0. am. 
tv. Qed. 


Lemma create_extensionality :
 forall (a b : E) (f g : E1),
 a = b ->
 (forall x : E, inc x a -> inc x b -> f x = g x) -> create a f = create b g.
ir.
assert (axioms (create a f)).
ap create_axioms.

assert (axioms (create b g)).
ap create_axioms.

ap function_extensionality; au.
unfold defined in |- *; ir.
xd.
rewrite create_domain.
rewrite <- H.
rewrite create_domain in H4.
am.

unfold defined in |- *.
ir; xd.
rewrite create_domain.
rewrite create_domain in H4.
rewrite H.
am.

ir.
assert (inc x a).
unfold defined in H3.
xd.
rewrite create_domain in H4; am.

repeat rewrite create_V_rewrite.
ap H0.
am.

rewrite <- H.
am.

rewrite <- H.
am.

am.
Qed.

Lemma create_create :
 forall (a : E) (f : E1),
 create a (fun x : E => V x (create a f)) = create a f.
ir.
ap create_extensionality.
tv.

ir.
ap create_V_rewrite.
am.
Qed.

Lemma create_rw : forall x f,
x = domain f -> 
axioms f -> 
create x (fun x => V x f) = f. 
Proof.
ir. rw H. 
util (create_recovers (f:= f)). am. am. 
Qed. 

Lemma create_V_out : forall x f y,
~inc y x -> V y (create x f) = emptyset.
Proof.
ir. cp (V_or y (create x f)). 
nin H0. 
assert (axioms (create x f)). app create_axioms. 
cp (lem2 H1 H0). rwi pr1_pair H2. 
rwi create_domain H2. nin (H H2). ee; am.  
Qed. 


Definition composable (f g : E) :=
axioms f & axioms g & sub (range g) (domain f). 



Definition compose (f g : E) :=
  create (inverse_image (domain f) g) (fun y : E => V (V y g) f).

Lemma compose_axioms : forall f g : E, axioms (compose f g).
ir. unfold compose in |- *. 
ap create_axioms. Qed. 


Lemma compose_domain :
 forall f g : E, domain (compose f g) = inverse_image (domain f) g.
ir. unfold compose in |- *. 
rewrite create_domain. tv. 
Qed.

Lemma composable_domain :
 forall f g : E, composable f g -> domain (compose f g) = domain g. 
ir. unfold compose in |- *. 
rewrite create_domain. ap extensionality. 
ap inverse_image_sub. 
unfold sub in |- *; ir. ap inverse_image_inc. am.
unfold composable in H. xd. 
ap H2. ap range_inc. am. 
apply ex_intro with x. xd. Qed. 



Lemma compose_ev :
 forall x f g : E,
 inc x (domain (compose f g)) -> V x (compose f g) = V (V x g) f.
ir. unfold compose in |- *. 
unfold compose in H. 
rewrite create_domain in H. ap create_V_apply. 
am. tv. Qed. 



Definition identity (x : E) := create x (fun y : E => y).


Lemma identity_axioms : forall x : E, axioms (identity x). 
ir; unfold identity in |- *; ap create_axioms. 
Qed. 


Lemma identity_domain : forall x : E, domain (identity x) = x.
ir; unfold identity in |- *; rewrite create_domain; tv. 
Qed. 


Lemma identity_ev : forall x a : E, inc x a -> V x (identity a) = x.
ir. unfold identity in |- *. ap create_V_apply; au. 
Qed.


(*** function restriction ****)

Definition restr f x :=
Z f (fun y=> inc (pr1 y) x).

Lemma restr_inc_rw : forall f x y,
inc y (restr f x) = (inc y f & inc (pr1 y) x).
Proof.
ir. ap iff_eq; ir. ufi restr H. Ztac. 
uf restr. ap Z_inc; xd. 
Qed.

Lemma restr_axioms : forall f x,
Function.axioms f -> Function.axioms (restr f x).
Proof.
ir. 
uhg; dj.
rwi restr_inc_rw H0. uh H; ee. ap H; am. 
uh H; ee. ap H4. rwi restr_inc_rw H1; xd. 
rwi restr_inc_rw H2; xd. am. 
Qed.

Lemma restr_domain : forall f x,
Function.axioms f -> 
domain (restr f x) = intersection2 (domain f) x.
Proof.
ir. 
ap extensionality; uhg; ir. ufi domain H0. 
rwi Image.inc_rw H0. nin H0; ee. 
ufi restr H0; Ztac. 
ap intersection2_inc. uf domain. 
rw Image.inc_rw. sh x1; ee. am. am. wr H1; am. 
cp (intersection2_first H0).
cp (intersection2_second H0). 
uf domain. rw Image.inc_rw. 
ufi domain H1. rwi Image.inc_rw H1. nin H1; ee. 
sh x1. ee; try am. uf restr; ap Z_inc. 
am. rw H3; am.  
Qed.

Lemma restr_sub : forall f x, sub (restr f x) f.
Proof.
ir.
uhg; ir. rwi restr_inc_rw H. ee; am. 
Qed.

Lemma function_sub_eq : forall r s, 
Function.axioms r -> Function.axioms s -> sub r s ->
sub (domain s) (domain r) -> r = s.
Proof.
ir. 
ap extensionality; try am. uhg; ir. 
cp (Function.lem1 H0 H3).
cp (Function.lem2 H0 H3).
assert (inc (pr1 x) (domain r)). 
ap H2; am. 
util (Function.defined_lem (f:=r) (x:=(pr1 x))). 
am. uhg; ee; am. 
assert (inc (pair (pr1 x) (V (pr1 x) r)) s).
ap H1; am. rwi H4 H3. uh H0; ee. 
assert (pair (pr1 x) (V (pr1 x) r) = pair (pr1 x) (V (pr1 x) s)).
ap H9. 
am. am. do 2 (rw pr1_pair). tv. rwi H10 H7. 
wri H4 H7. am. 
Qed. 

Lemma restr_to_domain : forall f g, 
Function.axioms f -> Function.axioms g -> sub f g ->
restr g (domain f) = f.
Proof.
ir. sy. ap function_sub_eq. am. ap restr_axioms. am. 
uhg; ir. uf restr; ap Z_inc. ap H1; am. uf domain.
rw Image.inc_rw. sh x; ee; try am; try tv. 
rw restr_domain. uhg; ir. cp (intersection2_second H2). am.
am.  
Qed. 

Lemma restr_ev : forall f u x,
Function.axioms f -> sub u (domain f) -> inc x u ->
V x (restr f u) = V x f.
Proof.
ir. util (Function.defined_lem (f:=f) (x:=x)). 
am. uhg. ee. am. ap H0; am. cp (restr_sub (f:=f) (x:= u)). 
assert (inc (pair x (V x f)) (restr f u)).
uf restr; ap Z_inc; ee. am. rw pr1_pair. am. 
cp Function.pr2_V. assert (Function.axioms (restr f u)).
ap restr_axioms; try am. cp (H5 _ _ H6 H4). 
rwi pr2_pair H7. rwi pr1_pair H7. sy; am. 
Qed. 

(*********************************)


Lemma function_glueing : forall z,
(forall f, inc f z -> Function.axioms f) -> 
(forall f g x, inc f z -> inc g z -> defined f x -> defined g x
-> (V x f) = (V x g)) -> 
Function.axioms (union z).
Proof.
ir. 
uhg; ee; ir. nin (union_exists H1); ee. 
cp (H _ H3). uh H4. ee. ap H4; am. 
nin (union_exists H1);  nin (union_exists H2); ee. 
cp (H _ H7); cp (H _ H6).
cp (Function.lem1 H8 H4).
cp (Function.lem1 H9 H5).
rw H10; rw H11. 
rw H3. 
assert (V (pr1 y) x0 = V (pr1 y) x1). 
ap H0. am. am. uhg; ee; try am. 
wr H3; 
ap Function.lem2; try am. 
uhg; ee; try am; ap Function.lem2; try am.
rw H12; tv. 
Qed. 

Lemma function_sub_V : forall f g x:E,
Function.axioms g -> defined f x -> sub f g ->
V x f = V x g.
Proof. 
ir. 
cp H0; uh H0; ee. 
cp (Function.defined_lem H0 H2).
cp (H1 _ H4). 
cp (Function.lem1 H H5). 
rwi pr1_pair H6. 
transitivity (pr2 (pair x (V x f))). 
rw pr2_pair; tv. rw H6. 
rw pr2_pair; tv. 
Qed. 

(*** nb Function.defined_lem should be changed as its 
axioms hypothesis is extraneous ***)


Lemma domain_union : forall z:E, domain (union z) =
union (Image.create z domain).
Proof.
ir. ap extensionality; uhg; ir. ufi domain H. 
rwi Image.inc_rw H. nin H. ee. 
nin (union_exists H). ee. 
apply union_inc with (domain x1). uf domain;
rw Image.inc_rw. sh x0; xd. 
rw Image.inc_rw. sh x1; xd. 
nin (union_exists H). ee. 
rwi Image.inc_rw H1. nin H1; ee. uf domain;
rw Image.inc_rw. 
ufi domain H2. wri H2 H0. rwi Image.inc_rw H0. 
nin H0; ee. sh x2; xd. apply union_inc with x1. 
am. am. 
Qed.  

Lemma domain_tack_on : forall f x y:E,
domain (tack_on f (pair x y)) = tack_on (domain f) x.
Proof.
ir. ap extensionality; uhg; ir. 
ufi domain H; rwi Image.inc_rw H; nin H; ee. 
rwi tack_on_inc H; nin H. 
rw tack_on_inc; ap or_introl. 
uf domain; rw Image.inc_rw. sh x1. xd. 
rw tack_on_inc; ap or_intror. 
wr H0; rw H. rw pr1_pair. tv. 
uf domain; rw Image.inc_rw. 
rwi tack_on_inc H; nin H. 
ufi domain H; rwi Image.inc_rw H; nin H; ee. sh x1.
ee; try am. rw tack_on_inc. ap or_introl;am. 
sh (pair x y). ee. rw tack_on_inc; ap or_intror; tv. 
rw pr1_pair. sy; am. 
Qed. 

Lemma range_union : forall z:E, range (union z) =
union (Image.create z range).
Proof.
ir. ap extensionality; uhg; ir. ufi range H. 
rwi Image.inc_rw H. nin H. ee. 
nin (union_exists H). ee. 
apply union_inc with (range x1). uf range;
rw Image.inc_rw. sh x0; xd. 
rw Image.inc_rw. sh x1; xd. 
nin (union_exists H). ee. 
rwi Image.inc_rw H1. nin H1; ee. uf range;
rw Image.inc_rw. 
ufi range H2. wri H2 H0. rwi Image.inc_rw H0. 
nin H0; ee. sh x2; xd. apply union_inc with x1. 
am. am. 
Qed.  

Lemma range_tack_on : forall f x y:E,
range (tack_on f (pair x y)) = tack_on (range f) y.
Proof.
ir. ap extensionality; uhg; ir. 
ufi range H; rwi Image.inc_rw H; nin H; ee. 
rwi tack_on_inc H; nin H. 
rw tack_on_inc; ap or_introl. 
uf range; rw Image.inc_rw. sh x1. xd. 
rw tack_on_inc; ap or_intror. 
wr H0; rw H. rw pr2_pair. tv. 
uf range; rw Image.inc_rw. 
rwi tack_on_inc H; nin H. 
ufi range H; rwi Image.inc_rw H; nin H; ee. sh x1.
ee; try am. rw tack_on_inc. ap or_introl; am. 
sh (pair x y). ee. rw tack_on_inc; ap or_intror; tv. 
rw pr2_pair. sy; am. 
Qed. 





Lemma function_tack_on_axioms : forall f x y:E,
Function.axioms f -> ~inc x (domain f) ->
Function.axioms (tack_on f (pair x y)).
Proof.
ir. uhg; ee; ir. rwi tack_on_inc H1.

nin H1. uh H; ee; au. rw H1. 
rw pr1_pair; rw pr2_pair; tv. 
rwi tack_on_inc H1; rwi tack_on_inc H2; nin H1; nin H2.
uh H; ee; au. assert False. 
ap H0. rwi H2 H3. 
rwi pr1_pair H3. wr H3. 
ap Function.lem2; try am. elim H4. 
assert False. ap H0. 
rwi H1 H3; rwi pr1_pair H3. rw H3. 
ap Function.lem2; try am.
elim H4. rw H2; am. 
Qed. 


(**** now we create a function given a set x and a map f : x->E ***)

Definition tcreate (x:E) (f:x->E) :=
create x (fun y => (Yy (fun (hyp : inc y x) => f (B hyp)) emptyset)).

Lemma tcreate_value_type : forall x (f:x->E) y,
V (R y) (tcreate f) = f y.
Proof.
ir. uf tcreate. 
rw create_V_rewrite. 
assert (inc (R y) x). 
ap R_inc. 
apply Yy_if with H.
rw B_back. 
tv. ap R_inc. 
Qed.

Lemma tcreate_value_inc : forall x (f:x->E) y (hyp : inc y x),
V y (tcreate f) = f (B hyp).
Proof.
ir. assert (y = R (B hyp)). rww B_eq. 
transitivity (V (R (B hyp)) (tcreate f)). 
wr H. tv. ap tcreate_value_type. 
Qed.

Lemma domain_tcreate : forall x (f:x->E), domain (tcreate f) = x.
Proof.
ir. uf tcreate. rw create_domain. tv. 
Qed.


End Function.

Notation L := Function.create.




Module Transformation.


Definition covers (a b : E) (f : E1) :=
  forall x : E, inc x b -> ex (fun y : E => A (inc y a) (f y = x)).
Definition injects (a : E) (f : E1) :=
  forall x y : E, inc x a -> inc y a -> f x = f y -> x = y.


Definition inverse (a : E) (f : E1) (y : E) :=
  choose (fun x : E => (inc x a & f x = y)).


Definition axioms (a b : E) (f : E1) := forall x : E, inc x a -> inc (f x) b.

Lemma compose_axioms :
 forall (a b c : E) (f g : E1),
 axioms b c f -> axioms a b g -> axioms a c (fun x : E => f (g x)).
ir.
unfold axioms in |- *.
ir.
unfold axioms in H.
unfold axioms in H0.
au.
Qed.


Lemma identity_axioms : forall a : E, axioms a a (fun x : E => x).
ir.
unfold axioms in |- *.
ir.
am.
Qed.

Definition surjective (a b : E) (f : E1) := 
(axioms a b f & covers a b f).

Lemma surjective_inverse_axioms :
 forall (a b : E) (f : E1), surjective a b f -> axioms b a (inverse a f).
ir.
unfold axioms in |- *.
ir.
unfold inverse in |- *.
unfold surjective in H; xd.
unfold covers in H1; xd.
pose (H1 x H0).
pose (choose_pr e).
assert
 (A (inc (choose (fun x0 : E => A (inc x0 a) (f x0 = x))) a)
    (f (choose (fun x0 : E => A (inc x0 a) (f x0 = x))) = x)). 
am.
xd.
Qed.


Lemma surjective_inverse_right :
 forall (a b : E) (f : E1) (x : E),
 surjective a b f -> inc x b -> f (inverse a f x) = x.
ir.
unfold inverse in |- *.
unfold surjective in H; xd.
unfold covers in H1; xd.
pose (H1 x H0).
pose (choose_pr e).
assert
( inc (choose (fun x0 : E => (inc x0 a & f x0 = x))) a
& f (choose (fun x0 : E => (inc x0 a & f x0 = x))) = x). 
am. 
xd.
Qed.


Definition injective (a b : E) (f : E1) := 
( axioms a b f 
& injects a f).

Definition bijective (a b : E) (f : E1) :=
( axioms a b f
& surjective a b f
& injective a b f).

Definition are_inverse (a b : E) (f g : E1) :=
  axioms a b f
& axioms b a g
& (forall x : E, inc x a -> g (f x) = x)
& (forall y : E, inc y b -> f (g y) = y).

Lemma bijective_inverse :
 forall (a b : E) (f : E1),
 bijective a b f -> are_inverse a b f (inverse a f).
ir.
unfold are_inverse in |- *; xd.
unfold bijective in H; xd.

ap surjective_inverse_axioms.
unfold bijective in H; xd.


ir.
unfold bijective in H; ee.
unfold injective in H2.
ee.

assert (axioms b a (inverse a f)).
ap surjective_inverse_axioms; au.
unfold axioms in H4.
ap H3.
ap H4.
ap H. 
am.

am.

pose surjective_inverse_right.
assert (inc (f x) b).
ap H; am. 

pose (e _ _ _ _ H1 H5).
am.

ir.
unfold bijective in H; xd.
apply surjective_inverse_right with b.
am.

am.
Qed.

Lemma inverse_bijective :
 forall (a b : E) (f g : E1), are_inverse a b f g -> bijective a b f.
ir.
unfold bijective in |- *.
unfold are_inverse in H.
xd.
unfold surjective in |- *; xd.
unfold covers in |- *.
ir.
apply ex_intro with (g x).
xd.



unfold injective in |- *; xd.
unfold injects in |- *; ir.
rewrite <- H1.
rewrite <- H5.
rewrite H1; au.

am.
Qed. 

Lemma trans_sub_bijective : forall x y f u,
Transformation.injective x y f -> sub u x ->
Transformation.bijective u (Image.create u f) f.
Proof.
ir. 
uhg; dj. uhg; ee. 
ir. rw Image.inc_rw. sh x0; ee; try tv. 
uhg; ee; try am. uhg. ir. 
rwi Image.inc_rw H2. nin H2; ee. sh x1; ee; am. 
uhg; ee; try am. uhg; ir. uh H; ee. uh H6; ee.
ap H6; try am. ap H0; am.
ap H0; am. 
Qed. 

Lemma identity_bijective : forall x, 
Transformation.bijective x x (fun y => y).
Proof.
ir. uhg; dj. 
ap Transformation.identity_axioms. 
uhg; ee. am. uhg; ir. sh x0. ee. 
am. tv. uhg; ee; try am. 
uhg; ir. am. 
Qed. 

Lemma subidentity_injective : forall x y,
sub x y ->
Transformation.injective x y (fun z => z). 
Proof.
ir. uhg; ee. 
uhg; ee. ir; ap H; am. 
uhg; ir. am. 
Qed. 

Lemma compose_injective : forall x y z f g,
Transformation.injective x y f -> 
Transformation.injective y z g ->
Transformation.injective x z (fun y=> g (f y)).
Proof.
ir. uhg; dj. apply Transformation.compose_axioms
with y. lu. lu. uhg; ir. uh H; uh H0. ee.
assert (f x0 = f y0). ap H5. ap H. 
am. ap H; am. am. ap H6. am. am. am. 
Qed. 

Lemma compose_surjective : forall x y z f g,
Transformation.surjective x y f -> 
Transformation.surjective y z g ->
Transformation.surjective x z (fun y=> g (f y)).
Proof.
ir; uhg; dj. apply Transformation.compose_axioms with y; 
try lu. uhg; ir. uh H; uh H0; ee.
nin (H3 x0). ee. nin (H4 x1); ee. sh x2; ee; try am. 
rw H8. am. am. am. 
Qed. 

Lemma compose_bijective : forall x y z f g,
Transformation.bijective x y f ->
Transformation.bijective y z g ->
Transformation.bijective x z (fun y => g (f y)).
Proof.
ir. uhg; ee. 
apply Transformation.compose_axioms with y; lu. 
apply compose_surjective with y; lu. 
apply compose_injective with y; lu. 
Qed. 


End Transformation.


Module Map.

Import Function. 
Import Transformation. 

Definition axioms (a b f : E) :=
  Function.axioms f
& Function.domain f = a
& sub (Function.range f) b.

Lemma compose_axioms :
 forall a b c f g : E,
 axioms b c f -> axioms a b g -> axioms a c (Function.compose f g).
ir. unfold axioms in H, H0; xd. 
assert (Function.composable f g). unfold Function.composable in |- *. 
xd. rewrite H3; am. 
unfold axioms in |- *; xd. ap Function.compose_axioms.
rewrite Function.composable_domain; au. 
unfold sub in |- *; ir. 
assert (Function.axioms (Function.compose f g)). 
ap Function.compose_axioms. pose (Function.range_ex H7 H6). 
nin e; xd. pose (Function.compose_ev H8). 
rewrite H9 in e. rewrite e. ap H4. ap Function.range_inc. 
am. apply ex_intro with (V x0 g); xd. 
unfold Function.composable in H5; xd. 
ap H11. ap Function.range_inc. am. 
apply ex_intro with x0; xd. 
assert (Function.domain (Function.compose f g) = Function.domain g). 
ap Function.composable_domain. 
unfold Function.composable in |- *; xd. rewrite <- H12. 
am. Qed. 



Lemma identity_axioms : forall a : E, axioms a a (Function.identity a).
ir. unfold axioms in |- *; xd. ap Function.identity_axioms. 
ap Function.identity_domain. unfold sub in |- *; ir. 
assert (Function.axioms (Function.identity a)). 
ap Function.identity_axioms. pose (Function.range_ex H0 H). 
nin e; xd. rewrite Function.identity_domain in H1. 
rewrite Function.identity_ev in H2. rewrite <- H2; am. 
am. Qed. 



Definition surjective (a b f : E) :=
  axioms a b f 
& Transformation.covers a b (fun x : E => V x f).

Definition injective (a b f : E) :=
axioms a b f
& Transformation.injects a (fun x : E => V x f).

Definition bijective (a b f : E) :=
axioms a b f
& surjective a b f
& injective a b f.


Definition isomap x y := 
choose (Map.bijective x y).

Definition isotrans x y u:=
V u (isomap x y).

Definition are_isomorphic x y :=
exists f, Map.bijective x y f.

Lemma trans_map_axioms : forall x y f,
Transformation.axioms x y f =
Map.axioms x y (Function.create x f).
Proof.
ir. ap iff_eq; ir. uhg; ee. 
ap create_axioms. 
rw create_domain. tv. uhg; ir. 
rwi create_range H0. 
rwi Image.inc_rw H0. nin H0. ee. wr H1. 
uh H; ee. ap H. am. 


uhg. ir. uh H; ee. uh H2. 
ap H2. rw create_range. rw Image.inc_rw. 
sh x0. ee; try am; try tv. 
Qed.

Lemma trans_map_injective : forall x y f,
Transformation.injective x y f =
Map.injective x y (Function.create x f).
Proof.
ir. ap iff_eq; ir. 
uhg; ee. wr trans_map_axioms. 
uh H; ee; am. 
uhg. ir. rwi create_V_rewrite H2. 
rwi create_V_rewrite H2. uh H. 
ee. ap H3. am. 
am. am. am. am. 

uhg; ee. rw trans_map_axioms. uh H; ee; am. 
uhg; ir. uh H; ee. 
uh H3. 
cp (H3 _ _ H0 H1). ap H4. rw create_V_rewrite. 
rw create_V_rewrite. am. am. am. 
Qed.

Lemma trans_map_surjective : forall x y f,
Transformation.surjective x y f =
Map.surjective x y (Function.create x f).
Proof.
ir. 
ap iff_eq; ir. 
uhg; ee. 
wr trans_map_axioms. uh H; ee; am. 
uhg. ir. uh H; ee. uh H1. cp (H1 _ H0). 
nin H2. sh x1; ee. am. rw create_V_rewrite.
am. am. 
uhg; ee. rw trans_map_axioms. uh H; ee; am. 
uhg; ir. uh H; ee. uh H1.
cp (H1 _ H0). nin H2.
sh x1; ee. am. rwi create_V_rewrite H3. 
am. am. 
Qed.



Lemma trans_map_bijective : forall x y f,
Transformation.bijective x y f =
Map.bijective x y (Function.create x f).
Proof.
ir.
ap iff_eq; ir. uhg; ee.
wr trans_map_axioms; uh H; ee; am. 
wr trans_map_surjective; uh H; ee; am.
wr trans_map_injective; uh H; ee; am.
uhg; ee. 
rw trans_map_axioms; uh H; ee; am.
rw trans_map_surjective; uh H; ee; am.
rw trans_map_injective; uh H; ee; am.
Qed.

Lemma trans_bij_isomorphic : forall x y f,
Transformation.bijective x y f -> are_isomorphic x y.
Proof.
ir. uhg. 
sh (Function.create x f). 
wr trans_map_bijective; am.
Qed. 

Lemma isomap_bij : forall x y,
are_isomorphic x y -> Map.bijective x y (isomap x y). 
Proof.
ir. uh H. cp (choose_pr H). 
am. 
Qed. 



Lemma isotrans_bij : forall x y,
are_isomorphic x y -> 
Transformation.bijective x y (isotrans x y).
Proof.
ir. 
cp (isomap_bij H). 
rw trans_map_bijective. 
assert (create x (isotrans x y)= isomap x y).
uf  isotrans. 
rw create_rw. tv. 
uh H0; ee. uh H0; ee. rw H3; tv. lu. rw H1; am.
Qed. 




Lemma isomap_isotrans_rw : forall x y,
are_isomorphic x y ->
isomap x y = Function.create x (isotrans x y).
Proof.
ir. uf isotrans. rw create_rw. tv. 
cp (isomap_bij H). uh H0; ee. uh H0; ee. rw H3; tv. 
cp (isomap_bij H). uh H0; ee.
uh H0; ee. am. 
Qed. 



Lemma iso_isotrans_rw : forall x y,
are_isomorphic x y = 
Transformation.bijective x y (isotrans x y).
Proof.
ir; ap iff_eq; ir. 
ap isotrans_bij; am. 
uhg. sh (Function.create x (isotrans x y)). 
wr trans_map_bijective. am. 
Qed. 

Lemma iso_trans_ex_rw : forall x y,
are_isomorphic x y =
(exists f, Transformation.bijective x y f).
Proof.
ir; ap iff_eq; ir. 
sh (isotrans x y). 
wr iso_isotrans_rw; am. 
nin H. uhg. sh (Function.create x x0). 
wr trans_map_bijective; am. 
Qed. 

Lemma are_isomorphic_refl : forall x, are_isomorphic x x.
Proof.
ir. 
uhg. 
sh (Function.create x (fun y => y)). 
wr trans_map_bijective. ap identity_bijective. 
Qed.

Lemma are_inverse_symm : forall x y f g,
Transformation.are_inverse x y f g ->
Transformation.are_inverse y x g f.
Proof.
ir. uh H; uhg; xd. 
Qed. 

Lemma are_isomorphic_symm : forall x y, 
are_isomorphic x y ->
are_isomorphic y x.
Proof.
ir. rwi iso_isotrans_rw H. 
uhg. sh 
(Function.create y (Transformation.inverse x (isotrans x y))).
wr trans_map_bijective. 
apply Transformation.inverse_bijective with (isotrans x y). 
apply are_inverse_symm. 
apply Transformation.bijective_inverse. 
am. 
Qed.

Lemma are_isomorphic_trans : forall x z,
(exists y, (are_isomorphic x y & are_isomorphic y z)) ->
are_isomorphic x z.
Proof.
ir. nin H. ee. 
rwi iso_isotrans_rw H. rwi iso_isotrans_rw H0. 
rw iso_trans_ex_rw. 
sh (fun a => (isotrans x0 z (isotrans x x0 a))). 
apply compose_bijective with x0. am. am. 
Qed. 

End Map.

Module Bounded.

Definition property (p : EP) (x : E) :=
  forall y : E, (p y -> inc y x & inc y x -> p y). 


Definition axioms (p : EP) := ex (property p).


Definition create (p : EP) := choose (property p). 


Lemma criterion :
 forall p : EP,
 ex (fun x : E => forall y : E, p y -> inc y x) -> axioms p. 
ir. nin H. unfold axioms in |- *.
eapply ex_intro with (Z x p). unfold property in |- *.
ir; xd; ir. 
ap Z_inc. ap H; au. au. 
apply Z_pr with x. am. Qed. 



Lemma lem1 : forall (p : EP) (y : E), axioms p -> inc y (create p) -> p y.
ir. unfold create in H0. unfold axioms in H. 
pose (choose_pr H). unfold property in H0. 
unfold property in (type of p0). pose (p0 y). 
xd. Qed. 

Lemma lem2 : forall (p : EP) (y : E), axioms p -> p y -> inc y (create p).
ir. unfold create in |- *. unfold axioms in H. pose (choose_pr H). set (K := choose (property p)) in *. unfold property in (type of p0). pose (p0 y); xd. Qed. 

Lemma inc_create :
 forall (p : EP) (y : E), axioms p -> inc y (create p) = p y. 
ir. 
ap iff_eq; ir. ap lem1; am. 
ap lem2; am. 
Qed. 

Lemma trans_criterion :
 forall (p : EP) (f : E1) (x : E),
 (forall y : E, p y -> ex (fun z : E => A (inc z x) (f z = y))) ->
 axioms p.
ir. 
ap criterion. 
sh (Image.create x f). 
ir. ap Image.show_inc. ap H. am. 
Qed. 

Lemma little_criterion :
 forall (p : EP) (x : E) (f : x -> E),
 (forall y : E, p y -> exists a : x, f a = y) -> axioms p. 
ir. 
ap criterion; sh (IM f). 
ir. ap IM_inc. ap H; am. 
Qed. 


End Bounded.


Module Quotient.


Definition is_part (a : E) (r : E2P) (y : E) :=
sub y a
& (forall x z : E, inc x y -> r x z -> inc z a -> inc z y)
& (forall x z : E, inc x y -> r z x -> inc z a -> inc z y). 

Definition is_class (a : E) (r : E2P) (y : E) :=
is_part a r y
& nonempty y
& (forall z : E, 
        is_part a r z -> nonempty (intersection2 y z) -> sub y z).

Lemma lem1 : forall (a : E) (r : E2P), is_part a r a.
ir.
unfold is_part in |- *; xd.
unfold sub in |- *; ir; au.
Qed.

Definition parts_containing (a : E) (r : E2P) (y : E) :=
  Z (powerset a) (fun z : E => (is_part a r z & inc y z)). 


Definition class_of (a : E) (r : E2P) (y : E) :=
  intersection (parts_containing a r y). 

Lemma inc_parts_containing :
 forall (a : E) (r : E2P) (y z : E),
 inc y z -> is_part a r z -> inc z (parts_containing a r y). 
ir. unfold parts_containing in |- *. ap Z_inc. 
ap powerset_inc. unfold is_part in H0; xd. 
xd. Qed. 

Lemma class_of_origin :
 forall (a : E) (r : E2P) (y : E), inc y a -> inc y (class_of a r y). 
ir. unfold class_of in |- *. ap intersection_inc. 
apply nonempty_intro with a. ap inc_parts_containing. 
am. ap lem1. ir. 
unfold parts_containing in H0. cp (Z_pr H0). cbv beta in H1.
xd; au. Qed. 


Lemma class_of_sub :
 forall (a : E) (r : E2P) (y z : E),
 inc y z -> is_part a r z -> sub (class_of a r y) z. 
ir. unfold class_of in |- *. ap intersection_sub. 
ap inc_parts_containing; au. Qed. 




Lemma class_of_part :
 forall (a : E) (r : E2P) (y : E), inc y a -> is_part a r (class_of a r y).
ir.
unfold is_part in |- *; xd; ir.
unfold class_of in |- *.
ap intersection_sub.
unfold parts_containing in |- *.
ap Z_inc.
ap powerset_inc.
unfold sub in |- *; ir; au.

xd.
ap lem1.

unfold class_of in |- *.
ap intersection_inc.
apply nonempty_intro with a.
unfold parts_containing in |- *.
ap Z_inc.
ap powerset_inc; unfold sub in |- *; ir; au.

xd.
ap lem1.


ir.
assert (is_part a r y0).
unfold parts_containing in H3.

cp (Z_pr H3). cbv beta in H4. 
xd.

unfold is_part in H4; xd.
apply H5 with x.
apply intersection_forall with (parts_containing a r y).
exact H0. am. am. am. 


unfold class_of in |- *.
ap intersection_inc.
apply nonempty_intro with a.
unfold parts_containing in |- *.
ap Z_inc.
ap powerset_inc; unfold sub in |- *; ir; au.

xd.
ap lem1.


ir.
assert (is_part a r y0).
unfold parts_containing in H3.

cp (Z_pr H3). cbv beta in H4. 
xd.

unfold is_part in H4; xd.
apply H6 with x.
apply intersection_forall with (parts_containing a r y).
exact H0.
am. am. am.

Qed.

Ltac Inbeta v :=
  match goal with
  | v:?X1 |- _ =>
      assert (inbeta_identx : X1);
       [ exact v
       | clear v; cbv beta in inbeta_identx; cp inbeta_identx;
          clear inbeta_identx ]
  end.

Ltac zpr b := set (zpr_identx := Z_pr b); Inbeta zpr_identx.

Ltac chpr b := set (zpr_identx := choose_pr b); Inbeta zpr_identx.


Lemma class_of_class :
 forall (a : E) (r : E2P) (y : E), inc y a -> is_class a r (class_of a r y).
ir.
unfold is_class in |- *; xd; ir.
ap class_of_part.
am.

apply nonempty_intro with y.
unfold class_of in |- *.
ap intersection_inc.
apply nonempty_intro with a.
unfold parts_containing in |- *; ap Z_inc; xd.
ap powerset_inc; unfold sub in |- *; ir; au.

ap lem1.

ir.
unfold parts_containing in H0.
zpr H0. 
xd.

unfold class_of in |- *.
ap intersection_sub.
unfold parts_containing in |- *.
ap Z_inc.
ap powerset_inc.
unfold is_part in H0.
xd.

xd.
nin H1.
pose (intersection2_first H1).
pose (intersection2_second H1).
ap excluded_middle; unfold not in |- *; ir.
pose (Z (class_of a r y) (fun v : E => inc v z -> False)). 
assert (is_part a r e). unfold is_part in |- *. 
xd. apply sub_trans with (class_of a r y). 
unfold e in |- *; ap Z_sub. unfold sub in |- *; ir. 
unfold class_of in H3. apply intersection_forall with (parts_containing a r y). am. unfold parts_containing in |- *. 
ap Z_inc. ap powerset_inc; unfold sub in |- *; ir; au. xd; try ap lem1; au. 

ir. unfold e in |- *; Ztac. unfold class_of in |- *. 
ap intersection_inc; ir. 
apply nonempty_intro with a.
unfold parts_containing in |- *; Ztac; xd.
ap powerset_inc; unfold sub in |- *; ir; au.

ap lem1. unfold parts_containing in H6. 
zpr H6. xd. assert (inc x (class_of a r y)). 
assert (sub e (class_of a r y)). unfold e in |- *; ap Z_sub. 
ap H9. am. unfold class_of in H9. 
assert (inc x y1). apply intersection_forall with (parts_containing a r y). am. unfold parts_containing in |- *; ap Z_inc. ap powerset_inc. 
unfold is_part in H7; xd; au. xd. 
unfold is_part in H7; xd. apply H11 with x; am. 
ir. assert (inc x z). unfold is_part in H0; xd. 
apply H8 with z0; au. assert (sub e a). 
apply sub_trans with (class_of a r y). 
unfold e in |- *; ap Z_sub. ap class_of_sub. 
am. ap lem1. ap H9; am. 
unfold e in H3. zpr H3. 
ap H8; am. 
ir. unfold e in |- *; ap Z_inc. 
assert (sub e (class_of a r y)). unfold e in |- *; ap Z_sub. 
ap H6. unfold e in |- *; ap Z_inc. 
assert (is_part a r (class_of a r y)). ap class_of_part.
am. unfold is_part in H7.
xd. apply H9 with x. ap H6. am. 
am. am. ir. assert (inc x z). 
unfold is_part in H0; xd. apply H8 with z0. 
am. am. assert (sub e a). apply sub_trans with (class_of a r y). unfold e in |- *; ap Z_sub. 
ap class_of_sub. am. ap lem1. ap H10; am. unfold e in H3. zpr H3. 
ap H9; am. 
ir.
assert (inc x z). unfold is_part in H0; xd. 
apply H7 with z0; au. assert (sub e a).
apply sub_trans with (class_of a r y). unfold e in |- *; ap Z_sub. 
ap class_of_sub. am. ap lem1.
ap H9; au. unfold e in H3. zpr H3. 
ap H8; au. assert (sub (class_of a r y) e). 
ap class_of_sub. unfold e in |- *; ap Z_inc. 
ap class_of_origin; au. am. am.
assert (inc y0 e).
ap H4. am. unfold e in H5. 
zpr H5. ap H6; au. 
Qed. 


Lemma class_rep_inc :
 forall (a : E) (r : E2P) (x : E), is_class a r x -> inc (rep x) x. 
ir. unfold is_class in H. xd. unfold rep in |- *. 
ap choose_pr. nin H0. 
apply ex_intro with y; au. Qed. 

Lemma class_eq_class_of :
 forall (a : E) (r : E2P) (y : E),
 is_class a r y -> forall x : E, inc x y -> class_of a r x = y.
ir. ap extensionality. ap class_of_sub; au. 
unfold is_class in H; xd; au. unfold is_class in H. 
xd. ap H2. ap class_of_part. unfold is_part in H; xd. apply nonempty_intro with x. 
ap intersection2_inc; au. ap class_of_origin. 
unfold is_part in H; xd. Qed. 






Lemma intersecting_classes_eq :
 forall (a : E) (r : E2P) (x y : E),
 is_class a r x -> is_class a r y -> nonempty (intersection2 x y) -> x = y.
ir. pose (class_eq_class_of H). pose (class_eq_class_of H0). 
nin H1. pose (intersection2_first H1). 
pose (intersection2_second H1). 
pose (e _ i). pose (e0 _ i0).
rewrite <- e1. rewrite <- e2.
tv. Qed.  


Lemma intersecting_classes_of_eq :
 forall (a : E) (r : E2P) (x y : E),
 inc x a ->
 inc y a ->
 nonempty (intersection2 (class_of a r x) (class_of a r y)) ->
 class_of a r x = class_of a r y.
ir.
pose class_of_class.
apply intersecting_classes_eq with a r; au.
Qed.



Definition quotient (a : E) (r : E2P) :=
  Z (powerset a) (fun y : E => is_class a r y).

Lemma in_quotient_is_class :
 forall (a : E) (r : E2P) (x : E), inc x (quotient a r) -> is_class a r x.
ir. unfold quotient in H. zpr H; au. 
Qed. 

Lemma is_class_in_quotient :
 forall (a : E) (r : E2P) (x : E), is_class a r x -> inc x (quotient a r).
ir. unfold quotient in |- *; ap Z_inc. 
ap powerset_inc. unfold is_class in H.
xd. unfold is_part in H; xd; au. am. 
Qed.


Lemma class_of_in_quotient :
 forall (a : E) (r : E2P) (x : E),
 inc x a -> inc (class_of a r x) (quotient a r).
ir. unfold quotient in |- *; ap Z_inc.
ap powerset_inc. ap class_of_sub; au. 
ap lem1. ap class_of_class; au. 
Qed. 


Lemma inc_class_of :
 forall (a : E) (r : E2P) (x y : E),
 inc x a -> inc y a -> r x y -> inc x (class_of a r y).
ir.
assert (is_part a r (class_of a r y)).
ap class_of_part.
am.

unfold is_part in H2.
xd.
set (x_ := class_of_origin).
apply H4 with y; au.
Qed.

Lemma related_classes_eq :
 forall (a : E) (r : E2P) (x y : E),
 inc x a -> inc y a -> r x y -> class_of a r x = class_of a r y.
ir.
ap intersecting_classes_of_eq; au.
apply nonempty_intro with x.
pose class_of_origin.
pose inc_class_of.
ap intersection2_inc; au.
Qed.


Definition class_in (q x : E) := choose (fun y : E => A (inc y q) (inc x y)).



Lemma class_of_eq_class :
 forall (a : E) (r : E2P) (x : E),
 inc x a -> class_of a r x = class_in (quotient a r) x.
ir. ap class_eq_class_of. 
assert (inc (class_in (quotient a r) x) (quotient a r)). 
unfold class_in in |- *. 
assert (ex (fun y : E => A (inc y (quotient a r)) (inc x y))). 
apply ex_intro with (class_of a r x). 
xd. ap class_of_in_quotient; au. 
ap class_of_origin; au. 
chpr H0. xd. unfold quotient in H0. 
zpr H0. am. 
assert (ex (fun y : E => A (inc y (quotient a r)) (inc x y))).
apply ex_intro with (class_of a r x). 
xd. ap class_of_in_quotient; au. 
ap class_of_origin; au. 
chpr H0. xd.  
Qed.

Lemma class_of_rep :
 forall (a : E) (r : E2P) (x : E),
 inc x (quotient a r) -> class_of a r (rep x) = x. 
ir. ap class_eq_class_of. ap in_quotient_is_class; au.
assert (is_class a r x). ap in_quotient_is_class; au.
unfold is_class in H0; xd. 
unfold rep in |- *. nin H1. ap choose_pr. 
apply ex_intro with y. am. 
Qed. 


Definition is_eq_reln (a : E) (r : E2P) :=
  (forall x : E, inc x a -> r x x)
& (forall x y : E, inc x a -> inc y a -> r x y -> r y x)
& (forall x y z : E,
        inc x a -> inc y a -> inc z a -> r x y -> r y z -> r x z).

Definition equivalent (a : E) (r : E2P) (x y : E) :=
  inc x a
& inc y a
& class_of a r x = class_of a r y.

Lemma equivalent_symm :
 forall (a : E) (r : E2P) (x y : E), equivalent a r x y -> equivalent a r y x.
ir.
unfold equivalent in H.
unfold equivalent in |- *. xd.
Qed.

Lemma equivalent_refl :
 forall (a : E) (r : E2P) (x : E), inc x a -> equivalent a r x x.
ir; unfold equivalent in |- *; xd.
Qed.

Lemma equivalent_trans :
 forall (a : E) (r : E2P) (x y z : E),
 equivalent a r x y -> equivalent a r y z -> equivalent a r x z.
unfold equivalent in |- *; ir; xd.
transitivity (class_of a r y); au.
Qed.

Lemma equivalent_is_eq_reln :
 forall (a : E) (r : E2P), is_eq_reln a (equivalent a r).
ir.
unfold is_eq_reln in |- *; xd; ir.
ap equivalent_refl; au.
ap equivalent_symm; au.
apply equivalent_trans with y; au.
Qed.

Lemma related_equivalent :
 forall (a : E) (r : E2P) (x y : E),
 inc x a -> inc y a -> r x y -> equivalent a r x y.
ir.
unfold equivalent in |- *; xd.
ap intersecting_classes_of_eq; au.
apply nonempty_intro with x.
ap intersection2_inc.
ap class_of_origin; au.
ap inc_class_of; au.
Qed.

Lemma equivalent_related :
 forall (a : E) (r : E2P) (x y : E),
 is_eq_reln a r -> equivalent a r x y -> r x y.
ir.
unfold is_eq_reln in H; xd.
set (z := Z a (fun u : E => r x u)).
assert (inc y z).
unfold equivalent in H0; xd.
assert (sub (class_of a r y) z).
rewrite <- H4.
ap class_of_sub.
unfold z in |- *; Ztac.

unfold is_part in |- *; xd.
unfold z in |- *; ap Z_sub.

ir.
unfold z in |- *; Ztac.
apply H2 with x0.
am.

assert (sub z a); [ unfold z in |- *; ap Z_sub | ap H8; au ].

au.

unfold z in H5; Ztac.

am.

ir.
unfold z in |- *; Ztac.
apply H2 with x0; au.
assert (sub z a); [ unfold z in |- *; ap Z_sub | ap H8; au ].

unfold z in H5; Ztac.

ap H1; au.
assert (sub z a); [ unfold z in |- *; ap Z_sub | ap H8; au ].

ap H5.
ap class_of_origin.
am.

unfold z in H3; Ztac.
Qed.


Lemma equivalent_to_rep :
 forall (a : E) (r : E2P) (x : E),
 inc x a -> equivalent a r x (rep (class_of a r x)).
ir.
unfold equivalent in |- *; xd.
assert (sub (class_of a r x) a).
ap class_of_sub; au.
ap lem1.

ap H0.
ap nonempty_rep.
apply nonempty_intro with x; ap class_of_origin.
am.

ap intersecting_classes_of_eq.
am.

assert (sub (class_of a r x) a).
set (x_ := lem1); ap class_of_sub; au.

ap H0.
ap nonempty_rep.
apply nonempty_intro with x; ap class_of_origin.
am.

apply nonempty_intro with (rep (class_of a r x)).
ap intersection2_inc.
ap nonempty_rep.
apply nonempty_intro with x; ap class_of_origin.
am.

ap class_of_origin.
assert (sub (class_of a r x) a).
ap class_of_sub.
au.

ap lem1.

ap H0.
ap nonempty_rep.
apply nonempty_intro with x.
ap class_of_origin.
am.
Qed.

Lemma equivalent_universal :
 forall (a : E) (r s : E2P),
 is_eq_reln a s ->
 (forall x y : E, inc x a -> inc y a -> r x y -> s x y) ->
 forall x y : E, equivalent a r x y -> s x y.
ir.
set (z := Z a (fun u : E => s x u)).
assert (sub z a).
unfold z in |- *; ap Z_sub.

unfold sub in H2.
unfold equivalent in H1; xd.
assert (sub (class_of a r y) z).
rewrite <- H4.
ap class_of_sub.
unfold z in |- *; Ztac.
unfold is_eq_reln in H; xd.

unfold is_part in |- *; xd.
ir.
unfold z in |- *; Ztac.
unfold is_eq_reln in H; xd.
apply H9 with x0; au.
unfold z in H5; Ztac.

ir.
unfold z in |- *; Ztac.
unfold is_eq_reln in H; xd.
apply H9 with x0; au.
unfold z in H5; Ztac.

assert (inc y z).
ap H5; ap class_of_origin.
au.

unfold z in H6; Ztac.
Qed.

Definition quotient_endo (q : E) (endo : E1) (x : E) :=
  class_in q (endo (rep x)).

Definition endo_within (a : E) (endo : E1) :=
  forall x : E, inc x a -> inc (endo x) a.

Definition endo_compatible (a : E) (r : E2P) (endo : E1) :=
  forall x y : E, inc x a -> inc y a -> r x y -> r (endo x) (endo y).

Definition endo_passes_to_quotient (q : E) (endo : E1) :=
  forall x a : E,
  inc x q -> inc a x -> class_in q (endo a) = quotient_endo q endo x.

Lemma endo_compatible_passes :
 forall (a : E) (r : E2P) (endo : E1),
 endo_within a endo ->
 endo_compatible a r endo -> endo_passes_to_quotient (quotient a r) endo.
ir.
unfold endo_passes_to_quotient in |- *.
set (q := quotient a r) in *.
ir.
assert (is_class a r x).
ap in_quotient_is_class.
am.

assert (class_of a r (rep x) = x).
ap class_of_rep.
am.

assert (class_of a r a0 = x).
ap class_eq_class_of.
am.

am.

set (z := Z a (fun u : E => class_in q (endo u) = quotient_endo q endo x)).
assert (sub z a). unfold z in |- *; ap Z_sub.

assert (sub (class_of a r (rep x)) z).
ap class_of_sub.
unfold z in |- *; Ztac.
unfold is_class in H3.
xd.
unfold is_part in H3; xd.
ap H3.
ap nonempty_rep.
am.

unfold is_part in |- *; xd.
ir.
unfold z in |- *; Ztac.
transitivity (class_in q (endo x0)).
unfold q in |- *.
assert (inc x0 a).
ap H6; au.

rewrite <- class_of_eq_class.
rewrite <- class_of_eq_class.
sy.
ap related_classes_eq.
ap H.
am.

ap H; am.

ap H0; au.

ap H.
au.

ap H; au.

unfold z in H7; Ztac.

ir.
unfold z in |- *; Ztac.
transitivity (class_in q (endo x0)).
assert (inc x0 a).
ap H6; au.

unfold q in |- *.
rewrite <- class_of_eq_class.
rewrite <- class_of_eq_class.
ap related_classes_eq.
ap H; au.

ap H; au.

ap H0; au.

ap H; au.

ap H; au.

unfold z in H7; Ztac.

assert (inc a0 z).
ap H7.
rewrite H4; au.

unfold z in H8; Ztac.
Qed.

Definition quotient_op (q : E) (op : E2) (x y : E) :=
  class_in q (op (rep x) (rep y)).

Definition op_within (a : E) (op : E2) :=
  forall x y : E, inc x a -> inc y a -> inc (op x y) a.

Definition op_left_compatible (a : E) (r : E2P) (op : E2) :=
  forall x y z : E,
  inc x a -> inc y a -> inc z a -> r x z -> r (op x y) (op z y).

Definition op_right_compatible (a : E) (r : E2P) (op : E2) :=
  forall x y z : E,
  inc x a -> inc y a -> inc z a -> r y z -> r (op x y) (op x z).

Definition op_passes_to_quotient (q : E) (op : E2) :=
  forall x y a b c d : E,
  inc x q ->
  inc y q -> inc a x -> inc b y -> class_in q (op a b) = quotient_op q op x y. 



Lemma op_left_very_compatible :
 forall (a : E) (r : E2P) (op : E2),
 op_within a op ->
 op_left_compatible a r op ->
 forall x b c d : E,
 inc x (quotient a r) ->
 inc b x ->
 inc c x ->
 inc d a ->
 class_in (quotient a r) (op b d) = class_in (quotient a r) (op c d).
ir.
set (f := fun u : E => op u d).
assert (endo_within a f).
unfold endo_within in |- *.
ir.
unfold f in |- *.
ap H; au.

assert (endo_compatible a r f).
unfold endo_compatible in |- *.
ir.
unfold f in |- *.
ap H0; au.

pose (endo_compatible_passes H5 H6).
unfold endo_passes_to_quotient in (type of e).
unfold f in (type of e).
transitivity (quotient_endo (quotient a r) (fun u : E => op u d) x).
ap e; au.

sy.
ap e; au.
Qed. 

Lemma op_right_very_compatible :
 forall (a : E) (r : E2P) (op : E2),
 op_within a op ->
 op_right_compatible a r op ->
 forall x b c d : E,
 inc x (quotient a r) ->
 inc b a ->
 inc c x ->
 inc d x ->
 class_in (quotient a r) (op b c) = class_in (quotient a r) (op b d).
ir.
set (f := fun u : E => op b u).
assert (endo_within a f).
unfold endo_within in |- *.
ir.
unfold f in |- *.
ap H; au.

assert (endo_compatible a r f).
unfold endo_compatible in |- *.
ir.
unfold f in |- *.
ap H0; au.

pose (endo_compatible_passes H5 H6).
unfold endo_passes_to_quotient in (type of e).
unfold f in (type of e).
transitivity (quotient_endo (quotient a r) (fun u : E => op b u) x).
ap e; au.

sy.
ap e; au.
Qed. 



Lemma op_compatible_passes :
 forall (a : E) (r : E2P) (op : E2),
 op_within a op ->
 op_left_compatible a r op ->
 op_right_compatible a r op -> op_passes_to_quotient (quotient a r) op.
ir.
unfold op_passes_to_quotient in |- *; ir.
unfold quotient_op in |- *.
assert (inc (rep x) x).
ap nonempty_rep.
apply nonempty_intro with a0.
am.

assert (inc (rep y) y).
ap nonempty_rep; apply nonempty_intro with b; au.

transitivity (class_in (quotient a r) (op a0 (rep y))).
apply op_right_very_compatible with y; au.
assert (inc x (powerset a)).
unfold quotient in H2; Ztac.

assert (sub x a).
ap powerset_sub.
am.

ap H9.
am.

apply op_left_very_compatible with x; au.
assert (sub y a).
ap powerset_sub.
unfold quotient in H3; Ztac.

ap H8; au.
Qed.

End Quotient.



Module Cartesian.

Definition in_record (a : E) (f : E1) (x : E) :=
  is_pair x
& inc (pr1 x) a
& inc (pr2 x) (f (pr1 x)).

Record recordRec (a : E) (f : E1) : E :=  {first : a; second : f (R first)}.

Definition recordMap (a : E) (f : E1) (i : recordRec a f) :=
  pair (R (first i)) (R (second i)).

Lemma in_record_ex :
 forall (a : E) (f : E1) (x : E),
 in_record a f x -> exists i : recordRec a f, recordMap i = x.
ir.
unfold in_record in H; xd.
set (u := B H0).
assert (R u = pr1 x).
unfold u in |- *.
ap B_eq.

assert (inc (pr2 x) (f (R u))).
rewrite H2; am.

set (v := B H3).
pose (Build_recordRec (a:=a) (f:=f) (first:=u) v).
apply ex_intro with r.
transitivity (pair (R u) (R v)).
tv.

assert (R v = pr2 x).
unfold v in |- *.
ap B_eq.

rewrite H4.
assert (R u = pr1 x); au.
rewrite H5.
ap pair_recov.
am.
Qed.

Lemma in_record_bounded :
 forall (a : E) (f : E1), Bounded.axioms (in_record a f).
ir.
ap Bounded.criterion.
apply ex_intro with (IM (recordMap (a:=a) (f:=f))).
ir.
ap IM_inc.
ap in_record_ex.
am.
Qed.

Definition record (a : E) (f : E1) := Bounded.create (in_record a f).

Lemma record_in :
 forall (a : E) (f : E1) (x : E), inc x (record a f) -> in_record a f x.
ir.
unfold record in H.
pose (in_record_bounded a f).
pose (Bounded.lem1 a0 H).
am.
Qed.

Lemma record_pr :
 forall (a : E) (f : E1) (x : E),
 inc x (record a f) ->
 (is_pair x & inc (pr1 x) a & inc (pr2 x) (f (pr1 x))).
ir. pose (record_in H). am.
Qed.

Lemma record_inc :
 forall (a : E) (f : E1) (x : E), in_record a f x -> inc x (record a f).
ir.
unfold record in |- *.
ap Bounded.lem2.
ap in_record_bounded.
am.
Qed.

Lemma record_pair_pr :
 forall (a : E) (f : E1) (x y : E),
 inc (pair x y) (record a f) -> (inc x a & inc y (f x)).
ir.
xd.
pose (record_in H).
unfold in_record in (type of i); xd.
rewrite pr1_pair in H1.
am.

pose (record_in H).
unfold in_record in (type of i); xd.
rewrite pr1_pair in H2.
rewrite pr2_pair in H2.
am.
Qed.

Lemma record_pair_inc :
 forall (a : E) (f : E1) (x y : E),
 inc x a -> inc y (f x) -> inc (pair x y) (record a f).
ir.
ap record_inc.
unfold in_record in |- *; xd.
ap pair_is_pair.
rewrite pr1_pair; am.
rewrite pr2_pair; rewrite pr1_pair; am.
Qed.

Definition product (a b : E) := record a (fun x : E => b).

Lemma product_pr :
 forall a b u : E,
 inc u (product a b) -> (is_pair u & inc (pr1 u) a & inc (pr2 u) b).
ir. unfold product in H. pose (record_pr H). xd.
Qed.

Lemma product_inc :
 forall a b u : E,
 is_pair u -> inc (pr1 u) a -> inc (pr2 u) b -> inc u (product a b).
ir. unfold product in |- *. ap record_inc. unfold in_record in |- *; xd.
Qed.

Lemma product_pair_pr :
 forall a b x y : E, inc (pair x y) (product a b) -> (inc x a & inc y b).
ir. unfold product in H. pose (record_pair_pr H). am.
Qed.

Lemma product_pair_inc :
 forall a b x y : E, inc x a -> inc y b -> inc (pair x y) (product a b).
ir. unfold product in |- *. ap record_pair_inc; au.
Qed.


End Cartesian.

Export Cartesian.


Module Relation.
Export Quotient.

Definition is_relation r :=
forall y, inc y r -> is_pair y.

Definition substrate r :=
union2 (Image.create r pr1) (Image.create r pr2).

Lemma inc_pr1_substrate : forall r y,
inc y r -> inc (pr1 y) (substrate r).
Proof.
ir. uf substrate. 
ap union2_first. 
rw Image.inc_rw. 
sh y. ee. am. tv. 
Qed.

Lemma inc_pr2_substrate : forall r y,
inc y r -> inc (pr2 y) (substrate r).
Proof.
ir. uf substrate. 
ap union2_second. 
rw Image.inc_rw. 
sh y. ee. am. tv. 
Qed.

Lemma substrate_smallest : forall r s,
(forall y, inc y r -> inc (pr1 y) s) ->
(forall y, inc y r -> inc (pr2 y) s) ->
sub (substrate r) s.
Proof.
ir. uhg; ir. ufi substrate H1. 
cp (union2_or H1). 
nin H2. rwi Image.inc_rw H2. nin H2. ee. 
wr H3. ap H. am. 
 rwi Image.inc_rw H2. nin H2. ee. 
wr H3. ap H0. am. 
Qed.

Lemma inc_substrate : forall r x,
is_relation r ->
inc x (substrate r) =
((exists y, inc (pair x y) r) \/
(exists y, inc (pair y x) r)).
Proof.
ir. ap iff_eq; ir. ufi substrate H0. 
cp (union2_or H0). nin H1. ap or_introl. 
rwi Image.inc_rw H1. nin H1. ee. 
sh (pr2 x0). 
assert (pair x (pr2 x0) = x0). wr H2. 
uh H; ee. cp (H _ H1). uh H3. 
nin H3. nin H3. rw H3. rw pr1_pair. 
rw pr2_pair. tv. rww H3. 

ap or_intror. 
rwi Image.inc_rw H1. nin H1. ee. 
sh (pr1 x0). 
assert (pair (pr1 x0) x = x0). wr H2. 
uh H; ee. cp (H _ H1). uh H3. 
nin H3. nin H3. rw H3. rw pr1_pair. 
rw pr2_pair. tv. rww H3. 

nin H0. nin H0. assert (x = pr1 (pair x x0)). 
rww pr1_pair. rw H1. app inc_pr1_substrate. 

nin H0. assert (x = pr2 (pair x0 x)). 
rww pr2_pair. rw H1. app inc_pr2_substrate. 
Qed. 

Definition related r x y := inc (pair x y) r.

Definition is_reflexive r :=
is_relation r & (forall y, inc y (substrate r) ->related r y y).

Lemma reflexive_inc_substrate : forall r x,
is_reflexive r -> 
inc x (substrate r) = inc (pair x x) r.
Proof.
ir. ap iff_eq; ir. uh H; ee. 
cp (H1 _ H0). am. 
rw inc_substrate. ap or_introl. sh x. am. 
lu. 
Qed. 

Lemma reflexive_ap :
forall r x, is_reflexive r -> inc x (substrate r) ->
related r x x.
Proof.
ir. uh H; ee. cp (H1 _ H0). am. 
Qed. 

Definition is_transitive r :=
is_relation r & 
(forall x y z, related r x y -> related r y z -> related r x z).

Lemma transitive_ap : forall r x z,
is_transitive r -> 
(exists y, related r x y & related r y z) ->
related r x z. 
Proof.
ir. nin  H0. uh H; ee. ap (H2 x x0). am. am. 
Qed. 

Definition is_symmetric r :=
is_relation r & 
(forall x y, related r x y -> related r y x).

Lemma symmetric_ap : forall r x y,
is_symmetric r -> related r x y -> related r y x.
Proof.
ir. uh H; ee; au. 
Qed. 

Definition is_equivalence_relation r :=
is_relation r & is_reflexive r & is_transitive r &
is_symmetric r.

Lemma relation_intersection : forall z,
nonempty z -> (forall r, inc r z -> is_relation r) ->
is_relation (intersection z).
Proof.
ir. uhg; ee. ir. 
unfold is_relation in H0. 
nin H. apply H0 with y0. am. 
apply intersection_forall with z. am. am. 
Qed.

Lemma related_intersection : forall z x y,
nonempty z ->
related (intersection z) x y = 
(forall r, inc r z -> related r x y). 
Proof.
ir. ap iff_eq; ir. 
uh H0. uhg. apply intersection_forall with z. am. 
am. 
uhg. app intersection_inc. 
Qed. 

Lemma substrate_sub : forall r s, sub r s ->
sub (substrate r) (substrate s).
Proof.
ir. uhg; ir. uf substrate. 
ufi substrate H0. 
cp (union2_or H0). nin H1. ap union2_first. 
rwi Image.inc_rw H1. rw Image.inc_rw. nin H1. 
sh x0; ee. app H. am. 
ap union2_second. 
rwi Image.inc_rw H1. rw Image.inc_rw. nin H1. 
sh x0; ee. app H. am. 
Qed. 

Lemma substrate_intersection_sub : forall r z,
inc r z -> sub (substrate (intersection z)) (substrate r).
Proof.
ir. ap substrate_sub. uhg; ir. 
apply intersection_forall with z. am. am. 
Qed.

Lemma reflexive_intersection : forall z,
nonempty z -> (forall r, inc r z -> is_reflexive r) ->
is_reflexive (intersection z).
Proof.
ir. uhg; ee. 
app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. 
ir. 
rw related_intersection. ir. cp (H0 _ H2).
uh H3; ee. ap H4. 
assert (sub (substrate (intersection z)) (substrate r)). 
app substrate_sub. uhg; ir. apply intersection_forall
with z. am. am. ap H5. am. am. 
Qed.

Lemma transitive_intersection : forall z,
nonempty z -> (forall r, inc r z -> is_transitive r) ->
is_transitive (intersection z).
Proof.
ir. uhg; ee. 
app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. 

ir. 
rww related_intersection.  ir. 
rwi related_intersection H1; rwi related_intersection H2. 
cp (H0 _ H3). uh H4; ee. 
apply H5 with y. au. au. am. am. am. 
Qed.

Lemma symmetric_intersection : forall z,
nonempty z -> (forall r, inc r z -> is_symmetric r) ->
is_symmetric (intersection z).
Proof.
ir. uhg; ee. 
app relation_intersection. ir. cp (H0 _ H1). uh H2; ee; am. 

ir. 
rww related_intersection.  ir. 
rwi related_intersection H1. 
cp (H0 _ H2). uh H3; ee. 
ap H4. au. au.  
Qed.

Lemma symmetric_transitive_reflexive : forall r,
is_symmetric r -> is_transitive r -> is_reflexive r.
Proof.
ir. uhg; ee. uh H; ee; am. 
ir. rwi inc_substrate H1. nin H1. nin H1. 
app transitive_ap. sh x. 
ee. am. app symmetric_ap. 

nin H1. app transitive_ap. sh x. ee. 
app symmetric_ap. am. uh H; ee; am. 
Qed. 

Lemma show_equivalence_relation : forall r,
is_relation r ->
(forall x y, related r x y -> related r y x) ->
(forall x y z, related r x y -> related r y z -> related r x z) ->
is_equivalence_relation r.
Proof.
ir. assert (is_symmetric r). 
uhg; ee; am. 
assert  (is_transitive r). 
uhg; ee; am. uhg; ee; try am. app symmetric_transitive_reflexive.
Qed. 

Lemma symmetric_transitive_equivalence : forall r,
is_symmetric r -> is_transitive r -> is_equivalence_relation r.
Proof.
ir. uhg; ee. 
uh H; ee; am. app symmetric_transitive_reflexive.
am. am. 
Qed. 


Lemma equivalence_relation_intersection : forall z,
nonempty z -> (forall r, inc r z -> is_equivalence_relation r) ->
is_equivalence_relation (intersection z).
Proof.
ir. ap symmetric_transitive_equivalence. 
app symmetric_intersection. ir. 
cp (H0 _ H1). lu. 
app transitive_intersection. ir. 
cp (H0 _ H1). lu. 
Qed.

Definition class r x := Image.create (Z r (fun y => pr1 y = x)) pr2.

Lemma is_pair_rw : forall x, is_pair x = (x = pair (pr1 x) (pr2 x)).
Proof.
ir. ap iff_eq. ir. cp (pair_recov H). uh H0. 
sy; am. ir. rw H. ap pair_is_pair. 
Qed. 

Lemma inc_class : forall r x y,
is_relation r -> inc y (class r x) = related r x y.
Proof.
ir. uf class. 
rw Image.inc_rw. ap iff_eq; ir. 
nin H0. ee. Ztac. assert (x0 = pair x y).
uh H; ee. cp (H _ H2). rwi is_pair_rw H4. 
rw H4. rw H1; rww H3. uhg. wrr H4. 

sh (pair x y). ee. app Z_inc. rww pr1_pair. rww pr2_pair. 
Qed. 

Lemma nonempty_class_symmetric : forall r x,
is_symmetric r -> 
nonempty (class r x) = inc x (substrate r).
Proof.
ir. ap iff_eq; ir. rw inc_substrate. 
nin H0. rwi inc_class H0. 
ap or_introl. sh y. am. lu. lu. 
rwi inc_substrate H0. nin H0. 
nin H0. sh x0. rw inc_class. am. lu. 
nin H0. sh x0. rw inc_class. app symmetric_ap. 
lu. lu. 
Qed. 

Lemma related_product : forall a b x y,
related (product a b) x y = (inc x a & inc y b).
Proof.
ir. ap iff_eq; ir. 
uh H. cp (product_pr H). 
rwi pr1_pair H0; rwi pr2_pair H0; xd. 

uhg. ee; app product_pair_inc. 
Qed. 

Lemma full_equivalence_relation : forall b,
is_equivalence_relation (Cartesian.product b b).
Proof.
ir. ap show_equivalence_relation.
uhg. ir. cp (Cartesian.product_pr H). 
ee; am. 
ir. 
rwi related_product H. rw related_product; xd. 

ir. rwi related_product H; rwi related_product H0. 
rw related_product; xd. 
Qed. 


Lemma related_class_eq : forall r u v,
is_equivalence_relation r ->
related r u u -> 
related r u v = (class r u = class r v).
Proof.
ir. 
ap iff_eq; ir. ap extensionality; uhg; ir. 
rwi inc_class H2. rw inc_class. 
ap transitive_ap. lu. sh u. ee. 
ap symmetric_ap. lu. am. am. lu. lu. 
rwi inc_class H2. rw inc_class. ap transitive_ap.
lu. sh v. ee; try am. lu. lu. 
wri inc_class H0. rwi H1 H0. 
rwi inc_class H0. ap symmetric_ap. 
lu. am. lu. lu. 
Qed. 

End Relation.


Module Function_Set.

Definition in_function_set (a : E) (f : E1) (u : E) :=
  Function.axioms u
& Function.domain u = a
& (forall y : E, inc y a -> inc (V y u) (f y)).

Lemma in_fs_sub_record :
 forall (a : E) (f : E1) (u : E), in_function_set a f u -> sub u (record a f).
ir.
unfold in_function_set in H; xd.
unfold sub in |- *; ir.
pose (Function.pr2_V H H2).
assert (Function.axioms u).
am.

unfold Function.axioms in H3; xd.
pose (H3 _ H2).
rewrite <- e0.
ap record_pair_inc.
rewrite <- H0.
ap Function.lem2; au.

rewrite e.
ap H1.
rewrite <- H0.
ap Function.lem2; au.
Qed.

Lemma in_fs_eq_L :
 forall (a : E) (f : E1) (u : E),
 in_function_set a f u -> u = Function.create a (fun y : E => V y u).
ir.
unfold in_function_set in H; xd.
rewrite <- H0.
sy.
ap Function.create_recovers.
am.
Qed.

Lemma in_fs_for_L :
 forall (a : E) (f v : E1),
 (forall y : E, inc y a -> inc (v y) (f y)) ->
 in_function_set a f (Function.create a v).
ir.
unfold in_function_set in |- *; xd.
ap Function.create_axioms.

ap Function.create_domain.

ir.
rewrite Function.create_V_rewrite.
ap H; au.

am.
Qed.

Lemma in_fs_bounded :
 forall (a : E) (f : E1), Bounded.axioms (in_function_set a f).
ir.
ap Bounded.criterion.
apply ex_intro with (powerset (record a f)).
ir.
ap powerset_inc.
ap in_fs_sub_record; au.
Qed.

Definition function_set (a : E) (f : E1) :=
  Bounded.create (in_function_set a f).

Lemma function_set_iff :
 forall (a : E) (f : E1) (u : E),
 inc u (function_set a f) <-> in_function_set a f u.
ir.
unfold iff in |- *; xd; ir.
unfold function_set in H.
ap Bounded.lem1.
ap in_fs_bounded.

am.

unfold function_set in |- *.
ap Bounded.lem2.
ap in_fs_bounded.

am.
Qed.

Lemma function_set_sub_powerset_record :
 forall (a : E) (f : E1), sub (function_set a f) (powerset (record a f)).
ir.
unfold sub in |- *; ir.
pose (function_set_iff a f x).
unfold iff in (type of i); xd.
pose (H0 H).
ap powerset_inc.
ap in_fs_sub_record; au.
Qed.

Lemma function_set_pr :
 forall (a : E) (f : E1) (u : E),
 inc u (function_set a f) ->
 (in_function_set a f u 
 & Function.axioms u
 & Function.domain u = a
 & (forall y : E, inc y a -> inc (V y u) (f y))).
ir.
assert (in_function_set a f u).
pose (function_set_iff a f u).
unfold iff in (type of i); xd.

unfold in_function_set in H0; xd.
unfold in_function_set in |- *; xd.
Qed.

Lemma function_set_inc :
 forall (a : E) (f : E1) (u : E),
 Function.axioms u ->
 Function.domain u = a ->
 (forall y : E, inc y a -> inc (V y u) (f y)) -> inc u (function_set a f).
ir.
pose (function_set_iff a f u).
unfold iff in (type of i); xd.
ap H3.
unfold in_function_set in |- *; xd.
Qed.


Lemma in_function_set_inc :
 forall (a : E) (f : E1) (u : E),
 in_function_set a f u -> inc u (function_set a f).
ir.
pose (function_set_iff a f u).
unfold iff in (type of i); xd.
Qed.


End Function_Set.


(*****************************************************************************************)
(*****************************************************************************************)
(*****************************************************************************************)
(*****************************************************************************************)




Module String.

Inductive string : E := 
DOT : string |
a_:string->string |
b_:string->string |
c_:string->string |
d_:string->string |
e_:string->string |
f_:string->string |
g_:string->string |
h_:string->string |
i_:string->string |
j_:string->string |
k_:string->string |
l_:string->string |
m_:string->string |
n_:string->string |
o_:string->string |
p_:string->string |
q_:string->string |
r_:string->string |
s_:string->string |
t_:string->string |
u_:string->string |
v_:string->string |
w_:string->string |
x_:string->string |
y_:string->string |
z_:string->string .

End String. 




Module Notation.
Import Function.
Export String.


Definition mask (*: Prop -> E -> E *)  (P : Prop) (x : E) := 
Y P x emptyset.

Lemma mask_in : forall (P : Prop) (x : E), P -> mask P x = x. 
ir. uf mask. ap Y_if. am. tv. 
Qed. 

Lemma mask_out : forall (P : Prop) (x : E), ~ P -> 
mask P x = emptyset.
ir. uf mask. ap Y_if_not. am. tv.  
Qed. 

Definition is_notation f :=
Function.axioms f &
Function.domain f = string.

Definition stop := L string (fun s => emptyset).

Lemma is_notation_stop : is_notation stop.
Proof.
uhg; ee. uf stop. 
app create_axioms. 
uf stop. rww create_domain. 
Qed.

Lemma V_stop : forall x, V x stop = emptyset.
Proof.
ir. uf stop. 
apply by_cases with (inc x string); ir. 
rww create_V_rewrite. 
rww create_V_out. 
Qed.

Definition denote str obj old :=
L string (fun s => (Y (s = str) obj (V s old))).

Lemma is_notation_denote : forall str obj old,
is_notation old -> is_notation (denote str obj old).
Proof.
ir. uhg; ee. 
uf denote. aw.
uf denote. aw. 
Qed.

Lemma V_denote_new : forall str obj old x,
x = str -> inc x string -> V x (denote str obj old) = obj.
Proof.
ir. uf denote. 
aw. rww Y_if_rw. 
Qed.

Lemma V_denote_old : forall str obj old x,
~x=str -> inc x string -> V x (denote str obj old) = V x old.
Proof.
ir. uf denote. aw. rww Y_if_not_rw. 
Qed. 



Ltac show_string :=
match goal with
| |- inc ?X1 string  => try am; unfold X1; ap R_inc
| _ => fail
end.
 
Lemma R_string_inj : forall a b:string,
~a=b -> ~(R a = R b).
Proof.
ir. uhg; ir. ap H. ap R_inj. am. 
Qed.

Ltac show_different :=
match goal with
| |- ~(?X1 = ?X2) => 
(try (unfold X1); try (unfold X2);
ap R_string_inj; discriminate)
| _ => fail
end. 

Ltac drw_solve := solve [tv | show_different | am | show_string].

Ltac drw_new := 
rewrite V_denote_new; [idtac | drw_solve | drw_solve].

Ltac drw_old :=
rewrite V_denote_old; [idtac | drw_solve | drw_solve].

Ltac drw_stop := rewrite V_stop.

Ltac drw := first [
drw_new ; drw | drw_old; drw | drw_stop ; drw | 
tv | am | idtac].

(*
Ltac drw :=
first [
rewrite V_denote_new; solve [drw_solve |drw] |
rewrite V_denote_old; solve [drw_solve |drw] |
rewrite V_stop].
*)



Definition Underlying := R (u_(d_(r_ DOT))).  


Definition U (x : E) := V Underlying x.


Definition unary (x:E) (f:E1) := L x f.

Lemma V_unary : forall x f a, inc a x -> 
V a (unary x f) = f a.
Proof.
ir. uf unary. rww Function.create_V_rewrite. 
Qed. 

Definition binary (x:E) (f:E2) :=
L x (fun a => (L x (fun b => f b a))).

Lemma V_V_binary : forall x f a b,
inc a x -> inc b x -> V a (V b (binary x f)) = f a b.
Proof.
ir. uf binary. 
rww Function.create_V_rewrite. 
rww Function.create_V_rewrite.
Qed. 

Hint Rewrite V_unary : aw.
Hint Rewrite V_V_binary : aw. 

End Notation. 
Export Notation. 

Module Arrow.
Import Function. 



Definition Source  := R (s_(r_(c_(DOT )))).
Definition Target  := R (t_(r_(g_(DOT )))).
Definition Arrow := R (a_(r_(r_ DOT ))).


Definition source (x : E) := V Source x. 
Definition target (x : E) := V Target x. 
Definition arrow (x : E) := V Arrow x.

Definition create (x y a: E) :=
denote Source x (
denote Target y (
denote Arrow a (
stop))). 


Lemma source_create : forall x y a, 
source (create x y a) = x. 
Proof.
ir.
uf source; uf create.  
drw.  
Qed. 

Lemma target_create : forall x y a, 
target (create x y a) = y. 
Proof.
ir. uf target; uf create; drw. 
Qed. 

Lemma arrow_create : forall x y a, 
arrow (create x y a) = a. 
Proof.
ir; uf arrow; uf create; drw.
Qed. 

Hint Rewrite source_create target_create arrow_create : aw. 

Definition like a := a = create (source a) (target a) (arrow a).

Lemma create_like : forall s t a :E,
like (create s t a) = True.
Proof.
ir. 
app iff_eq; ir. 
uf like. rw source_create. 
rw target_create. 
rw arrow_create. tv. 
Qed. 

Hint Rewrite create_like : aw.

Definition flip a :=
Y (like a) (create (target a) (source a) (arrow a)) a.

Lemma source_flip : forall a,
like a -> source (flip a) = target a.
Proof.
ir. uf flip.  rw Y_if_rw. rw source_create. tv. am. 
Qed.

Lemma target_flip : forall a,
like a -> target (flip a) = source a.
Proof.
ir. uf flip.  rw Y_if_rw. rw target_create. tv. am. 
Qed.

Lemma flip_not_like : forall a, ~(like a) -> flip a = a.
Proof.
ir. uf flip. rw Y_if_not_rw. tv. am. 
Qed. 

Lemma arrow_flip : forall a, arrow (flip a) = arrow a.
Proof.
ir. apply by_cases with (like a); ir. 
uf flip. 
rw Y_if_rw. rw arrow_create. tv. am. 
rw flip_not_like. tv. am. 
Qed.

Lemma flip_like : forall a, like a -> 
flip a = create (target a) (source a) (arrow a).
Proof.
ir. 
uf flip. rw Y_if_rw. tv. am. 
Qed. 

Lemma like_flip : forall a, like a = like (flip a).
Proof.
ir. ap iff_eq; ir. uf flip. 
rw Y_if_rw. aw.  am. 
apply by_cases with (like a); ir. am. 
rwi flip_not_like H. am. am. 
Qed. 

Lemma flip_flip : forall a, flip (flip a) = a.
Proof.
ir. apply by_cases with (like a); ir. 
rw flip_like. 
rw target_flip. rw source_flip. rw arrow_flip. 
uh H. sy; am. am. am. wr like_flip. am. 
rw flip_not_like. rw flip_not_like. tv. am. 
uhg; ir. ap H. rw like_flip. am. 
Qed. 

Definition ev u x := V x (arrow u). 


Lemma flip_eq : forall a b, flip a = flip b ->
a = b.
Proof.
ir. transitivity (flip (flip a)). rww flip_flip.
rw H. rww flip_flip. 
Qed. 

End Arrow.





Module Umorphism.
Import Function.
Import Notation.
Import Arrow. 
 



Section Construction.
Variables (x y : E) (f : E1).

Definition create := Arrow.create x y (L (U x) f).


Lemma source_create : source create = x. 
Proof.
uf create. rw Arrow.source_create. tv. 
Qed. 

Lemma target_create : target create = y. 
Proof.
uf create. rw Arrow.target_create. tv. 
Qed. 

Lemma ev_create : forall a : E, inc a (U x) -> 
ev create a = f a.
Proof. 
ir. uf ev. uf create. 
rw Arrow.arrow_create. 
rw create_V_rewrite. tv. am. 
Qed. 

Lemma arrow_create : arrow create = 
L (U (source create)) (ev create).
Proof.
uf create. 
rw Arrow.arrow_create. rw Arrow.source_create. 
uf ev. ap Function.create_extensionality. 
tv. ir. rw Arrow.arrow_create. 
rw Function.create_V_rewrite. 
tv. am. 
Qed. 


End Construction.




Lemma create_extens :
 forall (x x' y y' : E) (f g : E1),
 x = x' ->
 y = y' ->
 (forall a : E, inc a (U x) -> f a = g a) -> create x y f = create x' y' g.
ir.
wr H; wr H0. uf create. 
ap uneq. ap create_extensionality. tv. 
ir. au. 
Qed.



Definition realizes (x y : E) (f : E1) (a : E) :=
  source a = x
  & target a = y
  & (forall z : E, inc z (U x) -> ev a z = f z).

Definition property (x y : E) (f : E1) := Transformation.axioms (U x) (U y) f.

Definition like (a : E) := create (source a) (target a) (ev a) = a.


Lemma create_like : forall (x y : E) (f : E1), like (create x y f).
ir.
uf like. ap create_extens. ap source_create. 
ap target_create. ir. ap ev_create. rwi source_create H. am. 
Qed. 

Lemma like_arrow_like : forall u, like u -> Arrow.like u.
Proof.
ir. uh H. uhg. 
ufi create H. 
set (f:=Function.create (U (source u)) (ev u)) in H. 
assert (arrow u = f). wr H. rw Arrow.arrow_create. tv. rw H0.
sy; am. 
Qed. 


Lemma create_realizes :
 forall (x y : E) (f : E1), realizes x y f (create x y f).
ir.
pose source_create.
pose target_create.
pose ev_create.
unfold realizes in |- *; xe.
ir. au. 
Qed.


Lemma realizes_like_eq :
 forall (x y : E) (f : E1) (a : E),
 like a -> realizes x y f a -> create x y f = a.
ir. ufi like H. wr H. ap create_extens; ufi realizes H0; xd. ir; sy; ap H2; am. 
Qed. 


Definition axioms (a : E) := property (source a) (target a) (ev a).
Definition strong_axioms (a : E) := (axioms a & like a).

Lemma axioms_from_strong : forall a : E, strong_axioms a -> axioms a.
ir. unfold strong_axioms in H; xe.
Qed.

Lemma create_strong_axioms :
 forall (x y : E) (f : E1), property x y f -> strong_axioms (create x y f).
ir.
unfold strong_axioms in |- *.
ee.
unfold axioms in |- *.
rw source_create.
rw target_create.
uf property.
uf Transformation.axioms.
ir.
rw ev_create. 
ufi property H.
ufi Transformation.axioms H.
ap H.
am.

am.

ap create_like.
Qed.

Lemma create_axioms :
 forall (x y : E) (f : E1), property x y f -> axioms (create x y f).
ir. ap axioms_from_strong. ap create_strong_axioms; au.
Qed.

Definition identity (x : E) := create x x (fun y : E => y).

Definition compose (a b : E) :=
  create (source b) (target a) (fun y : E => ev a (ev b y)).

Lemma identity_strong_axioms : forall x : E, strong_axioms (identity x).
ir.
uf identity.
ap create_strong_axioms.
uf property.
ap Transformation.identity_axioms.
Qed.

Lemma identity_axioms : forall x : E, axioms (identity x).
ir. cp (identity_strong_axioms x). 
ufi strong_axioms H; xe.
Qed.


Lemma left_identity :
 forall a : E, strong_axioms a -> compose (identity (target a)) a = a.
ir.
unfold compose in |- *.
ap realizes_like_eq.
unfold strong_axioms in H; xe.

unfold realizes in |- *.
xe.
unfold identity in |- *; rewrite target_create.
tv.

ir.
unfold identity in |- *.
rewrite ev_create.
tv.

unfold strong_axioms in H.
xd.
Qed.


Lemma right_identity :
 forall a : E, strong_axioms a -> compose a (identity (source a)) = a.
ir.
unfold compose in |- *.
ap realizes_like_eq.
unfold strong_axioms in H; xe.

unfold realizes in |- *.
xe.
unfold identity in |- *; rewrite source_create.
tv.

ir.
unfold identity in |- *; rewrite ev_create.
tv.

unfold identity in H0; rewrite source_create in H0.
am.
Qed.

Lemma source_identity : forall x : E, source (identity x) = x.
ir. unfold identity in |- *; rewrite source_create. tv.
Qed.

Lemma target_identity : forall x : E, target (identity x) = x.
ir. unfold identity in |- *; rewrite target_create. tv.
Qed.

Lemma ev_identity : forall x y : E, inc y (U x) -> ev (identity x) y = y.
ir. unfold identity in |- *; rewrite ev_create; au.
Qed.

Lemma source_compose : forall a b : E, source (compose a b) = source b.
ir. unfold compose in |- *; rewrite source_create; tv.
Qed.

Lemma target_compose : forall a b : E, target (compose a b) = target a.
ir. unfold compose in |- *; rewrite target_create; tv.
Qed.

Lemma ev_compose :
 forall a b y : E,
 inc y (U (source b)) -> ev (compose a b) y = ev a (ev b y).
ir. unfold compose in |- *; rewrite ev_create; au.
Qed.

Hint Rewrite source_compose target_compose
source_identity target_identity ev_identity ev_compose : aw.

Definition composable (a b : E) :=
(axioms a & axioms b & source a = target b).



Lemma compose_strong_axioms :
 forall a b : E, composable a b -> strong_axioms (compose a b).
ir.
unfold strong_axioms in |- *.
xe.
unfold axioms in |- *.
rewrite source_compose.
rewrite target_compose.
unfold property in |- *.
unfold Transformation.axioms in |- *.
ir.
rewrite ev_compose.
unfold composable in H.
xe.
unfold axioms in H.
unfold property in H.
unfold Transformation.axioms in H.
ap H.
unfold axioms in H1.
unfold property in H1.
unfold Transformation.axioms in H1.
rewrite H2.
ap H1.
am.

am.

unfold compose in |- *.
ap create_like.
Qed.

Lemma compose_axioms : forall a b : E, composable a b -> axioms (compose a b).
ir. set (K := compose_strong_axioms H). unfold strong_axioms in (type of K); xe.
Qed. 

Lemma extens :
 forall a b : E,
 strong_axioms a ->
 strong_axioms b ->
 source a = source b ->
 target a = target b ->
 (forall x : E,
  inc x (U (source a)) -> inc x (U (source b)) -> ev a x = ev b x) ->
 a = b.
ir.
unfold strong_axioms in H, H0.
xe.
unfold like in H5, H4.
rewrite <- H5.
ap realizes_like_eq; au.
unfold realizes in |- *.
xe.
ir.
sy; ap H3.
am.

rewrite <- H1.
am.
Qed.

Lemma associativity :
 forall a b c : E,
 composable a b ->
 composable b c -> compose (compose a b) c = compose a (compose b c).
ir.
ap extens.
ap compose_strong_axioms.
unfold composable in |- *.
xe.
ap compose_axioms; au.

unfold composable in H0; xe.

rewrite source_compose.
unfold composable in H0; xe.

ap compose_strong_axioms.
unfold composable in |- *; xe.
unfold composable in H; xe.

ap compose_axioms.
am.

rewrite target_compose.
unfold composable in H; xe.

repeat rewrite source_compose.
tv.

repeat rewrite target_compose; tv.

ir.
repeat rewrite ev_compose.
tv.

repeat rewrite source_compose in H1.
am.

rewrite source_compose in H2.
am.

repeat rewrite source_compose in H1.
unfold composable in H0.
xe.
rewrite H4.
ap H3.
am.

repeat rewrite source_compose in H1.
am.
Qed.


Definition inclusion (a b : E) := create a b (fun y : E => y).


Lemma inclusion_strong_axioms :
 forall a b : E, sub (U a) (U b) -> strong_axioms (inclusion a b).
ir.
unfold inclusion in |- *.
ap create_strong_axioms.
unfold property in |- *.
unfold Transformation.axioms in |- *.
ir.
ap H; au.
Qed.

Lemma inclusion_axioms :
 forall a b : E, sub (U a) (U b) -> axioms (inclusion a b).
ir. ap axioms_from_strong. ap inclusion_strong_axioms; au.
Qed.


Definition injective (u : E) :=
  axioms u
  & Transformation.injective (U (source u)) (U (target u)) (ev u).

Lemma injective_rewrite :
 forall u : E,
 axioms u ->
 injective u =
 (forall x y : E,
  inc x (U (source u)) ->
  inc y (U (source u)) -> ev u x = ev u y -> x = y).
ir.
ap iff_eq; ir.
unfold injective in H0.
xe.
unfold Transformation.injective in H4.
xe. au.

unfold injective in |- *; xe.
unfold Transformation.injective in |- *; xe.
Qed.

Lemma injective_compose_with :
 forall u v w : E,
 strong_axioms u ->
 strong_axioms v ->
 injective w ->
 composable w u -> composable w v -> compose w u = compose w v -> u = v.
ir.
ap extens; au.
transitivity (source (compose w u)).
rewrite source_compose; au.

rewrite H4.
rewrite source_compose; au.

unfold composable in H2, H3.
xe.
transitivity (source w); au.

ir.
unfold injective in H1.
xe.
unfold Transformation.injective in H7.
xe.
ap H8.
unfold strong_axioms in H.
xe.
unfold axioms in H.
unfold property in H.
unfold composable in H2.
xe.
rewrite H11.
ap H.
am.

unfold composable in H3; xe.
rewrite H10.
unfold strong_axioms in v; xe. au.

transitivity (ev (compose w u) x).
rewrite ev_compose; au.

rewrite H4.
rewrite ev_compose; au.
Qed. 

Definition surjective (u : E) :=
  axioms u
  & Transformation.surjective (U (source u)) (U (target u)) (ev u).

Lemma surjective_rewrite :
 forall u : E,
 axioms u ->
 surjective u =
 (forall x : E,
  inc x (U (target u)) ->
  ex (fun y : E => (inc y (U (source u)) & ev u y = x))).
ir.
ap iff_eq; ir.
unfold surjective in H0; xe.
unfold Transformation.surjective in H2; xe. au.

unfold surjective in |- *; xe.
unfold Transformation.surjective in |- *; xe.
Qed. 

Definition inverse (u : E) :=
  create (target u) (source u)
    (Transformation.inverse (U (source u)) (ev u)).

Lemma surjective_inverse_axioms :
 forall u : E, surjective u -> strong_axioms (inverse u).
ir.
unfold strong_axioms in |- *; xe.
unfold inverse in |- *.
ap create_axioms.
unfold property in |- *.
ap Transformation.surjective_inverse_axioms.
unfold surjective in H; xe.

unfold inverse in |- *.
ap create_like.
Qed. 

Lemma surjective_composable_left :
 forall u : E, surjective u -> composable (inverse u) u.
ir.
unfold composable in |- *.
xe.
ap axioms_from_strong.
ap surjective_inverse_axioms; au.

unfold surjective in H; xe.

unfold inverse in |- *.
rewrite source_create; tv.
Qed.

Lemma surjective_composable_right :
 forall u : E, surjective u -> composable u (inverse u).
ir.
unfold composable in |- *; xe.
unfold surjective in H; xe.

ap axioms_from_strong.
ap surjective_inverse_axioms; au.

unfold inverse in |- *; rewrite target_create; tv.
Qed. 

Lemma surjective_inverse_right :
 forall u : E, surjective u -> compose u (inverse u) = identity (target u).
ir.
assert (axioms u).
unfold surjective in H; xe.

ap extens.
ap compose_strong_axioms.
ap surjective_composable_right.
am.

ap identity_strong_axioms.

rewrite source_compose.
rewrite source_identity.
unfold inverse in |- *; rewrite source_create.
tv.

rewrite target_compose.
rewrite target_identity; tv.

ir.
rewrite ev_compose.
rewrite ev_identity.
unfold inverse in |- *.
rewrite ev_create.
unfold surjective in H.
xe.
rewrite source_identity in H2.
pose (Transformation.surjective_inverse_right H3 H2).
ap e.

rewrite source_identity in H2; am.

rewrite source_identity in H2; am.

rewrite source_compose in H1.  
am. Qed.

Definition bijective (u : E) := (injective u & surjective u).

Lemma bijective_transformation_bijective :
 forall u : E,
 bijective u ->
 Transformation.bijective (U (source u)) (U (target u)) (ev u).
ir.
unfold bijective in H; xe.
unfold injective in H.
unfold surjective in H0.
xe.
unfold axioms in H.
unfold property in H.
unfold Transformation.bijective in |- *; xe.
Qed. 

Lemma transformation_bijective_bijective :
 forall u : E,
 axioms u ->
 Transformation.bijective (U (source u)) (U (target u)) (ev u) ->
 bijective u.
ir.
unfold Transformation.bijective in H0.
unfold bijective in |- *.
xe.
unfold injective in |- *; xe.

unfold surjective in |- *; xe.
Qed. 

Definition are_inverse (u v : E) :=
  composable u v
  & composable v u
  & compose u v = identity (source v)
  & compose v u = identity (source u).

Lemma inverse_symm : forall u v : E, are_inverse u v -> are_inverse v u.
ir.
unfold are_inverse in |- *.
unfold are_inverse in H.
xe.
Qed. 

Lemma inverse_unique :
 forall u v w : E,
 strong_axioms v ->
 strong_axioms w -> are_inverse u v -> are_inverse u w -> v = w.
ir.
transitivity (compose v (identity (source v))).
sy.
ap right_identity.
am.

unfold are_inverse in H1, H2; ee.
assert (source v = target u).
unfold composable in H6; xe.

assert (source v = source w).
rewrite H9.
unfold composable in H3; xe.

rewrite H10.
rewrite <- H4.
rewrite <- associativity.
rewrite H8.
assert (source u = target w).
unfold composable in H2; xe.

rewrite H11.
ap left_identity.
am.

am.

am.
Qed. 

Definition has_inverse (u : E) := ex (fun v : E => are_inverse u v).

Lemma are_inverse_transfo_inverse :
 forall u v : E,
 are_inverse u v ->
 Transformation.are_inverse (U (source u)) (U (target u)) (
   ev u) (ev v).
ir.
unfold Transformation.are_inverse in |- *.
unfold are_inverse in H.
xe.
unfold composable in H; xe.

unfold composable in H, H0; xe.
rewrite <- H4.
rewrite H6.
am.

ir.
transitivity (ev (compose v u) x).
sy; ap ev_compose.
am.

rewrite H2.
ap ev_identity.
am.

ir.
assert (inc y (U (source v))).
unfold composable in H0; xe.
rewrite H5; am.

transitivity (ev (compose u v) y).
rewrite ev_compose.
tv.

am.

rewrite H1.
rewrite ev_identity.
tv.

am.
Qed. 

Lemma inverse_bijective : forall u v : E, are_inverse u v -> bijective u.
ir.
ap transformation_bijective_bijective.
unfold are_inverse in H; xe.
unfold composable in H; xe.

apply Transformation.inverse_bijective with (ev v).
ap are_inverse_transfo_inverse.
am.
Qed.

Lemma bijective_inverse :
 forall u : E, bijective u -> are_inverse u (inverse u).
ir.
unfold bijective in H; xe.
pose (surjective_composable_left H0).
pose (surjective_composable_right H0).
pose (surjective_inverse_right H0).
unfold are_inverse in |- *; ee. am. am. 
unfold composable in (type of c); ee. 
rewrite H3.
ap e.

apply injective_compose_with with u.
ap compose_strong_axioms; au.

ap identity_strong_axioms.

am.

unfold composable in |- *.
ee.
unfold injective in H; xe.

ap compose_axioms; au.

rewrite target_compose.
unfold composable in (type of c0); xe.

unfold composable in |- *; ee.
unfold injective in H; xe.

ap identity_axioms.

rewrite target_identity; tv.

rewrite <- associativity.
rewrite e.
ap extens.
ap compose_strong_axioms.
unfold composable in |- *; ee.
ap identity_axioms.

unfold injective in H; xe.

rewrite source_identity.
tv.

ap compose_strong_axioms.
unfold composable in |- *; ee.
unfold injective in H; xe.

ap identity_axioms.

rewrite target_identity; tv.

rewrite source_compose.
rewrite source_compose.
rewrite source_identity; tv.

repeat rewrite target_compose.
rewrite target_identity.
tv.

ir.
repeat rewrite ev_compose.
repeat rewrite ev_identity.
tv.

rewrite source_compose in H2.
rewrite source_identity in H2; am.

unfold injective in H; ee.
unfold axioms in H.
unfold property in H; xe.
ap H.
rewrite source_compose in H2.
rewrite source_identity in H2.
am.

rewrite source_compose in H2; am.

rewrite source_compose in H2.
rewrite source_identity in H2.
am.

am.

am.
Qed.


Lemma bijective_has_inverse : forall u : E, bijective u -> has_inverse u.
ir. unfold has_inverse in |- *. apply ex_intro with (inverse u).
ap bijective_inverse; au.
Qed. 


Lemma bijective_eq_has_inverse : forall u : E, bijective u = has_inverse u.
ir.
ap iff_eq; ir.
unfold has_inverse in |- *.
apply ex_intro with (inverse u).
ap bijective_inverse; au.

unfold has_inverse in H.
nin H.
apply inverse_bijective with x; au.
Qed.

Lemma bijective_eq_inverse :
 forall u : E, bijective u = are_inverse u (inverse u).
ir.
ap iff_eq; ir.
ap bijective_inverse.
am.

apply inverse_bijective with (inverse u); am.
Qed. 

Lemma has_inverse_eq_inverse :
 forall u : E, has_inverse u = are_inverse u (inverse u).
ir.
rewrite <- bijective_eq_inverse.
rewrite bijective_eq_has_inverse.
tv.
Qed. 




Definition Uempty := stop.


Definition Uempty_initial (a : E) := inclusion Uempty a.

Lemma underlying_Uempty : U Uempty = emptyset.
uf Uempty. uf U. drw. 
Qed. 

Lemma Uempty_initial_strong_axioms :
 forall a : E, strong_axioms (Uempty_initial a).
ir. uf Uempty_initial. ap inclusion_strong_axioms. rw underlying_Uempty. uf sub; ir.
nin H. elim x0. Qed. 

Lemma use_axioms :
 forall u x y a : E,
 axioms u ->
 source u = x -> target u = y -> inc a (U x) -> inc (ev u a) (U y).
ir. cx. wr H1. ap H. rw H0. am.
Qed. 

Ltac clst :=
  match goal with
  | id1:?X1 |- _ => first
  [ rewrite source_create in id1; clst
  | rewrite target_create in id1; clst
  | rewrite source_identity in id1; clst
  | rewrite target_identity in id1; clst
  | rewrite source_compose in id1; clst
  | rewrite target_compose in id1; clst ]
  |  |- _ => first
  [ rewrite source_create; clst
  | rewrite target_create; clst
  | rewrite source_identity; clst
  | rewrite target_identity; clst
  | rewrite source_compose; clst
  | rewrite target_compose; clst ]
  | _ => idtac
  end.




End Umorphism.






(*****************************************************************************************)
(*****************************************************************************************)
(*****************************************************************************************)
(*****************************************************************************************)



Module Universe.
Export Function.
Export Notation.
Export Arrow.
Export Umorphism. 


Definition axioms u :=
(forall x y, inc x u -> inc y x -> inc y u) &
(forall x (f:x->E), inc x u -> (sub (IM f) u) ->
inc (IM f) u) &
(forall x, inc x u -> inc (union x) u) &
(forall x, inc x u -> inc (powerset x) u) &
inc nat u &
inc string u.

Lemma inc_trans_u : forall x u, axioms u -> 
(exists y, (inc x y & inc y u)) -> inc x u.
Proof.
ir. nin H0. uh H; ee. 
app (H x0 x). 
Qed. 

Lemma inc_powerset_u : forall x u, axioms u ->  inc x u ->
inc (powerset x) u.
Proof.
ir. uh H; ee; au. 
Qed. 

Lemma inc_nat_u : forall u, axioms u -> inc nat u.
Proof.
ir. uh H; ee; au.
Qed.

Lemma inc_R_nat_u : forall (n:nat) u, axioms u -> inc (R n) u.
Proof.
ir. ap inc_trans_u. am. sh nat. 
ee. uf inc. sh n. tv. app inc_nat_u. 
Qed. 

Lemma inc_prop_u : forall u, axioms u -> inc Prop u.
Proof.
ir. wr R_two_prop. ap inc_R_nat_u. am. 
Qed.

Lemma inc_R_a_prop_u : forall u (p:Prop), axioms u -> 
inc (R p) u.
Proof.
ir. app inc_trans_u. sh Prop. ee. 
uf inc. sh p; tv. app inc_prop_u. 
Qed. 

Lemma inc_a_prop_u : forall u (p:Prop), axioms u -> inc p u.
Proof.
ir. 
assert (R p = p). rww prop_realization. wr H0. 
app inc_R_a_prop_u. 
Qed.

Lemma inc_proof_u : forall u (p:Prop) (t:p), axioms u ->
inc (R t) u. 
Proof.
ir. app inc_trans_u. 
sh p. ee. ap R_inc. app inc_a_prop_u. 
Qed. 


Lemma inc_string_u : forall u, axioms u -> inc string u.
Proof.
ir. uh H; ee; au.
Qed. 

Lemma inc_subset_u : forall x u, axioms u ->
(exists y, (inc y u & sub x y)) -> inc x u.
Proof. 
ir. nin H0. ee. ap inc_trans_u. am. 
sh (powerset x0). ee. ap powerset_inc. am. 
app inc_powerset_u. 
Qed. 

Lemma inc_emptyset_u : forall u, axioms u ->
inc emptyset u.
Proof.
ir. app inc_subset_u. sh nat. 
ee. app inc_nat_u. uhg; ir. 
cp (B H0). nin X0. 
Qed. 

Lemma inc_IM_u : forall x (f:x->E) u,
axioms u -> inc x u -> sub (IM f) u ->
inc (IM f) u.
Proof.
ir. uh H; ee. ap H2. am. am. 
Qed. 


Definition doubleton_step :forall (x y:E) (n:nat), E.
ir. nin n. exact x. exact y. 
Defined. 

Lemma IM_doubleton_step: forall x y,
IM (doubleton_step x y) = (doubleton x y).
Proof.
ir. app extensionality; uhg; ir. 
cp (IM_exists H). nin H0. 
nin x1. assert (x = x0). am. wr H1. 
ap doubleton_first. 
assert (y = x0). am. wr H1. 
ap doubleton_second. 
ap IM_inc. 
cp (doubleton_or H). nin H0. sh 0. sy; am. 
sh 1. sy; am. 
Qed. 

Lemma inc_doubleton_u : forall x y u, 
axioms u -> inc x u -> inc y u -> inc (doubleton x y) u.
Proof.
ir. 
wr IM_doubleton_step. 
ap inc_IM_u. am. app inc_nat_u. 
rw IM_doubleton_step. uhg; ir. 
cp (doubleton_or H2). nin H3. rww H3.
rww H3. 
Qed.

Lemma inc_singleton_u : forall x u,
axioms u -> inc x u -> inc (singleton x) u.
Proof.
ir. wr doubleton_singleton. app inc_doubleton_u. 
Qed. 

Lemma inc_pair_u : forall x y u, 
axioms u -> inc x u -> inc y u -> inc (pair x y) u.
Proof.
ir. uf pair. 
app inc_doubleton_u. app inc_singleton_u. 
app inc_doubleton_u. app inc_emptyset_u. 
app inc_singleton_u. 
Qed.

Lemma sub_u : forall x u, axioms u -> inc x u ->
sub x u.
Proof.
ir. uhg; ir. app inc_trans_u. sh x; ee; am. 
Qed. 

Lemma inc_function_create_u : forall x f u,
axioms u -> inc x u -> 
(forall y, inc y x -> inc (f y) u) ->
inc (L x f) u.
Proof.
ir. uf Function.create. 
uf Image.create. ap inc_IM_u. am. am. 
uhg; ir. cp (IM_exists H2). nin H3. wr H3.
ap inc_pair_u. am. app inc_trans_u. 
sh x; ee; try am. ap R_inc. 
ap H1. ap R_inc. 
Qed. 

Lemma inc_function_tcreate_u : forall x (f:x->E) u,
axioms u -> inc x u -> 
(forall y, inc (f y) u) ->
inc (tcreate f) u. 
Proof.
ir. uf tcreate. 
ap inc_function_create_u. am. am. 
ir. 
assert ( (Yy (fun hyp : inc y x => f (B hyp)) emptyset) 
= f (B H2)). 
ap (Yy_if (hyp := H2)). tv. 
rw H3. ap H1. 
Qed. 





Lemma inc_pr1_of_pair_u : forall u x,
axioms u -> (exists y, inc (pair x y) u) -> inc x u.
Proof.
ir. nin H0. 
app inc_trans_u. sh (singleton x). 
ee. ap singleton_inc. 
app inc_trans_u. sh (pair x x0). ee. uf pair.
ap doubleton_first. am. 
Qed.

Lemma inc_pr2_of_pair_u : forall u y,
axioms u -> (exists x, inc (pair x y) u) -> inc y u.
Proof.
ir. nin H0. app inc_trans_u. sh (singleton y).
ee. ap singleton_inc. 
app inc_trans_u. 
sh (doubleton emptyset (singleton y)). ee. ap doubleton_second. 
app inc_trans_u. sh (pair x y). 
ee. uf pair; ap doubleton_second. am. 
Qed. 

Lemma inc_V_u : forall f x u,
axioms u -> inc f u -> inc x u -> inc (V x f) u.
Proof.
ir. cp (V_or x f). nin H2. 
app inc_pr2_of_pair_u. sh x. 
app inc_trans_u. sh f; ee; try am. 
ee. rw H3. app inc_emptyset_u. 
Qed. 

Lemma inc_denote_u : forall s x a u,
axioms u -> inc a u -> inc s string -> inc x u ->
inc (denote s x a) u.
Proof.
ir. uf denote. 
app inc_function_create_u. app inc_string_u. ir.
apply by_cases with (y=s);
ir. rww Y_if_rw. 
rww Y_if_not_rw. app inc_V_u. 
app inc_trans_u. sh string; ee; try am. 
app inc_string_u. 
Qed. 




Lemma inc_binary_u : forall x f u,
axioms u -> inc x u -> 
(forall y z, inc y x -> inc z x -> inc (f y z) u) ->
inc (binary x f) u.
Proof.
ir. uf binary. 
app inc_function_create_u. 
ir. app inc_function_create_u. ir. 
au. 
Qed. 

Lemma inc_stop_u : forall u,
axioms u -> inc stop u. 
Proof.
ir. uf stop. 
app inc_function_create_u. app inc_string_u. ir. 
app inc_emptyset_u. 
Qed. 

Ltac incdu := 
first [
app inc_denote_u; try drw_solve| app inc_stop_u].


Lemma inc_arrow_create_u : forall s t a u,
axioms u -> inc s u -> inc t u -> inc a u ->
inc (Arrow.create s t a) u. 
Proof.
ir. uf Arrow.create. 
incdu. incdu. incdu. incdu. 
Qed. 

Lemma inc_Uempty_u : forall u, axioms u ->
inc Umorphism.Uempty u.
Proof.
ir. uf Umorphism.Uempty. incdu. 
Qed. 

End Universe. 


(*****************************************************************************************)
(*****************************************************************************************)
(*****************************************************************************************)
(*****************************************************************************************)