Require Export "set_theory".

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.


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.


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.


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 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.