(** * Theory of Sets  EII-3 Correspondences
  Copyright INRIA (2009-2010) Apics Team (Jose Grimm).
*)

(* $Id: set2.v,v 1.109 2010/08/02 07:30:56 grimm Exp $ *)
Require Export set1.
Set Implicit  Arguments.
(** ** EII-3-1  Graphs et correspondences *) 

Module Correspondence.

(** ** Additional lemmas *) 


(** Properties of the empty set *)

Lemma sub_emptyset : forall x,
  sub x emptyset = (x = emptyset).
Proof. ir. ap iff_eq. ir. empty_tac. nin (H _ H0). elim x0.
  ir. ue.
Qed.


(** We say [related r x y] if the pair (x,y) is in the graph  *) 
Definition related r x y := inc (J x y) r.

(** Proposition 1: existence and uniqueness of range and domain *)
Theorem range_domain_exists: forall r, 
  is_graph r -> 
  (exists_unique (fun a=> (forall x, inc x a = (exists y, inc (J x y) r))) &
    exists_unique (fun b=> (forall y, inc y b  = (exists x, inc (J x y) r)))).
Proof. ir. ee. red. ee. exists (domain r). ir. aw. 
  ir. set_extens. rw H1;wrr H0. rw H0; wrr H1. 
  red. ee. exists (range r). ir. aw. 
  ir. set_extens. rw H1; wrr H0. rw H0; wrr H1.
Qed. 

Lemma sub_graph_prod: forall r, is_graph r -> 
  sub r (product (domain r)(range r)).
Proof. ir. red. ir. set (H _ H0). aw. ee. am. ex_tac. ex_tac.
Qed. 

Lemma empty_graph1: forall r, is_graph r -> 
  (domain r = emptyset) = (r = emptyset).
Proof. ir. ap iff_eq; ir; empty_tac. 
  empty_tac1 (P y). aw. ex_tac. app H.
  awi H1. nin H1. rwi H0 H1. elim (emptyset_pr H1). am.
Qed.

Lemma empty_graph2: forall r, is_graph r -> 
  (range r = emptyset) =  (r = emptyset).
Proof. ir. app iff_eq; ir; empty_tac.
  empty_tac1 (Q y). aw. ex_tac.  app H. 
  awi H1. nin H1. rwi H0 H1. elim (emptyset_pr H1).  am.
Qed. 

(** A product is a special graph *)

Lemma product_is_graph: forall x y,
  is_graph (product x y).
Proof. red. ir. awi H. eee. Qed. 

Hint Resolve product_is_graph: fprops.

Lemma product_related: forall x y a b,
  related (product x y) a b = (inc a x & inc b y).
Proof. ir. uf related. aw. ap iff_eq. int. ir. eee. 
Qed.

Lemma product_domain: forall x y,
  nonempty y -> domain (product x y) = x.
Proof. ir. set (@product_is_graph x y).
  set_extens. awii H0. nin H0. awi H0. int. 
  aw. nin H. exists y0. fprops.  
Qed.

Lemma product_range: forall x y,
   nonempty x -> range (product x y) = y.
Proof. ir. set (@product_is_graph x y).
  set_extens. awii H0. nin H0. awi H0. int. 
  aw. nin H. exists y0. fprops.
Qed.

Lemma constant_function_p1: forall x y,
  fgraph (product x (singleton y)).
Proof. ir. red. ee. fprops. intros a b. aw. ir. ee. inter2tac. ue.
Qed.

Lemma emptyset_graph: is_graph (emptyset).
Proof. red. ir. nin H. elim x. Qed. 

Hint Resolve emptyset_graph : fprops.

Lemma emptyset_range: range emptyset = emptyset.
Proof. rww empty_graph2. fprops. Qed.

Lemma emptyset_domain: domain emptyset = emptyset.
Proof. rww empty_graph1. fprops. Qed.

Lemma emptyset_fgraph: fgraph emptyset.
Proof. red. ee. fprops. ir. elim (emptyset_pr H).
Qed.

Hint Rewrite emptyset_range emptyset_domain : sw.

(** Diagonal of a set: this is a functional graph [x -> x] *)

Definition diagonal x := Zo (product x x)(fun y=> P y = Q y).

Lemma diagonal_is_identity: forall x, diagonal x = identity_g x.
Proof. ir. uf identity_g. uf L.  uf diagonal. set_extens. Ztac. awi H0. 
  aw. ee.  wr (pair_recov H0). rw H1. ex_tac. awi H. nin H. ee. wr H0. Ztac.
  fprops. aw.
Qed.

Lemma inc_diagonal_rw: forall x u,
  inc u (identity_g x) = (is_pair u & inc (P u) x & P u = Q u).
Proof. ir. wr diagonal_is_identity. uf diagonal.
  ap iff_eq; ir; [ idtac | ee] ; Ztac. awi H0. int. aw. wr H1. au. 
Qed.

Lemma inc_pair_diagonal: forall x u v,
  inc (J u v) (identity_g x)  = (inc u x & u = v).
Proof. ir. rw inc_diagonal_rw. aw. ap iff_eq; int.
Qed.

Hint Rewrite inc_pair_diagonal : aw.

Lemma identity_graph:  forall x, is_graph (identity_g x).
Proof. ir. nin (identity_fgraph x). am.
Qed. 

Hint Resolve identity_graph : fprops.

Lemma identity_range: forall x, range (identity_g x) = x.
Proof. ir.  uf identity_g. set_extens. bwi H. nin H. nin H. ue.  bw. ex_tac.
Qed. 

(** For Bourbaki, a correspondence between A and B is a triple (G,A,B), 
   graph, source and target, with constraints.
   We use a record, convertible to a triple *)


(** A triple (G,A,B) or a record F is a correspondence only if 
   G is a subset of the product of A and B. This can be restated as:
   G is a graph, domain and range are subsets of source and target *)
Definition is_triple  f := is_pair f & is_pair (Q f).
Definition source x := P (Q x). 
Definition target x := Q (Q x). 
Definition graph x := P x. 
Definition corr_propb s t g:=  sub g (product s t).  
Definition corresp s t g  := J g (J s t).

Definition is_correspondence f  :=
  is_triple f &  corr_propb (source f) (target f) (graph f).

Lemma corr_propa: forall x y z,
   corr_propb x y z = inc z (powerset (product x y)).
Proof. ir. aw.
Qed. 

Lemma corr_propc: forall s t g,
  corr_propb s t g = (is_graph g & sub (domain g) s & sub (range g) t).
Proof. ir. sy. uf corr_propb. ap iff_eq; ir. ee.
  apw sub_trans (product (domain g) (range g)). ap (sub_graph_prod H).
  app product_monotone.
  assert (is_graph g). red. ir. cp (H _ H0). awi H1; eee. 
  ee. am. red. ir. awii H1. nin H1. set (H _ H1). awi i. int. 
  red. ir. awii H1. nin H1. set (H _ H1). awi i. int.
Qed.

Lemma is_triple_corr: forall s t g, is_triple (corresp s t g).
Proof. red. ir.  uf corresp. ee.  fprops. aw. fprops.
Qed.

Lemma corresp_recov: forall f, is_triple f ->
  corresp (source f) (target f) (graph f) = f.
Proof. ir. nin H. uf corresp. uf source; uf target; uf graph. 
  app pair_extensionality. fprops. aw. aw.
Qed.

Lemma corresp_source: forall s t g,   source (corresp s t g) = s.
Proof. ir. uf corresp; uf source; aw. Qed.

Lemma corresp_target: forall s t g,   target (corresp s t g) = t.
Proof. ir. uf corresp; uf target; aw. Qed.

Lemma corresp_graph: forall s t g,   graph (corresp s t g) = g.
Proof. ir. uf corresp; uf graph; aw. Qed.

Hint Rewrite corresp_source  corresp_target corresp_graph : aw.


Lemma corresp_create: forall s t g,
  corr_propb s t g -> is_correspondence (corresp s t g).
Proof. ir. red. split. app is_triple_corr. aw.
Qed.

Lemma corresp_propb: forall f,
  is_correspondence f -> corr_propb (source f) (target f)(graph f). 
Proof. ir. red in H. int.
Qed.

(** Some properties of a correspondence *)
Lemma corresp_is_graph: forall g,
  is_correspondence g -> is_graph (graph g).
Proof. ir. red in H. rwi corr_propc H. eee.
Qed.

Lemma corresp_sub_range: forall g,
  is_correspondence g -> sub (range (graph g)) (target g).
Proof. ir. red in H.  rwi corr_propc H. eee.
Qed.

Lemma corresp_sub_domain: forall g,
  is_correspondence g -> sub (domain (graph g)) (source g).
Proof. ir. red in H. rwi corr_propc H. eee.
Qed.

Hint Resolve corresp_sub_range corresp_sub_domain corresp_is_graph: fprops.

(** The set of correspondences  [E->F] is the product of P and  singleton E and     singleton F, where P is [powerset (product E F)] is the set of graphs of
    correspondences *)

Definition set_of_correspondences (x y:Set) :=
  product (powerset (product x y))
          (product (singleton x) (singleton y)).

Lemma set_of_correspondences_rw: forall x y z,
  inc z (set_of_correspondences x y) =
  (is_correspondence z & source z = x & target z = y).
Proof. ir. uf set_of_correspondences. uf is_correspondence. 
  uf source; uf target; uf graph. uf is_triple. rw corr_propa. aw.
  app iff_eq; ir; eee. rw H2; rww H3. rwi H0 H2; rwi H1 H2. am.
Qed.

Lemma set_of_correspondences_propa: forall f,
  is_correspondence f ->
  inc f (set_of_correspondences (source f) (target f)).
Proof. ir. rw set_of_correspondences_rw. au.
Qed.


(** We create a correspondence from a map [f:a->b] *)

Definition gacreate (a b:Set) (f:a->b) := IM (fun y:a => J (Ro y) (Ro (f y))).
Definition acreate (a b:Set) (f:a->b)  := corresp a b (gacreate f).

Lemma acreate_corresp: forall  (a b:Set) (f:a->b),
  is_correspondence (acreate f).
Proof. ir. uf acreate. app corresp_create. red. uf gacreate. red. ir.
  nin (IM_exists H). wr H0. aw. ee. fprops. app R_inc. app R_inc.
Qed.

(** Image by the graph [r] of a set [u] *)

Definition image_by_graph r u:=
  Zo (range r) (fun y=>exists x, inc x u & inc (J x y) r). 

Definition image_by_fun r u :=
  image_by_graph (graph r) u.

Definition image_of_fun f :=
  image_by_graph (graph f) (source f).

Lemma image_by_graph_rw: forall u r y, 
  inc y (image_by_graph r u) = exists x, (inc x u & inc (J x y) r).
Proof. ir. uf image_by_graph. ap iff_eq; ir;Ztac. am.
  uf range. aw. nin H. exists (J x y). ee. am. aw.
Qed.

Hint Rewrite image_by_graph_rw : aw.

Lemma sub_image_by_graph: forall u r,
  sub (image_by_graph r u) (range r).
Proof. ir. uf image_by_graph. ap Z_sub. Qed.

Lemma image_by_graph_domain: forall r, is_graph r ->
  image_by_graph r (domain r) =  range r.
Proof. ir.  app extensionality. app sub_image_by_graph. 
  red. ir. aw. awii H0. nin H0. ex_tac. ex_tac. 
Qed.

Lemma image_by_emptyset: forall r, 
  image_by_graph r emptyset =  emptyset.
Proof. ir. uf image_by_graph. empty_tac. Ztac. nin H1. ee. 
  ap (emptyset_pr H1).
Qed.

Lemma image_by_nonemptyset: forall u r,
  is_graph r -> nonempty u -> sub u (domain r)
  -> nonempty (image_by_graph r u).
Proof. ir. nin H0. set (H1 _ H0). awii i. nin i. exists x. aw. ex_tac. Qed.

Theorem image_by_increasing: forall u u' r,
  is_graph r -> sub u u' -> sub (image_by_graph r u) (image_by_graph r u').
Proof. ir. uf image_by_graph. red. ir. Ztac. nin H3. ee. ex_tac. app H0. 
Qed. 

Lemma image_of_large: forall u r,  is_graph r -> 
  sub  (domain r) u ->  image_by_graph r u =  range r.
Proof. ir. app extensionality. app sub_image_by_graph. 
  wrr image_by_graph_domain. app image_by_increasing.
Qed.

(** Section of the graph [r] at [x] *)

Definition im_singleton r x := image_by_graph r (singleton x).

Lemma im_singleton_pr: forall r x y,
  inc y (im_singleton r x) = inc (J x y) r.
Proof. ir. uf im_singleton. ap iff_eq; ir. awi H. nin H. awi H. ee. ue.
  aw. ex_tac. fprops. 
Qed. 

Hint Rewrite im_singleton_pr : aw.


Lemma im_singleton_inclusion: forall r r', is_graph r -> is_graph r' ->
  (forall x, sub (im_singleton r x) (im_singleton r' x)) = sub r r'.
Proof. ir. app iff_eq; ir; red; ir. 
  set (H _ H2). wr (pair_recov i). wrr im_singleton_pr. app H1. aw. 
  aw. awi H2. app H1.
Qed.

(** ** EII-3-2 Inverse of a correspondence  *)

(** Inverse graph of [r] *)

Definition inverse_graph r :=
  Zo (product(range r)(domain r))
  (fun y=> inc (J (Q y)(P y)) r).

Lemma inverse_graph_is_graph: forall r, is_graph (inverse_graph r).
Proof. ir. red. ir. ufi inverse_graph H. Ztac. ap (pair_in_product H0).
Qed.

Hint Resolve inverse_graph_is_graph: fprops.

Lemma inverse_graph_rw: forall r y, is_graph r ->
  inc y (inverse_graph r) = (is_pair y &  inc (J (Q y)(P y)) r).
Proof. ir. app iff_eq. ir. ee. app (inverse_graph_is_graph H0).
  ufi inverse_graph H0. Ztac. am. ir. ee. uf inverse_graph. Ztac. aw. 
  ee. am. ex_tac. ex_tac.
Qed.

Lemma inverse_graph_alt: forall r, is_graph r ->
  inverse_graph r = fun_image r (fun z => J (Q z) (P z)).
Proof. ir. set_extens. rwi inverse_graph_rw H0.
  aw. nin H0.  ex_tac. aw. am.
  awi H0. nin H0. ee. rww inverse_graph_rw. wr H1. aw. ee; fprops. app H. 
Qed.

Lemma inverse_graph_pair: forall r x y, 
  inc (J x y) (inverse_graph r) = inc (J y x) r.
Proof. ir. uf inverse_graph. ap iff_eq; ir; Ztac. awi H1. am.
  uf range. uf domain. aw. ee. fprops. ex_tac.  aw. ex_tac. aw. aw.
Qed.

Lemma inverse_graph_pr2: forall r x y,
  related (inverse_graph r) y x = related r x y.
Proof. ir. uf related. app inverse_graph_pair. 
Qed. 

Hint Rewrite inverse_graph_pair : aw.
Hint Rewrite inverse_graph_pr2: bw.


Lemma inverse_graph_involutive: forall r, is_graph r ->
  inverse_graph (inverse_graph r) = r.
Proof. ir. assert (is_graph (inverse_graph r)). fprops.
  set_extens. rwii inverse_graph_rw H1. nin H1. awii H2. 
  rww inverse_graph_rw. set (H _ H1). split. am. aw. 
Qed. 

Lemma range_inverse: forall r, is_graph r ->
  range (inverse_graph r) = domain r.
Proof. ir. set_extens; aw; awii H0; fprops;nin H0. awi H0;ex_tac. 
  exists x0. aw. 
Qed.

Lemma domain_inverse: forall r, is_graph r ->
  domain (inverse_graph r) = range r.
Proof. ir.  transitivity (range (inverse_graph (inverse_graph r))).
  sy. rww range_inverse. fprops. rww inverse_graph_involutive.   
Qed. 

Lemma inverse_graph_emptyset: inverse_graph (emptyset) = emptyset.
Proof. uf inverse_graph. aw. srw. wr sub_emptyset. app Z_sub. 
Qed.

Hint Rewrite inverse_graph_emptyset: sw.

Lemma inverse_product: forall x y,
  inverse_graph (product x y) = product y x.
Proof. ir. set (product_is_graph (x:=x) (y:=y)).
  set_extens.  rwii inverse_graph_rw H. nin H. aw. awi H0. int.
  awi H. ee. rww inverse_graph_rw. eee. 
Qed.

Lemma inverse_identity_g: forall x,
  inverse_graph (identity_g x) = identity_g x.
Proof. ir. uf inverse_graph. rw identity_range; rw identity_domain. 
  set_extens. Ztac. awi H1. awi H0. ee. wr (pair_recov H0). aw. int.
  rwi inc_diagonal_rw H. ee. Ztac. aw. eee. wr (pair_recov H). aw. wr H1. int.  
Qed.

Hint Rewrite inverse_identity_g inverse_product: aw.

(** Inverse correspondence *)

Definition inverse_fun m :=
  corresp (target m) (source m) (inverse_graph (graph m)).

Lemma inverse_correspondence: forall m,  
  is_correspondence m -> is_correspondence (inverse_fun m).
Proof. ir. uf inverse_fun.  app corresp_create. red. 
  red. ir. ufi inverse_graph H0. Ztac. set (product_pr H1). ee. aw.
  red in H. rwi corr_propc H. eee.
Qed.

Lemma inverse_fun_involutive: forall m,
  is_correspondence m -> inverse_fun (inverse_fun m) = m.
Proof. ir. assert (is_graph (graph m)). fprops. 
  uf inverse_fun. uf corresp.  uf target; uf source; uf graph.
  red in H. ee. nin H. aw. rww inverse_graph_involutive. aw.
Qed.

Lemma inverse_source: forall f, source (inverse_fun f) = target f.
Proof. ir. uf inverse_fun. aw. Qed.

Lemma inverse_target: forall f, target (inverse_fun f) = source f.
Proof. ir. uf inverse_fun. aw. Qed.

Hint Rewrite inverse_source inverse_target : aw.


Hint Resolve inverse_correspondence: fprops.


(** Inverse image by a graph r of a set x *)

Definition inv_image_by_graph r x :=
  image_by_graph (inverse_graph r) x.

Definition inv_image_by_fun r x:=
  inv_image_by_graph(graph r) x.

Lemma inv_image_by_fun_pr: forall r x,
  inv_image_by_fun r x = image_by_fun (inverse_fun r) x.
Proof. ir. uf inv_image_by_fun. uf inverse_fun. uf image_by_fun.
  uf corresp.  uf graph. aw. 
Qed.

Lemma inv_image_graph_rw: forall x r y, 
  (inc y (inv_image_by_graph r x)) = (exists u, inc u x & inc (J y u) r).
Proof. ir. uf inv_image_by_graph. aw. uf related. ap iff_eq; ir; nin H.
  awi H. nin H. ex_tac. nin H. ex_tac. aw. 
Qed. 

Hint Rewrite inv_image_graph_rw: aw.

(** ** EII-3-3  Composition of two correspondences *) 

(** Composition of two graphs *)
Definition compose_graph r' r :=
  Zo (product(domain r)(range r'))
  (fun w => exists y, (inc (J (P w) y) r & inc (J y (Q w)) r')).
 
Lemma composition_is_graph: forall r r',
  is_graph (compose_graph r r').
Proof. ir. red. ir. ufi compose_graph  H. Ztac. ee. ap (pair_in_product H0).
Qed. 

Hint Resolve composition_is_graph: fprops.

Lemma inc_compose: forall r r' x,
  inc x (compose_graph r' r) =
  (is_pair x &( exists y, inc (J (P x) y) r& inc (J y (Q x)) r')).
Proof. ir. uf compose_graph. ap iff_eq; ir. Ztac. split. 
  ap (pair_in_product H0). am.
  ee. nin H0. ee. Ztac. uf domain. uf range. aw. ee. am. 
  ex_tac. aw. ex_tac. aw. ex_tac. 
Qed. 


Hint Rewrite inc_compose: aw.

Lemma compose_related: forall r r' x z,
  (related (compose_graph r' r) x z=
  exists y, related r x y & related r' y z).
Proof. ir. uf related. ap iff_eq; ir. awi H; int.  aw; eee. 
Qed. 

Hint Rewrite compose_related: aw.


Lemma compose_domain1: forall r r',
  sub (domain (compose_graph r' r)) (domain r).
Proof. ir. red. ir. awi H. nin H. ufi compose_graph H. Ztac.
  rwi product_inc_rw H0. ee. rwii pr1_pair H2. fprops.
Qed.

Lemma compose_range1: forall r r',
  sub (range (compose_graph r' r)) (range r').
Proof. ir. red. ir. awi H. nin H. ufi compose_graph H.
  Ztac. rwi product_inc_rw H0. ee. rwii pr2_pair H3. fprops.
Qed.

(** Proposition 3, inverse of composition *)
Theorem inverse_compose:forall r r',
  inverse_graph (compose_graph r' r) =
  compose_graph (inverse_graph r)(inverse_graph r').
Proof. ir.
  set_extens. aw. rwii inverse_graph_rw H. ee. am. awi H0. 
  ee. nin H1. exists x0. aw. int. fprops.  
  awi H. ee. nin H0. awi H0. ee. wr (pair_recov H). aw.  ee. fprops. ex_tac. 
Qed. 

(** Proposition 4,  associativity of composition *)
Theorem composition_associative: forall r r' r'',
  compose_graph r'' (compose_graph r' r) =
  compose_graph (compose_graph r'' r') r.
Proof. ir. 
  set_extens; awi H; ee; nin H0; ee; [awi H0 | awi H1] ; ee; nin H2; ee; aw. 
  ee. am. exists x1. ee. am. aw. ee. fprops.  ex_tac. 
  ee. am. ex_tac. aw. ee. fprops.  ex_tac. 
Qed.

(** Proposition 5 Image of composition *)
Theorem image_composition: forall r r' x,
  image_by_graph(compose_graph r' r) x = image_by_graph r' (image_by_graph r x).
Proof. ir.
  set_extens. awi H. nin H. ee. awi H0. nin H0. ee. nin H1. ee.
  aw. ex_tac. aw. ex_tac. 
  awi H. nin H.  ee. awi H. ee. nin H. ee. aw. ex_tac. aw. ee. fprops. ex_tac.
Qed.

(** More properties of composition *)

Lemma compose_domain:forall r r',
  is_graph r' -> 
  domain (compose_graph r' r) = inv_image_by_graph r (domain r').
Proof. ir. set (@composition_is_graph r' r).
  set_extens. awii H0. nin H0. awi H0. nin H0. nin H1. ee. 
  aw. ex_tac. ex_tac.  
  awi H0. nin H0. ee. awii H0. nin H0. aw. exists x1. aw. 
  ee. fprops. ex_tac. 
Qed.

Lemma compose_range: forall r r',
  is_graph r -> 
  range (compose_graph r' r) = 
  image_by_graph r' (range r).
Proof. ir. set (@composition_is_graph r' r).
  set_extens. awii H0. nin H0. awi H0. ee. nin H1. ee. aw.  ex_tac. ex_tac.
  awi H0. nin H0. ee. awii H0. nin H0. ee. aw. exists x1. aw. ee.  
  fprops. ex_tac. 
Qed. 

Lemma inverse_direct_image: forall r x,
  is_graph r -> sub x (domain r) ->
  sub x (inv_image_by_graph r (image_by_graph r x)).
Proof. ir. red. ir.  set (H0 _ H1). awii i. nin i. 
  aw. ex_tac. aw. ex_tac. 
Qed.

Lemma composition_increasing: forall r r' s s',
  sub r s -> sub r' s' -> sub (compose_graph r' r) (compose_graph s' s).
Proof. ir. red; ir.  awi H1. ee. nin H2. ee. aw. ee. am. 
  set (H0 _ H3). ex_tac. app H. 
Qed. 

(** Composition of two correspondences *)

Definition composableC r' r := 
  is_correspondence r & is_correspondence r' & source r' = target r.
Definition compose r' r :=
  corresp (source r)(target r') (compose_graph (graph r')(graph r)).

Lemma compose_correspondence: forall r' r,
  is_correspondence r -> is_correspondence r' -> 
  is_correspondence (compose r' r).
Proof. ir. uf compose. app corresp_create. red in H. red in H0. ee.
  red. red. ir.  awi H3. nin H3; nin H4. nin H4.
  set (H2 _ H4). awi i. set (H1 _ H5). awi i0. aw. int. 
Qed.

Lemma compose_of_sets: forall r' r x,
  image_by_fun(compose r' r) x = image_by_fun r' (image_by_fun r x).
Proof. ir. uf image_by_fun. 
  assert (graph (compose r' r) = compose_graph (graph r') (graph r)).
  uf compose. uf corresp. uf graph. aw. rw H. app image_composition.
Qed.

Lemma inverse_compose_cor: forall r r',
  inverse_fun (compose r' r) =  compose (inverse_fun r)(inverse_fun r').
Proof. ir. uf inverse_fun. uf compose. uf corresp. uf source; uf target;
  uf graph. aw.  rww inverse_compose.  
Qed.


(** Identity correspondence, will be shown to be a function later *)
Definition identity x := corresp x x (identity_g x). 

Lemma identity_corresp: forall x, 
  is_correspondence (identity x).
Proof. ir.  uf identity. app corresp_create. red.
  wr diagonal_is_identity. uf diagonal. app Z_sub.
Qed.

Lemma identity_source: forall x, source (identity x) = x.
Proof. ir. uf identity. aw. Qed.

Lemma identity_target: forall x, target (identity x) = x.
Proof. ir. uf identity. aw. Qed. 

Hint Rewrite  identity_source identity_target: aw.
Lemma compose_identity_left: forall m, 
   is_correspondence m -> compose (identity (target m)) m = m.
Proof. ir. uf compose.
  assert (compose_graph (identity_g(target m)) (graph m) = graph m).
  set_extens. awi H0. ee. nin H1. ee. awi H2. ee. rwi H3 H1. awii H1.
  assert (is_graph (graph m)). fprops.  set (H1 _ H0).
  aw. ee. am.  exists (Q x). eee. rww (pair_recov i). 
  assert (sub (range (graph m)) (target m)). fprops. aw. eee. app H2.
  aw. ex_tac. 
  assert (graph (identity (target m)) = (identity_g (target m))).
  uf identity. uf corresp. uf graph. aw. rw H1. rw H0. 
  uf identity. aw. ap corresp_recov. nin H; am.
Qed. 

Lemma compose_identity_right: forall m,
  is_correspondence m -> compose m (identity (source m)) = m.
Proof. ir. assert (is_graph (graph m)). fprops. uf compose. uf identity. aw.
  assert (Ha:is_graph (identity_g (source m))). fprops.
  assert (compose_graph (graph m) (identity_g (source m))= graph m).
  set_extens. awi H1. ee. nin H2. ee. awi H2. ee. wri H4 H3.
  awi H3. am. am. set (H0 _ H1). aw. ee. am. exists (P x). aw.
  assert (sub (domain (graph m))(source m)). fprops. eee. app H2. 
  aw. ex_tac. rww H1. app corresp_recov. nin H;am.
Qed. 

Lemma compose_identity_identity: forall x, 
  compose (identity x) (identity x) =  (identity x).
Proof. ir. set (@identity_corresp x). set (compose_identity_right i). awii e.
Qed.

Lemma identity_self_inverse: forall x, 
  inverse_fun (identity x) =  (identity x).
Proof. ir. uf inverse_fun. uf identity. aw. 
Qed.

End Correspondence.

Export Correspondence.

(** **  EII-3-4 Functions*)
Module Bfunction.

Import Correspondence.



(** This is a different but equivalent definition *)
Definition functional_graph r :=
  forall x y y', related r x y -> related r x y' ->  y=y'.

Lemma is_functional: forall r,
  (is_graph r & functional_graph r) = (fgraph r).
Proof. ir. uf functional_graph. uf related. app iff_eq. ir. ee. red. ee. am.
  ir. assert (J (P x) (Q x) = x). aw. app H.
  assert (J (P y) (Q y) = y). aw. app H. 
  wri H4 H1.  wri H5 H2. wri H3 H2. set (H0 _ _ _ H1 H2). 
  wr H4; wr H5; rw H3; rw e. tv.
  ir. split. fprops. ir. app (fgraph_pr H H0 H1).
Qed. 

(** A function is a correspondence with a functional graph whose
   source is the domain of the graph *)

Definition is_function f :=
  is_correspondence f &
  fgraph (graph f) & source f = domain (graph f).

Lemma is_function_pr: forall s t g,
  fgraph g -> sub (range g) t -> s = domain g ->
  is_function (corresp s t g).
Proof. ir. uf is_function. aw. eee. app corresp_create.
  rw corr_propc. nin H. eee.
Qed.

Lemma function_fgraph: forall f ,
  is_function f -> fgraph (graph f).
Proof. ir. red in H. ee.  am. Qed.

Lemma function_graph: forall f,
  is_function f -> is_graph (graph f).
Proof. ir. red in H. ee. red in H. eee. Qed.

Lemma f_domain_graph: forall f, is_function f -> domain (graph f) = source f.
Proof. ir. sy. red in H. eee.
Qed.

Lemma f_range_graph: forall f, is_function f -> sub (range (graph f))(target f).
Proof. ir. red in H. eee.
Qed.

Hint Rewrite f_domain_graph : aw.
Hint Resolve  function_graph function_fgraph : fprops.


(** Bourbaki functions as a record  *)

Record functionT : Type :=
  function_t {sourceT : Set; 
    targetT : Set; 
    graphT: Set;
    functionT_fgraph: fgraph graphT;
    functionT_src: domain graphT = sourceT; 
    functionT_trg: sub (range graphT) targetT 
}.


Definition functionT_fun (f:Set) (H: is_function f) :=
  function_t (function_fgraph H)(f_domain_graph H)(f_range_graph H).

Definition corresp_functionT f :=
  corresp (sourceT f) (targetT f) (graphT f).

Lemma source_T: forall f, sourceT f = source (corresp_functionT f).
Proof. ir. uf corresp_functionT. aw. Qed.

Lemma target_T: forall f, targetT f = target (corresp_functionT f).
Proof. ir. uf corresp_functionT. aw. Qed.

Lemma graph_T: forall f, graphT f = graph (corresp_functionT f).
Proof. ir. uf corresp_functionT. aw. Qed.


Hint Rewrite  source_T graph_T target_T : aw.

Lemma corresp_functionT_prop: forall f,
  is_function (corresp_functionT f).
Proof. ir.  red. ee. uf corresp_functionT. app corresp_create. rw corr_propc. 
  split. assert (fgraph  (graphT f)). nin f. simpl. am. fprops.
  nin f. simpl. rw functionT_src0. eee. uf corresp_functionT. nin f.  simpl. 
  aw. uf corresp_functionT. rw corresp_graph. rw corresp_source. nin f. sy; am.
Qed.

Hint Resolve corresp_functionT_prop: fprops.

Lemma image_by_fun_source: forall f, is_function f ->
  image_by_fun f (source f) =  range (graph f).
Proof. ir. uf image_by_fun. wrr f_domain_graph. 
  app image_by_graph_domain. fprops.
Qed.

Lemma related_inc_source: forall f x y,
  is_function f -> related (graph f) x y -> inc x (source f).
Proof. ir. red in H0. red in H. ee. ue. set (u:=graph f). aw. ex_tac. fprops.
Qed. 

(** The value of the function [f] at [x] is [W x f] *)
Definition W x f := V x (graph f).

Lemma W_pr3: forall f x, 
  is_function f -> inc x (source f) -> inc (J x (W x f)) (graph f).
Proof. ir. uf W. app fdomain_pr1. fprops. aw.
Qed.

Lemma in_graph_W: forall f x,
  is_function f -> inc x (graph f) -> x = (J (P x) (W (P x) f)).
Proof. ir. uf W. app in_graph_V. fprops.
Qed.

Lemma W_pr2: forall f x, is_function f -> 
  inc x (graph f) -> Q x = W (P x) f.
Proof. ir.  uf W. app pr2_V. fprops.
Qed.

Lemma W_pr: forall f x y, is_function f -> 
  inc (J x y) (graph f) -> W x f = y.
Proof. ir. set (in_graph_W H H0).  awi e. inter2tac.
Qed.


Lemma range_inc_rw: forall f y, is_function f ->
  inc y (range (graph f)) = exists x, (inc x (source f) & y = W x f).
Proof. ir. uf W. rww frange_inc_rw. aw. fprops.
Qed.

Lemma inc_W_range_graph: forall f x, is_function f -> inc x (source f)
  -> inc (W x f) (range (graph f)).
Proof. ir. rww range_inc_rw. ex_tac.  
Qed.

Lemma inc_W_target: forall f x, is_function f -> inc x (source f)
  -> inc (W x f) (target f).
Proof. ir. cp (inc_W_range_graph H H0). nin H. 
  nin H. rwi corr_propc H3. ee. app H6.
Qed.

Hint Resolve inc_W_target : fprops.

Lemma inc_pr1graph_source: forall f x y, is_function f -> 
  inc (J x y) (graph f) ->  inc x (source f).
Proof. ir. app (related_inc_source H H0).  
Qed.

Lemma inc_pr2graph_target: forall f x y, is_function f -> 
  inc (J x y) (graph f) ->  inc y (target f).
Proof. ir. wr (W_pr H H0).  cp (inc_pr1graph_source H H0). fprops.
Qed.

Lemma inc_pr1graph_source1:forall f x, is_function f -> 
  inc x (graph f) ->  inc (P x) (source f).
Proof. ir. cp (in_graph_W H H0). rwi H1 H0. ap (inc_pr1graph_source H H0).
Qed.

Lemma inc_pr2graph_target1:forall f x, is_function f -> 
  inc x (graph f) ->  inc (Q x) (target f).
Proof. ir. cp (in_graph_W H H0). rw H1.  aw. app inc_W_target.
  app inc_pr1graph_source1.
Qed.

Lemma W_image: forall f x y, is_function f -> sub x (source f) ->
  (inc y (image_by_fun f x) = exists u, inc u x & W u f = y).
Proof. ir. uf image_by_fun. aw. app iff_eq.
  ir.  nin H1. ee.  red in H2. ex_tac. ee. app W_pr. ir.
  nin H1. ee.  ex_tac. red. wr H2. app W_pr3. app H0. 
Qed.

Hint Rewrite W_image : aw.

Ltac graph_tac :=
  match goal with
    | |-  inc (J ?x (W ?x ?f)) (graph ?f) => app W_pr3 ; fprops
    |  h:inc (J ?x ?y) (graph ?f) |- W ?x ?f = ?y => app W_pr ; fprops
    |  h:inc (J ?x ?y) (graph ?f) |- ?y  = W ?x ?f => sy; app W_pr ; fprops
    | |- inc (W _ ?f) (range (graph ?f)) => app inc_W_range_graph ; fprops
    | |- inc (W _ ?f) (target ?f)  => app inc_W_target ; fprops

    | Ha:is_function ?X1, Hb: inc (J _ ?X2) (graph ?X1)
      |-  inc ?X2 (target ?X1)
        => ap (inc_pr2graph_target Ha Hb)
    | Ha:is_function ?X1, Hb: inc (J ?X2 _) (graph ?X1)
      |-  inc ?X2 (source ?X1)
        => ap (inc_pr1graph_source Ha Hb)
    | Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)
      |-  inc (P ?X2) (source ?X1)
        => ap (inc_pr1graph_source1 Ha Hb)
    | Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)
      |-  inc (Q ?X2) (target ?X1)
        => ap (inc_pr2graph_target1 Ha Hb)
  end.


Definition WT x f:= W x (corresp_functionT f).

Lemma defined_lemT: forall f x, 
  inc x (sourceT f) -> inc (J x (WT x f)) (graphT f).
Proof. ir. awi H. uf WT. aw. graph_tac. 
Qed.

Lemma inc_W_targetT: forall f x, inc x (sourceT f)
  -> inc (WT x f) (targetT f).
Proof. ir. awi H. uf WT. aw. fprops.
Qed.

Lemma is_function_functional: forall f, is_correspondence f->
  is_function f = (forall x, inc x (source f) -> 
    exists_unique (fun y => related (graph f) x y)).
Proof. ir. uf related. ap iff_eq; ir. split. exists (W x f). graph_tac. 
  ir.  nin H0. nin H4. nin H4. set (H6 _ _ H2 H3). awi e. 
  set (e (refl_equal x)). inter2tac.
  ir. red. split. am. red in H. rwi corr_propc H.
  set (g:=graph f) in *. ee. red. split. am. ir.
  assert (inc (P x) (source f)). app H2. aw. exists (Q x). aw. app H1.
  nin (H0 _ H7).  set (H1 _ H4). set (H1 _ H5). inter2tac. 
  app H9. aw. rw H6. aw.
  app extensionality. red. ir. aw. nin (H0 _ H4). am.
Qed.

Lemma image_of_fun_pr: forall f, image_of_fun f = image_by_fun f (source f).
Proof. ir. tv. Qed.

Lemma sub_image_target:
  forall f, is_function f -> sub (image_of_fun f) (target f).
Proof. ir. rw image_of_fun_pr. red. ir. awii H0. nin H0. nin H0. wr H1. 
  fprops. fprops.
Qed.


Lemma sub_image_target1: forall g x, is_function g ->
  sub (image_by_fun g x) (target g).
Proof. ir.  apw sub_trans (range (graph g)).  uf image_by_fun.
  app sub_image_by_graph. fprops. nin H. fprops. 
Qed.

(** The image of singleton by a function is a singleton*)
Lemma image_singleton: forall f x,
  is_function f -> inc x (source f) ->
  image_by_fun f (singleton x) = singleton (W x f).
Proof. ir. set (sub_singleton H0).  
  set_extens. aw. awi H1. nin H1. 
  nin H1. wr H2. db_tac. am. am.
  aw. exists x. split. fprops. db_tac.
Qed.

(** A lemma that says when two functions are equal *)

Lemma function_exten3: forall f g,
  is_function f -> is_function g -> graph f = graph g ->
  target f = target g -> source f = source g -> 
  f = g.
Proof. ir. nin H. nin H. wr (corresp_recov H).  nin H0. nin H0.
  wr (corresp_recov H0). ue; ue; ue.
Qed.

Lemma function_exten1: forall f g,
  is_function f -> is_function g -> graph f = graph g ->
  target f = target g -> 
  f = g.
Proof. ir. app function_exten3. do 2 wrr f_domain_graph. ue. 
Qed.

Lemma function_exten: forall f g,
  is_function f -> is_function g -> source f = source g ->
  target f = target g -> (forall x, inc x (source f) -> W x f = W x g)
  -> f = g.
Proof. ir. app function_exten3. set_extens.
  assert (inc (P x) (source f)). graph_tac. 
  rw (in_graph_W H H4). rww H3. graph_tac. ue.
  assert (inc (P x) (source g)).  graph_tac. wri H1 H5.
  rw (in_graph_W H0 H4). wrr H3. graph_tac. 
Qed. 

Lemma inv_image_complement: forall g x,
  is_function g ->
  inv_image_by_fun g (complement (target g) x) = 
  complement (source g) (inv_image_by_fun g x).
Proof. ir. assert (is_graph (graph g)). fprops.
  uf inv_image_by_fun. set_extens. awi H1. nin H1. ee.
  srwi H1; ee. srw. ee. graph_tac. dneg. awi H4. nin H4. ee. 
  assert (fgraph (graph g)). fprops. rww (fgraph_pr H6 H2 H5).
  srwi H1; ee. aw. assert (inc (J x0 (W x0 g))(graph g)). 
  graph_tac. ex_tac.  srw. split. fprops. dneg. aw. ex_tac. 
Qed.

(** The correspondence [acreate f] is a function  *)

Lemma prop_acreate: forall (A B:Set) (f:A->B) x, 
  inc x (graph (acreate f)) =  exists u:A, J (Ro u) (Ro (f u)) = x.
Proof. ir. uf acreate. aw. uf gacreate. app iff_eq. ir. nin (IM_exists H).
  exists x0. am. ir. nin H. app IM_inc. exists x0. am.
Qed.

Lemma acreate_fgraph : forall (A B:Set) (f:A->B),  fgraph(graph (acreate f)).
Proof. ir. red. ee. set (acreate_corresp f). fprops. ir. 
  rwi prop_acreate H. rwi prop_acreate H0. nin H; nin H0.
  replace x in *. replace y in *. awi H1. rww (R_inj H1).
Qed. 

Lemma domain_IM: forall (A:Set) (f:A->Set), 
   A = domain (IM (fun y : A => J (Ro y) (f y))).
Proof. ir. uf domain. set_extens. aw. exists (J x (f (Bo H))). split.
  app IM_inc.  exists (Bo H). rww B_eq. aw. awi H. nin H. nin H.
  nin (IM_exists H). wri H1 H0. awi H0. wr H0. app R_inc.
Qed.

Lemma acreate_function : forall (A B:Set) (f:A->B), 
  is_function (acreate f).
Proof. ir. red. ee.  app acreate_corresp. ap (acreate_fgraph f). 
  uf acreate. rw corresp_graph. aw. uf gacreate. wrr domain_IM.
Qed.

Hint Resolve acreate_function: fprops.

Lemma acreate_W : forall (A B:Set) (f:A->B) (x:A),
  W (Ro x) (acreate f) =  Ro (f x).
Proof. ir. assert (inc (Ro x) (source (acreate f))). uf acreate. aw. 
  app R_inc.  
  set (W_pr3 (acreate_function f) H). rwi prop_acreate i. nin i.
  wr (pr2_def H0). set (pr1_def H0). rww (R_inj e).
Qed.

(** We define [bcreate1 f] of type [source f-> target f]
 so that [ acreate (bcreate1 f) = f]  *)

Definition bcreate1 f (H:is_function f) :=
  fun x:source f => Bo (inc_W_target H (R_inc x)). 

Lemma prop_bcreate1: forall f (H:is_function f) (x:source f),
  Ro(bcreate1 H x) = W (Ro x) f.
Proof. ir. uf bcreate1. app B_eq. Qed.

Lemma bcreate_inv1: forall f (H:is_function f),
  acreate (bcreate1 H) = f.
Proof. ir. app function_exten. fprops. uf acreate; aw.  uf acreate; aw.   
  ir. ufi acreate H0.  awi H0. wr (B_eq H0). rw acreate_W. app prop_bcreate1.
Qed.

Lemma W_mapping: forall f A B (Ha:source f =A)(Hb:target f =B) x,
  is_function f -> inc x A -> inc (W x f) B.
Proof. ir. wri Ha H0. wr Hb. fprops. Qed.

(** We define [bcreate f a b] of type [a->b],
it satisfies [ acreate (bcreate f a b) = f]  *)
Definition bcreate f A B 
  (H:is_function f)(Ha:source f =A)(Hb:target f =B):=
  fun x:A => Bo (W_mapping Ha Hb H (R_inc x)). 

Lemma prop_bcreate2: forall f A B 
  (H:is_function f) (Ha:source f=A)(Hb:target f=B)(x:A),
  Ro(bcreate H Ha Hb x) = W (Ro x) f.
Proof. ir. uf bcreate. app B_eq.
Qed.

Lemma bcreate_inv2: forall f A B
  (H:is_function f) (Ha:source f=A)(Hb:target f=B),
  acreate (bcreate H Ha Hb) = f.
Proof. ir. app function_exten. fprops. uf acreate. aw. sy;am. 
  uf acreate; aw; sy; tv.
  ir. ufi acreate H0. awi H0. ir. wr (B_eq H0). rw acreate_W. app prop_bcreate2.
Qed.

Lemma acreate_source: forall (A B:Set) (f:A->B), source (acreate f)= A.
Proof. ir. uf acreate. aw.
Qed.

Lemma acreate_target: forall (A B:Set) (f:A->B), target (acreate f)= B.
Proof. ir. uf acreate. aw.
Qed.

Hint Rewrite acreate_source acreate_target: aw.

Lemma bcreate_inv3: forall (A B:Set) (f:A->B),
  bcreate  (acreate_function f) (acreate_source f)(acreate_target f) = f.
Proof. ir. app arrow_extensionality. ir. app R_inj.  
  rw prop_bcreate2. rww acreate_W. 
Qed.

Lemma bcreate_eq: forall f (H:is_function f),
  bcreate1 H = bcreate H (refl_equal (source f)) (refl_equal (target f)).
Proof.  ir. app arrow_extensionality. ir. app R_inj.
  rw prop_bcreate2. rww prop_bcreate1. 
Qed.


(** Function with empty graph *)
Definition empty_functionC : emptyset -> emptyset := fun x => x.
Definition empty_function:= acreate empty_functionC.


Lemma empty_function_function: is_function empty_function.
Proof. uf empty_function. fprops.
Qed.

Lemma empty_function_graph: graph empty_function = emptyset.
Proof. uf empty_function. uf acreate.  aw. uf gacreate. empty_tac. 
  nin (IM_exists H). elim x. 
Qed.

Lemma special_empty_function: forall f, is_function f ->
  graph f = emptyset -> source f = emptyset.
Proof. ir. red in H. ee. rw H2. rw H0. srw. 
Qed.

Lemma empty_function_prop:
  bcreate empty_function_function (acreate_source empty_functionC)
  (acreate_target empty_functionC)
  = empty_functionC.
Proof. app arrow_extensionality. ir. elim a. Qed.

(** Properties of the identity function *)

Lemma identity_function: forall x,
  is_function (identity x).
Proof. ir. uf identity. app is_function_pr.
  app identity_fgraph. rww identity_range.  fprops. rww identity_domain.
Qed.

Lemma identity_W: forall x y,
  inc y x -> W y (identity x) = y.
Proof. ir. uf W. uf identity. aw. app identity_ev.
Qed.

Hint Rewrite  identity_W: sw.
Hint Resolve identity_function: fprops.

Definition identityC (a:Set): a->a := fun x => x.
Implicit Arguments identityC [].

Lemma identity_prop: forall a, acreate (identityC a) = identity a.
Proof. ir. app function_exten. fprops. fprops. 
Qed. 

Lemma identity_prop2: forall a,
  bcreate (identity_function a) (identity_source a) (identity_target a) =
  identityC a.
Proof. ir. wr (bcreate_inv3 (identityC a)).  
  ap arrow_extensionality. ir. app R_inj.
  rw prop_bcreate2. rw prop_bcreate2.  rww identity_prop.
Qed.

(** A set is small if it has zero or one elements *)
Definition small_set x :=   
  forall u v, inc u x -> inc v x -> u = v.

(** Definition of a constant function  and of the constant function *)
Definition is_constant_function f :=
  (is_function f) & 
  (forall x x', inc x (source f) -> inc x' (source f) -> W x f = W x' f).
Definition is_constant_functionC x y (f:x->y) :=  forall a b, f a = f b.

Definition constant_functionC x y (a:y) := fun _:x => a.
Implicit Arguments constant_functionC [].

Definition constant_function (x y a:Set) (H:inc a y) :=
  acreate (constant_functionC x y (Bo H)).
Implicit Arguments constant_function [].

Lemma constant_source: forall x y a (H:inc a y),
  source (constant_function x y a H) = x.
Proof. ir. uf constant_function. aw. Qed.

Lemma constant_target: forall x y a  (H:inc a y),
  target (constant_function x y a H) = y.
Proof. ir. uf constant_function. aw. Qed.

Lemma constant_graph: forall x y a  (H:inc a y),
  graph (constant_function x y a H) = product x (singleton a).
Proof. ir. uf constant_function. uf constant_functionC. uf acreate. aw. 
  set_extens. ufi gacreate H0. nin (IM_exists H0).  wr H1. aw. ee. fprops.
  app R_inc. rw B_eq. fprops.
  uf gacreate. awi H0. ee. app IM_inc. exists (Bo H1).
  app pair_extensionality. fprops. aw. ap B_eq. aw. rw H2. ap B_eq.
Qed.

Lemma constant_function_fun: forall x y a (H: inc a y),
  is_function(constant_function x y a H).
Proof. ir. uf constant_function. fprops.
Qed.

Lemma constant_W: forall x y a (H:inc a y) b,
  inc b x ->  W b (constant_function x y a H) = a.
Proof. ir. app W_pr. app constant_function_fun. rw constant_graph. fprops.
Qed.

Lemma w_constant_functionC: forall  x y (a:y)  (z:x),
  constant_functionC x y a z = a.
Proof. tv. Qed.

Lemma constant_function_pr: forall f,
  is_function  f -> (is_constant_function f = 
    small_set (range (graph f))).
Proof. ir. uf small_set. app iff_eq. ir. rwii range_inc_rw H1.  
  rwii range_inc_rw H2. 
  nin H1; nin H2. ee. red in H0. ee. rw H4; rw H3. app H5.
  ir. red. ir. ee. am. ir. app H0.
  ap (inc_W_range_graph H H1). ap (inc_W_range_graph H H2). 
Qed.

Lemma constant_constant_fun: forall x y a (H: inc a y),
  is_constant_function(constant_function x y a H).
Proof. ir. red. ee. app constant_function_fun.  
  assert (source (constant_function x y a H) = x). uf constant_function.
  aw. tv. rw H0. ir. rww constant_W. rww constant_W.
Qed.

Lemma constant_fun_constantC: forall  x y a,
   is_constant_functionC (constant_functionC x y a).
Proof. ir. red. ir. tv.
Qed.

Lemma constant_function_prop2: forall (x y:Set) (a:y),
  bcreate (constant_function_fun x (R_inc a)) (constant_source x (R_inc a))
  (constant_target x (R_inc a)) = constant_functionC x y a.
Proof. ir. wr (bcreate_inv3 (constant_functionC x y a)).
  ap arrow_extensionality. ir. app R_inj. rw prop_bcreate2. rw prop_bcreate2.
  uf constant_function. rw B_back. tv.
Qed.

Lemma constant_fun_prC: forall x y (f:x->y)(b:x), is_constant_functionC f ->
  exists a:y, f= constant_functionC x y a.
Proof. ir.  exists (f b). app arrow_extensionality. ir. uf constant_functionC.
  app H.
Qed. 

Lemma constant_fun_pr: forall f (H:nonempty(graph f)),
  is_constant_function f ->
  exists a: target f,
  f= constant_function (source f) (target f) (Ro a) (R_inc a).
Proof. ir. red in H0.  ee.
  assert (is_graph (graph f)). fprops.
  assert (inc (rep (source f)) (source f)). app nonempty_rep. nin H. 
  exists (P y). assert (J (P y) (Q y) = y). aw. app H2. wri H3 H. graph_tac.
  assert (inc (W (rep (source f)) f) (target f)).
  fprops. exists (Bo H4). app function_exten. 
  app constant_function_fun.  uf constant_function. aw.
  uf constant_function. rww acreate_target.
  ir. rw constant_W. rw B_eq. app H1. am.
Qed. 


(** ** EII-3-5 Restrictions and extensions of functions *) 

(** Composition of Coq function *)
Definition composeC a b c (g:b->c) (f: a->b):= fun x:a => g (f x).

Lemma compositionC_associative: forall a b c d (f: c->d)(g:b->c)(h:a->b),
  composeC (composeC f g) h = composeC f (composeC g h).
Proof. ir. tv.
Qed.

Lemma compose_id_leftC: forall (a b:Set) (f:a->b),
  composeC (identityC b) f = f.
Proof. ir. app arrow_extensionality. 
Qed.
Lemma compose_id_rightC: forall (a b:Set) (f:a->b),
  composeC f (identityC a) = f.
Proof. ir. app arrow_extensionality.  
Qed.

(** Function associated to set inclusion *)

Definition inclusionC x y (H: sub x y):=
  fun u:x => Bo (H (Ro u) (R_inc u)).

Lemma inclusionC_pr: forall x y (H: sub x y) (a:x),
  Ro(inclusionC H a) = Ro a.
Proof. ir. uf inclusionC. ap B_eq. Qed.


Lemma inclusionC_identity: forall x,
  inclusionC (sub_refl (x:=x)) = identityC x.
Proof. ir. app arrow_extensionality. ir.  app R_inj. uf identityC. 
  rw inclusionC_pr. tv.
Qed.

Lemma inclusionC_compose: forall x y z (Ha:sub x y)(Hb: sub y z),
  composeC (inclusionC Hb)(inclusionC Ha) = inclusionC (sub_trans Ha Hb).
Proof. ir. app arrow_extensionality. ir. uf composeC. 
  app R_inj. rw inclusionC_pr. rw inclusionC_pr.  rw inclusionC_pr. tv.
Qed.

(** Restriction of a Coq function; agreement of subsets *)

Definition restrictionC  (x a b:Set) (f:a->b)(H: sub x a) :=
  composeC f (inclusionC H).

Definition agreeC (x a a' b b':Set) (f:a->b) (f':a'-> b')
  (Ha: sub x a)(Hb: sub x a') :=
  forall u:x, Ro(restrictionC  f Ha u) = Ro(restrictionC f' Hb u).


(**  The functions agree on [x] if they take the same value *)
Definition agrees_on x f f' :=
  (sub x (source f)) & (sub x (source f')) &  
  (forall a, inc a x -> W a f = W a f').

Lemma same_graph_agrees: forall f f',
  is_function f -> is_function f' -> graph f = graph f' ->
  agrees_on (source f) f f'.
Proof. ir. assert (source f = source f'). do 2 wrr f_domain_graph. rww H1.
  red. wr H2. eee. ir. set (W_pr3 H H3). rwi H1 i. wrr (W_pr H0 i). 
Qed.

Lemma function_exten2: forall f f',
  is_function f -> is_function f' ->
  (f =f') = ((source f =source f') & (target f= target f') &
    (agrees_on (source f) f f')).
Proof. ir. app iff_eq. ir. rww H1. eee. red. eee. 
  ir. ee. app function_exten. red in H3. ee. am.
Qed.

Lemma sub_function: forall f g,
  is_function f -> is_function g -> 
  (sub (graph f) (graph g)) = (agrees_on (source f) f g).
Proof. ir. ap iff_eq. ir.  split. fprops. split.
  do 2 wrr f_domain_graph. app sub_graph_domain.  ir.
  wrr (W_pr H0 (H1 _ (W_pr3 H H2))). 
  ir.  ee. red. ir. assert (inc (P x) (source f)). graph_tac.
  red in H1. ee. rw  (in_graph_W H H2). rww H5. graph_tac. 
Qed.

(** Restriction of the function to a part of it source *)

Lemma restr_domain2: forall f x,
  is_function f-> sub x (source f) -> 
  domain (restr (graph f) x) = x.
Proof. ir. red in H. ee. rww restr_domain1. ue.
Qed.

Lemma restr_range: forall f x,
  is_function f-> sub x (source f) -> 
  sub (range (restr (graph f) x)) (target f).
Proof. ir. uf range. uf restr. red. ir. awi H1. nin H1. nin H1. Ztac.
  wr H2. rw (W_pr2 H H3). fprops. 
Qed.


Definition restriction f x :=
  corresp x (target f) (restr (graph f) x).

Definition restriction1 f x :=
  corresp x (image_by_fun f x) (restr (graph f) x).

Lemma restriction_function: forall f x, 
  is_function f -> sub x (source f) ->
  is_function (restriction f x).
Proof. ir. uf restriction. app is_function_pr. fprops.
  app restr_range. rww restr_domain2. 
Qed.

Lemma restriction1_function: forall f x, 
  is_function f -> sub x (source f) ->
  is_function (restriction1 f x).
Proof. ir. uf restriction1. app is_function_pr. fprops.
  uf range. uf restr. red. ir. awi H1. nin H1. nin H1. Ztac. aw. ex_tac.
  wrr (W_pr2 H H3). rww restr_domain2. 
Qed.

Hint Resolve  restriction_function restriction1_function: fprops.

Lemma restriction_W: forall f x a,
  is_function f -> sub x (source f) ->
  inc a x ->  W a (restriction f x) = W a f.
Proof. ir. uf W. uf restriction.  aw.  bw. fprops. aw.
Qed.

Lemma restriction1_W: forall f x a,
  is_function f -> sub x (source f) ->
  inc a x ->  W a (restriction1 f x) = W a f.
Proof. ir. uf W. uf restriction1.  aw. bw. fprops. aw.
Qed.

(** [g] extends [f] if its restriction to the source of [f] is [f] *)
Definition extends g f := 
  (is_function f) & (is_function g) & (sub (graph f) (graph g))
  & (sub (target f)(target g)).

Definition extendsC (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a')  := 
  sub b b' & agreeC g f H (sub_refl (x:=a)).

Lemma source_extends: forall f g,
  extends g f -> sub (source f) (source g).
Proof. ir. red in H. ee. do 2 wrr f_domain_graph. app sub_graph_domain.
Qed. 

Lemma W_extends: forall f g x,
  extends g f -> inc x (source f) -> W x f = W x g.
Proof. ir. cp (source_extends H).
  red in H. ee. assert  (inc (J x (W x f)) (graph g)). app H3.
  graph_tac. rww (W_pr H2 H5).
Qed.

Lemma extendsC_pr : forall (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a'),
  extendsC g f H -> forall x:a, Ro (f x) = Ro(g (inclusionC H x)).
Proof. ir.  red in H0. ee.  ufi agreeC H1.  cp (H1 x).
  ufi restrictionC H2. ufi composeC H2. rww H2.
  rww inclusionC_identity. 
Qed.

Lemma function_extends_restr: forall f x,
  is_function f -> sub x (source f) ->
  extends f (restriction f x).
Proof. ir. red. ee. fprops. am. 
  uf restriction. aw. app restr_sub.
  uf restriction. aw. fprops. 
Qed.

Lemma function_extends_restC: forall (x a b:Set) (f:a->b)(H:sub x a),
  extendsC f (restrictionC f H) H.
Proof. ir. red. ee. fprops. red. uf restrictionC. 
  rw inclusionC_identity. rw compose_id_rightC.  tv.
Qed.

Lemma agrees_same_restriction: forall f g x,
  is_function f -> is_function g -> agrees_on x f g ->
  target f = target g -> 
  restriction f x =
  restriction g x.
Proof. ir.  red in H1. ee. apply function_exten. fprops. fprops.
  uf restriction. aw. uf restriction. aw.
  ir.  ufi restriction H5. awi H5.
  do 2 rww restriction_W. app H4.
Qed.

Lemma agrees_same_restrictionC: forall (a a' b x:Set)  (f:a->b)(g:a'->b)
  (Ha: sub x a)(Hb: sub x a'),
  agreeC f g Ha Hb -> restrictionC f Ha = restrictionC g Hb.
Proof. ir. red in H. app arrow_extensionality. ir. app R_inj.
Qed.

Lemma restriction_graph1: forall f x,
  is_function f -> sub x (source f) ->
  graph (restriction f x) = 
  intersection2 (graph f)(product x (target f)).
Proof. ir. uf restriction. aw. set_extens.  awi H1.  ee. inter2tac. aw.
  assert (is_pair x0).  assert (is_graph (graph f)). fprops. 
  app H3. eee. graph_tac. 
  aw. nin (intersection2_both H1). split. am. awi H3. int.
Qed.

Lemma restriction_recovers: forall f x,
  is_function f -> sub x (source f) ->
  restriction f x = corresp x (target f) 
    (intersection2 (graph f)(product x (target f))).
Proof. ir. wrr (restriction_graph1 H H0). uf restriction.  aw.
Qed.

(** Restriction of a function on the source and target *)

Definition restriction2 f x y := 
  corresp x y (intersection2 (graph f) (product x (target f))).

Definition restriction2_axioms f x y :=
  is_function f &
  sub x (source f) & sub y (target f) & sub (image_by_fun f x) y.

Lemma restriction2_graph: forall f x y, 
  sub (graph (restriction2 f x y)) (graph f).
Proof. ir. uf restriction2. aw. app intersection2sub_first. Qed.

Lemma inc_graph_restriction2: forall f x y a b,
  (inc (J a b) (graph (restriction2 f x y))) =
  (inc (J a b) (graph f) & inc a x & inc b (target f)).
Proof. ir. uf restriction2. aw.  app iff_eq. ir.
  nin (intersection2_both H). split. am. awi H1. eee.
  ir. ee. inter2tac. fprops.
Qed.

Lemma restriction2_props: forall  f x y, 
  restriction2_axioms f x y ->
  domain (intersection2 (graph f) (product x (target f))) = x.
Proof. ir. assert (is_graph (intersection2 (graph f) (product x (target f)))).
  red. ir.  nin (intersection2_both H0). awi H2. int.
  set_extens. awi H1. nin H1. nin (intersection2_both H1). awi H3.  int. am.
  aw. red in H. ee. exists (W x0 f). inter2tac. graph_tac. aw.  eee.
Qed.

Lemma restriction2_function: forall  f x y, 
  restriction2_axioms f x y ->  
  is_function (restriction2 f x y).
Proof. ir. assert (Ha:=restriction2_props H). red in H. ee. uf restriction2.
  set (g := intersection2 (graph f) (product x (target f))).
  assert (Hb: fgraph g).  uf g. apw sub_graph_fgraph (graph f). fprops. 
  ap intersection2sub_first.
  app is_function_pr. uf g.  red. ir. ufi g H3. awi H3. nin H3. app H2.
  aw. exists x1. nin (intersection2_both H3). awi H5. eee. graph_tac. fprops.
  sy; am.
Qed.

Hint Resolve restriction2_function: fprops.


Lemma restriction2_W: forall f x y a,
  restriction2_axioms f x y ->
  inc a x -> W a  (restriction2 f x y) = W a f.
Proof. ir. assert (Ha:=restriction2_props H).  
  uf W. uf restriction2.  aw. nin H. ee. app sub_graph_ev. fprops.
  ap intersection2sub_first. ue. 
Qed.


Lemma function_rest_of_prolongation: forall f g,
  extends g f -> f = restriction2 g (source f) (target f).
Proof. ir. red in H. ee. rwi (sub_function H H0) H1.  red in H1. ee.
  assert (sub (image_by_fun g (source f)) (target f)).
  red. ir. awi H5. nin H5. nin H5. wr H6. wrr H4. fprops. am. am.
  assert (restriction2_axioms g (source f) (target f)).  red; auto.
  app function_exten. fprops.
  uf restriction2; aw.  uf restriction2; aw.
  ir. rww restriction2_W. app H4.  
Qed.

Definition restriction2C (a a' b b':Set) (f:a->b)(Ha:sub a' a)
  (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') := 
  fun u=> Bo (H u).

Lemma restriction2C_pr: forall  (a a' b b':Set) (f:a->b)(Ha:sub a' a)
  (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') (x:a'),
  Ro (restriction2C f Ha H x) = W (Ro x) (acreate f).
Proof. ir.  uf restriction2C.  rw B_eq. 
  set (y:=inclusionC Ha x).  assert (Ro y = Ro x). uf y. uf inclusionC.
  rw B_eq. tv. wr H0. rww acreate_W. 
Qed.

Lemma restriction2C_pr1: forall (a a' b b':Set) (f:a->b)
  (Ha:sub a' a)(Hb:sub b' b)
  (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b'),
  composeC f (inclusionC Ha) = composeC (inclusionC Hb) (restriction2C f Ha H).
Proof. ir. app arrow_extensionality. ir. uf composeC.
  app R_inj. rw inclusionC_pr. rw restriction2C_pr. 
  cp (inclusionC_pr Ha a0). wr H0.   rww acreate_W.
Qed.

(** ** EII-3-6 Definition of a function by means of a term *) 

(** Function from a to b associated to the mapping f *)
Definition BL f a b :=
  corresp a b (L a f).

Lemma bl_source : forall f a b, source (BL f a b) = a.
Proof. ir.  uf BL; uf L; aw.  Qed.

Lemma bl_target : forall f a b, target (BL f a b) = b.
Proof. ir.  uf BL; uf L; aw.  Qed.

Hint Rewrite bl_source bl_target : aw.

Lemma bl_graph1: forall f a b c, 
  inc c (graph (BL f a b)) -> c = J (P c) (f (P c)).
Proof. ir. ufi BL H. ufi L H. awi H. nin H. ee. wr H0. aw.
Qed.

Lemma bl_graph2: forall f a b c, 
  inc c a -> inc (J c (f c)) (graph (BL f a b)).
Proof. ir.  uf BL. uf L. aw. ex_tac.
Qed.

Lemma bl_graph3: forall f a b c, 
  inc c (graph (BL f a b)) -> inc (P c) a.
Proof. uf BL. uf L. ir. awi H. nin H. nin H. wr H0. aw. 
Qed.

Lemma bl_graph4: forall f a b c, 
  inc c (graph (BL f a b)) -> f (P c) = (Q c). 
Proof. uf BL. uf L. ir. awi H. nin H. ee. wr H0. aw.  
Qed.

(** In order for [(BL f a b)]  to be a function,  the following must be satisfied *)
Definition transf_axioms f a b :=
  forall c, inc c a -> inc (f c) b. 

Lemma bl_function: forall f a b, 
  transf_axioms f a b -> is_function (BL f a b).
Proof. ir. uf BL. app is_function_pr. gprops. 
  red in H. red. ir. rwi L_range H0. awi H0. nin H0. nin H0. wr H1. app H. bw.
Qed.

Lemma bl_W: forall f a b c, 
  transf_axioms f a b ->  inc c a-> W c (BL f a b) = f c.
Proof. ir. ap W_pr. app bl_function. app bl_graph2.
Qed. 


Hint Rewrite bl_W : aw.

Lemma bl_recovers: forall f,
  is_function f -> BL (fun z => W z f)(source f)(target f) = f.
Proof. ir. assert(transf_axioms (fun z => W z f) (source f) (target f)).
  red. ir. fprops. app function_exten;aw. app bl_function. ir. aw. 
Qed.

(** Functions associated to P and Q*)

Definition first_proj g := BL P g (domain g).
Definition second_proj g := BL Q g (range g).

Lemma first_proj_W: forall g x, 
  inc x g -> W x (first_proj g) = P x.
Proof. ir. uf first_proj. aw. red. ir. uf domain.  aw.  ex_tac.
Qed.

Lemma second_proj_W: forall g x, 
  inc x g -> W x (second_proj g) = Q x.
Proof. ir. uf second_proj. aw. red. ir. uf range. aw. ex_tac.
Qed.

Lemma first_proj_function:forall g, 
  is_function (first_proj g).
Proof. ir. uf first_proj. app bl_function. red. ir. uf domain. aw. ex_tac.
Qed. 

Lemma second_proj_function :forall g, 
  is_function (second_proj g). 
Proof. ir. uf second_proj. app bl_function. red. ir.  uf range. aw. ex_tac.
Qed.


(** ** EII-3-7  Composition of two functions. Inverse function *) 

(** Condition for composition to be a function  *)
Definition composable g f :=  
  is_function g & is_function f &  source g = target f.

Lemma composable_pr: forall f g, composable g f ->
  fcomposable (graph g) (graph f).
Proof. ir. red. red in H. ee. fprops. fprops. aw. rw H1. app f_range_graph.
Qed.

Lemma composable_pr1: forall f g, composable g f ->
  graph (compose g f) = fcompose (graph g) (graph f).
Proof. ir. cp (composable_pr H). wrr alternate_compose. red in H. ee.
  assert (fgraph (graph f)). fprops.  assert (fgraph (graph g)). fprops. 
  uf compose. aw. uf gcompose. uf L. set_extens. awi H5. nin H5. nin H6. ee. 
  aw. exists (P x). split. graph_tac.
  set (pr2_V H3 H6). awi e. wr e. set (pr2_V H4 H7). awi e0. wr e0. aw.
  set (ff:= graph f) in *. awi H5. nin H5. ee. awi H5. nin H5.
  set (pr2_V H3 H5). awi e. wri e H6.
  aw. wr H6. aw. split. fprops. exists x1. split. am. app fdomain_pr1.
  aw. rw H2. ufi ff H5. graph_tac. fprops.
Qed.

Lemma compose_domain:forall g f,
  composable g f-> 
  domain (graph(compose g f)) = domain (graph f).
Proof. ir. rww composable_pr1. app fcomposable_domain.
  app composable_pr.
Qed.


Lemma compose_source: forall f g, source (compose g f) = source f.
Proof. ir. uf compose. aw. Qed.

Lemma compose_target: forall f g, target (compose g f) = target g.
Proof. ir. uf compose. aw. Qed.

Hint Rewrite compose_source compose_target : aw.


(** Proposition 6: composition of functions is a function *)
Theorem compose_function: forall g f, composable g f
  -> is_function (compose g f).
Proof. ir. cp (composable_pr1 H). cp (compose_domain H). rwi H0 H1.
  red in H. ee. ufi compose H0. awi H0. 
  assert (fgraph (fcompose (graph g) (graph f))). app fcompose_fgraph.
  rwi (f_domain_graph H2) H1. symmetry in H1.
  uf compose. rw H0.
  app is_function_pr. apw sub_trans (range (graph g)). 
  app fcompose_range. fprops. nin H. fprops. 
Qed.


(** Definition of injectivity, surjectivity and bijectivity *)
Definition injective f:=
  is_function f & 
  (forall x y, inc x (source f) -> inc y (source f) ->
    W x f = W y f -> x = y).

Definition surjective f :=
  is_function f & image_of_fun f = target f.

Definition bijective f :=
  injective f & surjective f.

(** We give here here some characterizations of injective, surjective, bijective functions *)


Lemma inj_is_function: forall f, injective f -> is_function f.
Proof. ir. nin H; am. Qed.

Lemma surj_is_function: forall f, surjective f-> is_function f.
Proof. ir. nin H; am. Qed.

Lemma bij_is_function: forall f, bijective f-> is_function f.
Proof. ir. nin H. nin H. am. Qed.

Ltac fct_tac := 
  match goal with
    | H:bijective ?X1 |- is_function ?X1 => exact (bij_is_function H)
    | H:injective ?X1 |- is_function ?X1 => exact (inj_is_function H)
    | H:surjective ?X1 |- is_function ?X1 => exact (surj_is_function H)
    | H:is_function ?X1 |- is_correspondence ?X1 =>
      nin H; am
    | H:is_function ?g |- sub (range (graph ?g)) (target ?g)
      => nin H; fprops
    | H:composable ?X1 _ |- is_function ?X1 => destruct H as [H _ ]; exact H
    | H:composable _ ?X1 |- is_function ?X1 => destruct H as [_ [H _ ]]; exact H
    | H:composable ?f ?g |- is_function (compose ?f ?g ) =>
     ap (compose_function H)
    | H:is_function ?f |- is_function (compose ?f ?g ) =>
     ap compose_function; red; ee; tv
    | H:is_function ?g |- is_function (compose ?f ?g ) =>
     ap compose_function; red; ee; tv
    | Ha:is_function ?f, Hb:is_function ?g |- ?f = ?g =>
      app function_exten
  end.

(** More properties of function composition *)

Lemma compose_W: forall g f x,  composable g f ->
  inc x (source f) -> W x (compose g f) = W (W x f) g.
Proof. ir. uf W. rww composable_pr1. app fcompose_ev. 
  rw fcomposable_domain. aw. red in H; eee. app composable_pr.
Qed.

Hint Rewrite compose_W: aw.

Lemma composable_acreate:forall (a b c:Set) (f: a-> b)(g: b->c),
  composable (acreate g) (acreate f).
Proof. ir. red. eee. aw.
Qed.

Lemma compose_acreate:forall (a b c:Set) (g: b->c)(f: a-> b),
  compose (acreate g) (acreate f) = acreate(composeC g f).
Proof. ir. set (composable_acreate f g).
  app function_exten. fct_tac. fprops. aw. aw. aw. 
  ir. aw. wr (B_eq H). uf composeC.  repeat rw acreate_W. tv.
Qed.

Lemma compose_assoc: forall f g h,
  composable f g -> composable g h ->
  compose (compose f g) h = compose f (compose g h).
Proof. ir.  
  assert (is_function (compose f g)). fct_tac.
  assert (is_function (compose g h)). fct_tac.   
  assert (composable (compose f g) h).  red in H0. red. eee.  aw.
  assert (composable f (compose g h)). red in H; red; eee. aw.
  ap function_exten.  fct_tac. fct_tac. aw. aw. aw. aw. ir. aw. 
  red in H0. ee. rw H7. fprops.
Qed.

Lemma compose_id_left: forall m, 
  is_function m-> compose (identity (target m)) m = m.
Proof. ir. app compose_identity_left. fct_tac.  
Qed.

Lemma compose_id_right: forall m, 
  is_function m-> compose m  (identity (source m)) = m.
Proof. ir. app compose_identity_right. fct_tac.
Qed.

Lemma injective_pr: forall f x x' y,
  injective f -> related (graph f) x y -> related (graph f) x' y -> x = x'.
Proof. ir. nin H.  app H2. app (related_inc_source H H0).
  app (related_inc_source H H1).  rw (W_pr H H0). rw (W_pr H H1). tv.
Qed.

Lemma injective_pr3: forall f x x' y,
  injective f -> inc (J x y) (graph f) -> inc (J x' y) (graph f) -> x = x'.
Proof. ir.  app (injective_pr H H0 H1).
Qed.

Lemma injective_pr_bis: forall f,
  is_function f -> (forall x x' y,
  related (graph f) x y -> related (graph f) x' y -> x = x') -> injective f.
Proof. ir. red. ee. am. ir. app (H0 x y (W x f)).
  ap (W_pr3 H H1).  rw H3. ap (W_pr3 H H2). 
Qed.

Lemma surjective_pr: forall f y,
  surjective f -> inc y (target f) ->
  exists x, inc x (source f) & related (graph f) x y .
Proof. ir. red in H. ee. wri H1 H0. ufi image_of_fun H0. awi H0. am.
Qed.

Lemma surjective_pr2: forall f y,
  surjective f -> inc y (target f) -> exists x, inc x (source f) & W x f = y.
Proof. ir. nin (surjective_pr H H0). exists x. ee. am. app W_pr. fct_tac.
Qed.

Lemma surjective_pr3: forall f,
  surjective f -> range (graph f) = target f.
Proof. ir. app extensionality. nin H. fct_tac. 
  red. ir. nin (surjective_pr H H0). aw. ee. exists x0. app H2. nin H. fprops.
Qed. 

Lemma surjective_pr4: forall f,
  is_function f-> range (graph f) = target f -> surjective f.
Proof. ir. red. ee. am. uf image_of_fun. red in H. ee. rw H2.
  rww image_by_graph_domain. fprops.
Qed. 

Lemma surjective_pr5: forall f,
  is_function f -> (forall y, inc y (target f) ->
  exists x, inc x (source f) & related (graph f) x y) -> surjective f.
Proof. ir. app surjective_pr4. app extensionality. fct_tac. 
  red. ir. nin (H0 _ H1). nin H2. red in H3. aw. ex_tac. fprops.
Qed.

Lemma surjective_pr6: forall f,
  is_function f-> (forall y, inc y (target f) ->
  exists x, inc x (source f) & W x f = y) -> surjective f.
Proof. ir. app surjective_pr5. ir. nin (H0 _  H1). nin H2. ex_tac.
  wr H3. red. graph_tac. 
Qed.

Lemma bl_injective: forall f a b, transf_axioms f a b ->
  (forall u v, inc u a-> inc v a -> f u = f v -> u = v) ->
  injective (BL f a b).
Proof. ir. red. ee. app bl_function. aw. ir.
  rwii bl_W H3. rwii bl_W H3. app H0.
Qed.

Lemma bl_surjective: forall f a b, transf_axioms f a b ->
  (forall y, inc y b -> exists x, inc x a & f x = y) -> 
  surjective (BL f a b).
Proof. ir. app surjective_pr6. app bl_function. aw. ir.
  nin (H0 _ H1). nin H2. ex_tac. rww bl_W.
Qed.

Lemma bl_bijective: forall f a b, transf_axioms f a b ->
  (forall u v, inc u a-> inc v a -> f u = f v -> u = v) ->
  (forall y, inc y b -> exists x, inc x a & f x = y) -> 
  bijective (BL f a b).
Proof. ir. split. app bl_injective. app  bl_surjective.
Qed.

Lemma bijective_pr: forall f y,
  bijective f -> inc y (target f) -> 
  exists_unique (fun x=> inc x (source f) & W x f = y).
Proof. ir. red in H. red. ee. app surjective_pr2. ir. ee. wri H4 H5. 
  red in H. ee.  app H6.
Qed.


Lemma function_exten4: forall f g, source f = source g ->
  surjective f -> surjective g -> 
  (forall x, inc x (source f) -> W x f = W x g) -> f = g.
Proof. ir. cp (surjective_pr3 H0). cp (surjective_pr3 H1). nin H0; nin H1.
  assert (graph f = graph g). app fgraph_exten. fprops. fprops.  aw. ir.
  awii H7. app (H2 _ H7). fprops. app function_exten1. wr H3; wr H4. rww H7.
Qed.



(** Bijectivity of Coq functions  *)
Definition injectiveC (a b:Set) (f:a->b) := forall u v, f u = f v -> u =v.
Definition surjectiveC (a b:Set) (f:a->b) := forall u, exists v, f v = u.
Definition  bijectiveC (a b:Set) (f:a->b) := injectiveC f & surjectiveC f.

Lemma bijectiveC_pr: forall (a b:Set) (f:a->b) (y:b),
  bijectiveC f ->   exists_unique (fun x:a=> y = f x).
Proof. ir. red in H. ee. uf exists_unique. ee. red in H0.  cp (H0 y). nin H1.
  exists x. sy. am. red in H. ir. rwi H1 H2. app H.
Qed.

Lemma bcreate_injective: forall f a b
  (H:is_function f)(Ha:source f =a)(Hb:target f =b),
  injective f -> injectiveC (bcreate H Ha Hb).
Proof. ir. red. ir. red in H0. ee. app R_inj.
  app H2. rw Ha. app R_inc. rw Ha. app R_inc. 
  assert (Ro (bcreate H Ha Hb u) = Ro (bcreate H Ha Hb v)). rw H1. tv.
  rwi prop_bcreate2 H3. rwi prop_bcreate2 H3. am. 
Qed.

Lemma bcreate_surjective: forall f a b
  (H:is_function f)(Ha:source f =a)(Hb:target f =b),
  surjective f -> surjectiveC (bcreate H Ha Hb).
Proof. ir. red. ir.  
  assert (inc (Ro u) (target f)). rw Hb. app R_inc. cp (surjective_pr2 H0 H1).
  nin H2. ee. rwi Ha H2. exists (Bo H2). app R_inj. wr H3. rw prop_bcreate2.
  rw B_eq. tv.
Qed.

Lemma bcreate_bijective: forall f a b
  (H:is_function f)(Ha:source f =a)(Hb:target f =b),
  bijective f -> bijectiveC (bcreate H Ha Hb).
Proof. ir. red in H0. ee. red.  ee. 
  app bcreate_injective. app bcreate_surjective.
Qed.

Lemma bcreate1_injective: forall f (H:is_function f),
  injective f -> injectiveC (bcreate1 H).
Proof. ir.  rw (bcreate_eq H). app bcreate_injective. Qed.

Lemma bcreate1_surjective: forall f (H:is_function f),
  surjective f -> surjectiveC (bcreate1 H).
Proof. ir.  rw (bcreate_eq H). app bcreate_surjective. Qed.

Lemma bcreate1_bijective: forall f (H:is_function f),
  bijective f -> bijectiveC (bcreate1 H).
Proof. ir. rw (bcreate_eq H). app bcreate_bijective. Qed.

Lemma acreate_injective: forall (a b:Set) (f:a->b),
  injectiveC f -> injective (acreate f).
Proof. ir. red in H; ee. red. ee. fprops. intros x y Ha Hb. 
  ufi acreate Ha; awi Ha.   ufi acreate Hb; awi Hb.
  wr (B_eq Ha). wr (B_eq Hb). rw (acreate_W f (Bo Ha)). 
  rw (acreate_W f (Bo Hb)). ir. cp (R_inj H0). rww (H  _ _ H1). 
Qed.

Lemma acreate_surjective: forall (a b:Set) (f:a->b),
  surjectiveC f -> surjective (acreate f).
Proof. ir. app surjective_pr6. fprops. aw.
   ir.  nin (H (Bo H0)). 
   exists (Ro x). ee. app R_inc. rw acreate_W. rw H1. rw B_eq. tv.
Qed.

Lemma acreate_bijective: forall (a b:Set) (f:a->b),
  bijectiveC f -> bijective (acreate f).
Proof. ir. red in H; ee. red. ee. app acreate_injective. app acreate_surjective.
Qed.

(** Equipotent means there is a bijection between the sets *)
Definition equipotent x y := 
  exists z, bijective z & source z = x & target z = y.

Lemma equipotentC: forall x y, equipotent x y = exists f:x->y, bijectiveC f.
Proof. ir. app iff_eq.  ir. nin H. nin H.  assert (is_function x0).
  red in H; ee; red in H; ee. am.  ee. exists (bcreate H1 H0 H2). 
  app bcreate_bijective. ir.  nin H. red. exists (acreate x0). ee.
  app acreate_bijective. aw. aw.
Qed.

(** Injectivity and surjectivity of identity and restriction *) 
Lemma identity_bijective: forall x,
  bijective (identity x).
Proof. ir. set (identity_function x).
  red. ir. ee. red. ee. am. aw. ir. srwi H1; tv. 
  app surjective_pr6.  aw. ir. exists y. split. am. srw.
Qed.

Lemma identityC_bijective: forall x,
  bijectiveC (identityC x).
Proof. red. ir. uf identityC. ee. red. tv. red. ir. exists u. tv.
Qed.

Lemma restriction2_injective: forall f x y,
  injective f -> restriction2_axioms f x y 
  -> injective (restriction2 f x y).
Proof. ir. red. ee. app restriction2_function. 
  assert (Ht:source (restriction2 f x y) = x). uf restriction2. aw. rw Ht.
  ir. rwii restriction2_W H3. rwii restriction2_W H3. nin H. red in H0. ee.
  app H4; app H5. 
Qed.

Lemma restriction2_surjective: forall f x y,
  restriction2_axioms f x y ->
  source f = x -> image_of_fun f = y ->
  surjective (restriction2 f x y).
Proof. ir. app surjective_pr6.  app restriction2_function. ir.
  ufi restriction2 H2. awi H2.
  ir. wri H1 H2. ufi image_of_fun H2. awi H2. nin H2. ee. exists x0.
  rwi H0 H2. ee. uf restriction2. aw. rww restriction2_W. app W_pr. 
  red in H; eee. 
Qed.

Lemma restriction1_surjective: forall f x,
  is_function f -> sub x (source f) ->
  surjective (restriction1 f x).
Proof. ir. app surjective_pr6.  app restriction1_function. ir.
  ufi restriction1 H1. awii H1. ufi image_of_fun H1. nin H1. ee. 
  exists x0. ee. uf restriction1. aw. rww restriction1_W. 
Qed.

Lemma restriction1_bijective: forall f x,
  injective f -> sub x (source f) ->
  bijective (restriction1 f x).
Proof. ir. nin H. split. red. split. app restriction1_function.
  assert (Ht:source (restriction1 f x) = x). uf restriction1. aw. rw Ht.
  ir. do 2 rwii restriction1_W H4. app H1. app H0. app H0. 
  app restriction1_surjective.
Qed.



(** Extension of a function by adding f(x)=y *)

Definition tack_on_f f x y:=
  corresp (tack_on (source f) x)
  (tack_on (target f) y)  (tack_on (graph f) (J x y)).

Lemma tack_on_corresp: forall  f x y,
  is_correspondence f ->  is_correspondence (tack_on_f f x y).
Proof. ir. uf tack_on_f. app corresp_create. cp (corresp_propb H). red. 
  red. ir. rwi tack_on_inc H1. nin H1. set (H0 _ H1). awi i. aw. eee. rw H1.
  aw. eee.
Qed.

Lemma tack_on_function: forall  f x y,
  is_function f -> ~ (inc x (source f)) -> is_function (tack_on_f f x y).
Proof. ir.  red in H. ee. uf tack_on_f. app is_function_pr. 
  app tack_on_fgraph. ue.
  rw tack_on_range. red. ir. rwi tack_on_inc H3. nin H3. 
  assert (sub (range (graph f))(target f)). fprops.
  set (H4 _ H3). fprops. rw H3. fprops. rww tack_on_domain.  ue.
Qed.

Hint Resolve tack_on_function: fprops.


Lemma tack_on_W_in: forall  f x y u,
  is_function f -> ~(inc x (source f)) -> inc u (source f) ->
  W u (tack_on_f f x y) = W u f.
Proof. ir. app W_pr. fprops. uf tack_on_f. aw.
  left. graph_tac. 
Qed.

Lemma tack_on_W_out: forall  f x y,
  is_function f -> ~(inc x (source f)) -> 
  W x (tack_on_f f x y) = y.
Proof. ir. app W_pr. fprops. uf tack_on_f. aw. au.
Qed.

Lemma tack_on_surjective: forall  f x y,
  surjective f -> ~(inc x (source f)) -> surjective (tack_on_f f x y).
Proof. ir. cp (surj_is_function H).  app surjective_pr6. fprops.  
  ir. ufi tack_on_f H2. awi H2. 
  assert  (source (tack_on_f f x y) = tack_on (source f) x). uf tack_on_f. aw.
  rw H3. nin H2. nin (surjective_pr2 H H2).  exists x0. eee. 
  rww tack_on_W_in. exists x. split. fprops.  sy. rww tack_on_W_out.
Qed.

Lemma tack_on_f_injective: forall x f g a b,
  is_function f -> is_function g -> target f = target g ->
  source f = source g -> ~ (inc x (source f)) ->
  (tack_on_f f x a = tack_on_f g x b) -> f = g.
Proof. ir. app function_exten. ir. wr (tack_on_W_in a H H3 H5).
  rw H4. rwi H2 H3. rwi H2 H5. wr (tack_on_W_in b H0 H3 H5). tv.
Qed.


(** Canonical injection of a set into another *) 
Definition canonical_injection a b :=
  corresp a b (identity_g a).

Lemma ci_function: forall a b, sub a b ->
  is_function  (canonical_injection a b).
Proof. ir. uf canonical_injection.  app is_function_pr. app identity_fgraph.
  rww identity_range. rww identity_domain.  
Qed.
  
Hint Resolve ci_function : fprops.
Lemma ci_W: forall a b x,
  sub a b -> inc x a -> W x (canonical_injection a b) = x.
Proof. ir. uf W. uf canonical_injection. aw. app identity_ev.
Qed.

Lemma ci_injective: forall a b,
  sub a b -> injective (canonical_injection a b).
Proof. ir. red. ee. fprops.
  assert (Ht:source  (canonical_injection a b) = a). 
  uf canonical_injection. aw. rw Ht. ir. rwii ci_W H2. rwii ci_W H2.  
Qed.

Lemma ci_range: forall a b, sub a b ->
  range (graph (canonical_injection a b)) = a.
Proof. ir. uf canonical_injection. aw. rww identity_range. 
Qed.

Lemma inclusionC_injective: forall a b (H: sub a b),
  injectiveC (inclusionC H).
Proof. red. uf inclusionC. ir.  app R_inj.
  assert (Ro (Bo (H (Ro u) (R_inc u))) = Ro u). app B_eq.
  assert (Ro (Bo (H (Ro v) (R_inc v))) = Ro v). app B_eq.
  wr H1; wr H2. rw H0. tv.
Qed.

(** Diagonal application *) 

Definition diagonal_application a :=
  BL (fun x=> J x x) a (product a a).

Lemma diag_app_W:forall a x, 
  inc x a -> W x (diagonal_application a) = J x x.
Proof. ir. uf diagonal_application. aw. red. ir. fprops. 
Qed.

Lemma injective_diag_app: forall a, 
  injective (diagonal_application a).
Proof. ir. uf diagonal_application. app bl_injective. red. ir. fprops. ir.
  inter2tac.
Qed.

Lemma diag_app_function: forall a, 
  is_function (diagonal_application a).
Proof. ir. nin (injective_diag_app a). am.
Qed.

Lemma diag_app_range: forall a, 
  range (graph (diagonal_application a)) = diagonal a.
Proof. ir.  rw diagonal_is_identity. uf diagonal_application. 
  uf BL. aw. set_extens. rwi L_range_rw H. nin H. nin H. wr H0. aw. eee.
  rw L_range_rw. rwi inc_diagonal_rw H. ee. ex_tac. app pair_extensionality.
  fprops. aw. aw.
Qed.

(** Injectivity and surjectivity of P and Q *)

Lemma second_proj_surjective: forall g,
  surjective (second_proj g).
Proof. ir. app surjective_pr5. app second_proj_function. uf second_proj. aw. 
  ir. ufi range H. awi H.  nin H; nin H. uf BL. uf L. aw. 
  ex_tac. red. aw. ex_tac. ue.
Qed.
  
Lemma first_proj_surjective: forall g ,
  surjective (first_proj g).
Proof. ir. app surjective_pr5. app first_proj_function. uf first_proj. aw. 
  ir. ufi domain H. awi H. nin H;nin H. uf BL. uf L.  aw. 
  ex_tac. red. aw. ex_tac. ue.
Qed.

Lemma first_proj_injective: forall g,
  is_graph g -> (injective (first_proj g) = functional_graph g).
Proof. ir. assert (is_function  (first_proj g)). app first_proj_function.
  uf injective. assert (Ht: source (first_proj g) = g). uf first_proj. aw. 
  rw Ht. app iff_eq. ir. red.  ir. red in  H2.  red in H3. nin H1.
  assert (J x y = J x y'). app H4. 
  rww first_proj_W. rww first_proj_W. aw. inter2tac.
  ir. ee. am. ir. 
  rwii first_proj_W H4. rwii first_proj_W H4. red in H1. ufi related H1.
  cp (H _ H2).  cp (H _ H3). app pair_extensionality.
  rwi is_pair_rw  H5. rwi is_pair_rw H6. rwi H5 H2; rwi H6 H3. wri H4 H3.
  app (H1 _ _ _ H2 H3).
Qed.

(** The function that maps [J x y] to [J y x] *) 
Definition inv_graph_canon g :=
   BL (fun x=> J (Q x) (P x)) g (inverse_graph g).

Lemma inv_graph_canon_W: forall g x, 
  is_graph g ->inc x g -> W x (inv_graph_canon g) = J (Q x) (P x).
Proof. ir. uf inv_graph_canon. aw. red. ir. aw. app H. 
Qed. 

Lemma inv_graph_canon_function:  forall g, 
  is_graph g -> is_function (inv_graph_canon g).
Proof. ir. uf inv_graph_canon. app bl_function. red. ir. aw. app H.
Qed. 

Lemma inv_graph_canon_bijective:  forall g, 
  is_graph g -> bijective (inv_graph_canon g).
Proof. ir.  uf inv_graph_canon. app bl_bijective. red; ir.
  aw. app H. ir.  app pair_extensionality.  app H. app H. inter2tac. inter2tac.
  ir. rwii inverse_graph_rw H0. ee. ex_tac.  aw. 
Qed.

(** Example 5 page 17 of Bourbaki (page 85 in the English edition) *)
Lemma bourbaki_ex5_17: forall a b, 
  bijective (BL (fun x=> J x b) a (product a (singleton b))).
Proof. ir. app bl_bijective. red. ir.
  aw. ee. fprops. am. tv. 
  ir. inter2tac.
  ir.  awi H. ee. exists (P y). split. am. wr H1. app pair_recov.
Qed.

Lemma equipotent_prod_singleton:
  forall a b, equipotent a (product a (singleton b)).
Proof. ir. exists (BL (fun x=> J x b) a (product a (singleton b))).
  ee. app (bourbaki_ex5_17 a b). aw. aw.
Qed.

Lemma restriction1_pr: forall f,
  is_function f -> restriction2 f (source f)  (image_by_fun f (source f)) =
  restriction1 f (source f).
Proof. uf restriction2. uf restriction1. ir.
  assert (restr (graph f) (source f) = graph f). ap extensionality.
  ap restr_sub. red. ir. rw restr_inc_rw. split. am. graph_tac.
  rw H0. nin H. red in H. nin H. red in H2. rwi intersection2_sub H2. rww H2.
Qed.

(** Proposition 7 summarizes next two theorems. Let f be a function; then 
 f is a bijection if and only if  its inverse is a function *)
Theorem bijective_inv_function: forall f,
  bijective f -> is_function (inverse_fun f).
Proof. ir. red in H; ee.  assert (is_graph (graph f)).  nin H; fprops.
  uf inverse_fun. app is_function_pr.
  red. split. fprops. ir. rwii inverse_graph_rw H2. rwii inverse_graph_rw H3.
  ee. wri H4 H5. cp (injective_pr3 H H6 H5). app pair_extensionality.
  nin H. rww range_inverse. aw. fprops. 
  rww domain_inverse. sy; app surjective_pr3.
Qed.

Theorem inv_function_bijective: forall f,
  is_function f -> is_function (inverse_fun f) -> bijective f.
Proof. ir. red in H0. ee. 
  assert (Ha: inverse_graph (graph f) = graph (inverse_fun f)).
  uf inverse_fun. aw.
  split. app injective_pr_bis. uf related. ir. 
  wri inverse_graph_pair H3. wri inverse_graph_pair H4. wri Ha H1.
  app (fgraph_pr H1 H3 H4).
  app surjective_pr4. wr domain_inverse. rw Ha. wr H2. 
  uf inverse_fun. aw. fprops.
Qed.

(** We define here an inverse of [(f:a->b)] *) 
Lemma bijective_inv_aux: forall (a b:Set) (f:a->b),
  bijectiveC f -> is_function (inverse_fun (acreate f)).
Proof. ir. app bijective_inv_function. app acreate_bijective.
Qed.
Lemma bijective_source_aux: forall (a b:Set) (f:a->b),
  source (inverse_fun (acreate f)) = b.
Proof. ir.  uf inverse_fun. uf acreate. aw. 
Qed.
Lemma bijective_target_aux: forall (a b:Set) (f:a->b),
  target (inverse_fun (acreate f)) = a.
Proof. ir. uf inverse_fun. uf acreate. aw. 
Qed.

Definition inverseC (a b:Set) (f:a->b)(H:bijectiveC f): b->a :=
  bcreate(bijective_inv_aux H)(bijective_source_aux f)
  (bijective_target_aux f).

Lemma inverseC_pra: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:a),
  (inverseC H) (f x) = x.
Proof. ir. app R_inj. uf inverseC. rw prop_bcreate2.
  wr (acreate_W f). set (g:= acreate f).  set (y:= Ro x). 
  assert (inc y a).  uf y. app R_inc. 
  assert (bijective g). uf g. app acreate_bijective.
  assert (is_function g). fct_tac.
  app W_pr. app bijective_inv_function. uf inverse_fun. aw.
  assert (inc (J (W y g) y) (inverse_graph (graph g))). aw. graph_tac.
  uf g. aw. awi H3. am.
Qed.

Lemma inverseC_prb: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:b),
  f ((inverseC H) x) = x.
Proof. ir. assert (bijectiveC f). am. nin H0. red in H1.
  nin (H1 x). wr H2. rww inverseC_pra.
Qed.

Lemma inverseC_prc: forall (a b:Set) (f:a-> b) (H:bijectiveC f),
  inverse_fun(acreate f) = acreate(inverseC H).
Proof. ir. cp (acreate_bijective H).
  app function_exten.  app bijective_inv_aux. fprops.
  uf inverse_fun. uf acreate. aw. uf inverse_fun. uf acreate. aw.
  ir. uf inverseC. rww bcreate_inv2. 
Qed.

Lemma bij_left_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
  composeC (inverseC H) f = identityC a. 
Proof. ir. app arrow_extensionality. ir.
  uf composeC. rww inverseC_pra. 
Qed.

Lemma bij_right_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
  composeC f (inverseC H) = identityC b. 
Proof. ir. app arrow_extensionality. ir.
  uf composeC. rww inverseC_prb.
Qed.

Lemma bijective_double_inverseC: forall (a b:Set) (f:a->b) g g',
  composeC  g f = identityC a -> composeC  f g' = identityC b ->
  bijectiveC f.
Proof. ir.  red. ee. red. ir. transitivity (identityC a u). tv. 
  wr H. transitivity (identityC a v). wr H. uf composeC. rww H1. tv.
  red. ir. exists (g' u). transitivity (identityC b u). wrr H0. tv.
Qed.

Lemma bijective_double_inverseC1: forall (a b:Set) (f:a->b) g g'
  (Ha: composeC  g f = identityC a)(Hb: composeC  f g' = identityC b),
  g = inverseC(bijective_double_inverseC Ha Hb)
  & g' = inverseC(bijective_double_inverseC Ha Hb).
Proof. ir. assert (g' = g). app arrow_extensionality.
  ir. transitivity  (identityC a (g' a0)). tv. wr Ha. uf composeC.
  assert (f (g' a0) = a0). transitivity (identityC b a0). tv. wrr Hb. tv. rww H.
  assert (g = inverseC (bijective_double_inverseC Ha Hb)).
  app arrow_extensionality. ir. 
  assert (f (g' a0) = a0). transitivity (identityC b a0). wrr Hb. tv.
  wr H0. rw inverseC_pra. rw H0. sy. rww H.  wr H0.  intuition.
Qed.

Lemma bijective_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
  bijectiveC (inverseC H). 
Proof. ir. red. ee. red. ir. wr (inverseC_prb H u). rw H0. 
  rw (inverseC_prb H v). tv. red. ir. exists (f u). rww inverseC_pra. 
Qed.

Lemma inverse_fun_involutiveC:forall (a b:Set) (f:a->b) (H: bijectiveC f),
  f = inverseC(bijective_inverseC H).
Proof. ir. app arrow_extensionality. ir. 
  set (g:= inverseC H).  set (Ha:= (bijective_inverseC H)).
  assert (bijectiveC g). uf g. am. red in H0. ee.  red in H0. app H0.
  uf g. rw inverseC_pra. rw inverseC_prb. tv.
Qed.

(** Properties of the inverse of a bijection*)

Lemma inverse_bij_is_bij1:forall f,
  bijective f ->  bijective (inverse_fun f).
Proof. ir. set (refl_equal (source f)). set (refl_equal (target f)).
  assert(is_function f).  fct_tac.
  set (bcreate_bijective H0 e e0  H). set (inverseC_prc b).
  rwi (bcreate_inv2  H0 e e0) e1. rw e1. app acreate_bijective.
  app bijective_inverseC.
Qed.

Lemma inverse_bij_is_bij:forall f,
  bijective f ->  bijective (inverse_fun f).
Proof. ir. assert (is_function f). fct_tac.
  set (bijective_inv_function H). app inv_function_bijective.
  rww inverse_fun_involutive.  fct_tac. 
Qed.

Lemma composable_f_inv:forall f,
  bijective f ->  composable f (inverse_fun f).
Proof. ir. red. 
  assert (is_function (inverse_fun f)). app bijective_inv_function.
  eee. fct_tac.  uf inverse_fun. aw.
Qed.

Lemma composable_inv_f: forall f,
  bijective f ->  composable (inverse_fun f) f.
Proof. ir. red. 
  assert (is_function (inverse_fun f)). app bijective_inv_function.
  eee. fct_tac. uf inverse_fun. aw.
Qed.

Lemma bij_right_inverse:forall f,
  bijective f ->  compose f (inverse_fun f) = identity (target f).
Proof. ir. set (refl_equal (source f)). set (refl_equal (target f)).
  wr (identity_prop (target f)).
  set (bij_is_function H).
  wr (bcreate_inv2 i e e0). rw (inverseC_prc (bcreate_bijective i e e0 H)).
  rw compose_acreate. rww bij_right_inverseC. aw. 
Qed.

Lemma bij_left_inverse:forall f,
  bijective f ->  compose (inverse_fun f) f = identity (source f).
Proof. ir. set (refl_equal (source f)). set (refl_equal (target f)).
  set (bij_is_function H).  wr (identity_prop (source f)).
  wr (bcreate_inv2 i e e0).  rw (inverseC_prc (bcreate_bijective i e e0 H)).
  rw compose_acreate.  rww bij_left_inverseC. aw.
Qed.

Lemma W_inverse: forall f x y,
  bijective f -> inc x (target f) ->
  (y = W x (inverse_fun f)) -> (x = W y f).
Proof. ir. rw H1. transitivity (W x (identity (target f))). srw.
  wr (bij_right_inverse H). aw. app composable_f_inv.  
Qed.

Lemma W_inverse2: forall f x y,
  bijective f -> inc y (source f) ->
  (x = W y f) -> (y = W x (inverse_fun f)).
Proof. ir. transitivity ( W y (identity (source f))). srw.
  wr (bij_left_inverse H). aw. wrr H1. app composable_inv_f.
Qed.


Lemma W_inverse3: forall f x,
  bijective f -> inc x (target f) -> inc (W x (inverse_fun f)) (source f).
Proof. ir.  assert (inc (W x (inverse_fun f)) (target (inverse_fun f))). 
  app inc_W_target. cp (inverse_bij_is_bij1 H). fct_tac. uf inverse_fun. aw.
  ufi inverse_fun H1. awi H1. am.
Qed.


(** Properties of direct and inverse images *)
Lemma sub_inv_im_source:forall f y,
  is_function f -> sub y (target f) -> 
  sub (inv_image_by_graph (graph f) y) (source f).
Proof. ir.   red. ir. awi H1. nin H1. ee. graph_tac.
Qed.

Lemma direct_inv_im: forall f y,
  is_function f ->  sub y (target f) -> 
  sub (image_by_fun f (image_by_fun (inverse_fun f) y)) y.
Proof. ir. red. ir. wri inv_image_by_fun_pr H1. ufi inv_image_by_fun H1.
  rwi W_image H1. nin H1. nin H1. simpl in H1. awi H1. nin H1. 
  nin H1. red in H3. awi H3. wr H2. rww (W_pr H H3). am. 
  app sub_inv_im_source.
Qed.

Lemma direct_inv_im_surjective: forall f y,
  surjective  f -> sub y (target f) -> 
  (image_by_fun f (image_by_fun (inverse_fun f) y)) = y. 
Proof. ir. assert (Ha: is_function f). red in H; eee.
  app extensionality. app direct_inv_im. 
  red. ir. wr inv_image_by_fun_pr. uf inv_image_by_fun.
  rww W_image. nin (surjective_pr2 H (H0 _ H1)).
  exists x0. ee. aw.  ex_tac. wr H3. graph_tac. am.
  app sub_inv_im_source.
Qed.

Lemma inverse_direct_image:forall f x,
  is_function f -> sub x (source f) ->
  sub x (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof. ir. red. ir. 
  assert (inc (J x0 (W x0 f))(graph f)). graph_tac. 
  uf image_by_fun. aw. exists (W x0 f). split.  aw. ex_tac. uf inverse_fun. aw. 
Qed.

Lemma inverse_direct_image_inj:forall f x,
  injective f -> sub x (source f) ->
   x = (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof. ir. app extensionality. app inverse_direct_image. fct_tac.
  red. ir. nin H. wri inv_image_by_fun_pr H1. ufi inv_image_by_fun H1. 
  awi H1. nin H1. ee. awii H1.  nin H1. nin H1. red in H3.
  wri (W_pr H H3) H4.
  wrr (H2 _ _  (H0 _ H1) (inc_pr1graph_source H H3) H4).
Qed.


(** ** EII-3-8 Retractions and sections *)

(** Definition of left and right inverse *)

Definition is_left_inverse r f :=
  composable r f & compose r f = identity (source f).

Definition is_right_inverse s f :=
  composable f s & compose f s = identity (target f).

(** Typechecking says that [r:b->a] and [s:b->a] *)
Definition is_left_inverseC (a b:Set) r (f:a->b) := composeC r f = identityC a.
Definition is_right_inverseC (a b:Set) s (f:a->b):= composeC f s = identityC b.

Lemma target_left_inverse: forall r f,
  is_left_inverse r f ->  target r = source f.
Proof. ir. nin H. cp (f_equal target H0).  ufi compose H1; ufi identity H1.
  awii H1.
Qed.

Lemma source_right_inverse: forall s f,
  is_right_inverse s f ->  source s = target f.
Proof. ir. nin H. cp (f_equal source H0). 
  ufi compose H1; ufi identity H1.  awii H1.
Qed.


Lemma W_right_inverse: forall s f x, 
  is_right_inverse s f -> inc x (target f) -> W (W x s) f = x.
Proof. ir. cp (source_right_inverse H).
  red in H. ee. wrr compose_W. rw H2. srw. rww H1.
Qed.

Lemma W_left_inverse: forall r f x, 
  is_left_inverse r f -> inc x (source f) -> W (W x f) r = x.
Proof. ir. cp (target_left_inverse H).
  red in H. ee. wrr compose_W. rw H2. srw. 
Qed.

Lemma w_right_inverse: forall (a b:Set)  s (f:a->b) (x:b), 
  is_right_inverseC s f ->  f (s x) = x.
Proof. ir. red in H. transitivity (identityC b x). wrr H. tv.
Qed.

Lemma w_left_inverse: forall (a b:Set) r (f:a->b) (x:a), 
  is_left_inverseC r f -> r (f x) = x.
Proof. ir. red in H.  transitivity (identityC a x). wrr H. tv.
Qed.


(** Proposition 8 concerns the next 4 theorems; it is the link between injectivity, surjectivity and existence of left and right inverse *)

Lemma inj_if_exists_left_invC: forall (a b:Set) (f:a-> b),
  (exists r, is_left_inverseC r f) -> injectiveC f.
Proof. ir. nin H. red. ee. ir. transitivity (x (f u)). 
  rww (w_left_inverse u H). rw H0. rww (w_left_inverse v H).
Qed.

Lemma surj_if_exists_right_invC: forall (a b:Set) (f:a->b),
  (exists s, is_right_inverseC s f) -> surjectiveC f.
Proof. ir. nin H. red. ir. exists (x u). rww (w_right_inverse u H).
Qed.

Theorem inj_if_exists_left_inv: forall f,
  (exists r, is_left_inverse r f) -> injective f.
Proof. ir. nin H. red. ee. nin H. red in H. ee. am. 
  ir. wr (W_left_inverse H H0).  wr (W_left_inverse H H1). rww H2.
Qed.

Theorem surj_if_exists_right_inv: forall f,
  (exists s, is_right_inverse s f) -> surjective f.
Proof. ir. nin H. app surjective_pr6. nin H. red in H. ee. am.
  ir. exists (W y x). rww W_right_inverse. wri (source_right_inverse H) H0.
  nin H. red in H. ee.  rw H3. fprops. tv.
Qed.

(** Left inverse for an injective function [(f: a->b)]*)
Definition left_inverseC (a b:Set) (f: a->b)(H:nonemptyT a) 
  (v:b) := (chooseT (fun u:a => (~ (exists x:a, f x = v)) \/ (f u = v)) H).

Lemma left_inverseC_pr:forall (a b:Set) (f: a->b) (H:nonemptyT a) (u:a),
  f(left_inverseC f H (f u)) = f u.
Proof. ir. uf left_inverseC.
  set (p:=(fun u0 : a => (~ (exists x : a, f x = f u)) \/ f u0 = f u)).
  set (y := chooseT p H). assert (p y). uf y. app chooseT_pr.
  uf p. exists u. au. nin H0. nin H0. exists u. tv. am.
Qed.
 
Lemma left_inverse_comp_id: forall (a b:Set) (f:a->b)  (H:nonemptyT a),
  injectiveC f ->  composeC (left_inverseC f H) f = identityC a.
Proof. ir. app arrow_extensionality. ir. uf composeC. uf identityC.
  app H0. app left_inverseC_pr.
Qed.

Lemma exists_left_inv_from_injC: forall (a b:Set) (f:a->b), nonemptyT a ->
  injectiveC f -> exists r, is_left_inverseC r f.
Proof. ir.  exists (left_inverseC f H). red. app left_inverse_comp_id.
Qed.

(** Right inverse for a surjective function [(f: a->b)]*)

Definition right_inverseC (a b:Set) (f: a->b)  (H:surjectiveC f): b ->a.
  ir. assert  (nonemptyT a). nin (H H0). app nonemptyT_intro.
  exact (chooseT (fun k:a => f k = H0) H1).
Defined.

Lemma right_inverse_pr:  forall (a b:Set) (f: a->b) (H:surjectiveC f) (x:b),
  f(right_inverseC H x) = x.
Proof. ir. uf right_inverseC. app chooseT_pr. 
Qed.

Lemma right_inverse_comp_id: forall (a b:Set) (f:a-> b) (H:surjectiveC f), 
  composeC f (right_inverseC H)  = identityC b.
Proof. ir. app arrow_extensionality. ir. uf composeC; uf identityC.
  app right_inverse_pr.
Qed.

Lemma exists_right_inv_from_surjC: forall (a b:Set)(f:a-> b) (H:surjectiveC f),
  exists s, is_right_inverseC s f.
Proof. ir. exists (right_inverseC H). red. app right_inverse_comp_id.
Qed.

(** Existence of left and right inverse for Bourbaki functions *)

Theorem exists_left_inv_from_inj: forall f,
  injective f ->nonempty (source f) -> exists r, is_left_inverse r f.
Proof. ir. set (inj_is_function H). set (bcreate1_injective (H:=i) H).
  nin H0. nin (exists_left_inv_from_injC (inc_nonempty H0) i0).
  exists (acreate x). red. ee. red. eee. aw.
  red in H1. set (compose_acreate x (bcreate1 i)). 
  rwi bcreate_inv1 e. rw e. rww H1.
Qed.

Theorem exists_right_inv_from_surj: forall f,
  surjective  f -> exists s, is_right_inverse s f.
Proof. ir. set (surj_is_function H).  
  set (bcreate1_surjective i H).
  nin (exists_right_inv_from_surjC s). 
  exists (acreate x). red. ee. red. eee. aw. 
  set (compose_acreate (bcreate1 i) x). 
  rwi bcreate_inv1 e. rw e. rww H0.
Qed.

(** If compositions in both order are the identity, then the functions are bijections *)

Lemma bijective_from_compose: forall g f,
  composable g f -> composable f g -> compose g f = identity (source f)
  -> compose f g = identity (source g) 
  -> (bijective f & bijective g & g = inverse_fun f).
Proof. ir. assert (is_function f). fct_tac. 
  assert (is_function g). fct_tac. 
  assert (injective f).  app inj_if_exists_left_inv. exists g. red. eee.
  assert (injective g).  app inj_if_exists_left_inv. exists f. red. eee.
  assert (source f = target g). red in H0. ee. am. rwi H7 H1.
  assert (source g = target f). red in H. ee. am. rwi H8 H2.
  assert (bijective f).
  red. ee. am. app surj_if_exists_right_inv. exists g. red. au. 
  ee. am.  split. am. app surj_if_exists_right_inv. exists f. red. au.
  sy. set (bijective_inv_function H9). app function_exten. sy; aw. aw.
  ir. app W_pr. uf inverse_fun. aw. awi H10. set (identity_W H10).  wri H2 e. 
  wri H8 H10. awi e.  set (y:= W x g). wr e. uf y. graph_tac. 
  rw H7. fprops. am. am.
Qed.

(** More links between left inverse and right inverse *)
Lemma right_inverse_from_leftC: forall (a b:Set) (r:b->a)(f:a->b),
  is_left_inverseC r f -> is_right_inverseC f r.
Proof. ir. tv.
Qed.

Lemma left_inverse_from_rightC: forall (a b:Set) (s:b->a)(f:a->b),
  is_right_inverseC s f -> is_left_inverseC f s.
Proof. ir. tv.  Qed.

Lemma left_inverse_surjectiveC: forall (a b:Set) (r:b->a)(f:a->b),
  is_left_inverseC r f -> surjectiveC r.
Proof. ir. ap surj_if_exists_right_invC. red in H. exists f. am.
Qed.

Lemma right_inverse_injectiveC: forall (a b:Set) (s:b->a)(f:a->b),
  is_right_inverseC s f -> injectiveC s.
Proof. ir. ap inj_if_exists_left_invC. red in H. exists f. am.
Qed.

Lemma section_uniqueC: forall (a b:Set) (f:a->b)(s:b->a)(s':b->a),
  is_right_inverseC s f -> is_right_inverseC s' f ->
  (forall x:a, (exists u:b, x = s u) = (exists u':b, x = s' u')) ->
  s = s'.
Proof. ir. app arrow_extensionality. ir. 
  cp (H1 (s a0)). assert (exists u' : b, s a0 = s' u'). wr H2. exists a0. tv.
  nin H3. rw H3. assert (f (s a0) = f (s' x)). rww H3. 
  rwi (w_right_inverse a0 H) H4. rwi (w_right_inverse x H0) H4. rww H4.
Qed.

Lemma right_inverse_from_left: forall r f,
  is_left_inverse r f -> is_right_inverse f r.
Proof. ir. assert (Ha:=target_left_inverse H). 
  red in H. nin H. wri Ha H0. red. auto.
Qed.

Lemma left_inverse_from_right: forall s f,
  is_right_inverse s f -> is_left_inverse f s.
Proof. ir. assert (H0:=source_right_inverse H). red in H.  wri H0 H. 
  ee. red. auto.
Qed.

Lemma left_inverse_surjective: forall f r,
  is_left_inverse r f -> surjective r.
Proof. ir. ap surj_if_exists_right_inv. exists f.
  app right_inverse_from_left.
Qed.

Lemma right_inverse_injective: forall f s,
  is_right_inverse s f -> injective s.
Proof. ir. ap inj_if_exists_left_inv. exists f.
  app left_inverse_from_right.
Qed.

Lemma section_unique: forall f s s',
  is_right_inverse s f -> is_right_inverse s' f ->
  range (graph s) = range (graph s') -> s = s'.
Proof. ir. cp (source_right_inverse H). cp (source_right_inverse H0).
  cp H. cp H0. red in H. red in H0. ee. red in H; red in H0; ee.
  app function_exten. rww H3. wrr H11. 
  ir.
  assert (inc (W x s) (range (graph s))). rw range_inc_rw. exists x. au.
  am. rwi H2 H12. cp (W_right_inverse H4 H12).
  rwi H1 H13.  rwi range_inc_rw H13. nin H13. ee.
  rwi H3 H13. cp (W_right_inverse H5 H13).
  rw H15. wri H15 H16. rwi H14 H16. rww H16. am.
Qed.

(** Theorem one is next 14 lemmas. It studies left and right invertibility 
of one of f g and the composition of f and g, given properties of the other objects. *)


Lemma composeC_inj: forall (a b c:Set) (f:a->b)(f':b->c),
  injectiveC f-> injectiveC f' -> injectiveC (composeC f' f).
Proof. ir. red. ir. app H. app H0. 
Qed.

Lemma composeC_surj: forall (a b c:Set) (f:a->b)(f':b->c),
  surjectiveC f-> surjectiveC f' -> surjectiveC (composeC f' f).
Proof. ir. red. ir. nin (H0 u). nin (H x). exists x0. wr H1. wrr H2.
Qed.

Lemma composeC_bij: forall (a b c:Set) (f:a->b)(f':b->c),
  bijectiveC f-> bijectiveC f' -> bijectiveC (composeC f' f).
Proof. ir. red. red in H; red in H0. ee. app composeC_inj. app composeC_surj.
Qed.

Lemma left_inverse_composeC: forall (a b c:Set) 
  (f:a->b) (f':b->c)(r:b->a)(r':c->b),
  is_left_inverseC r' f' -> is_left_inverseC r f ->
  is_left_inverseC (composeC r r') (composeC f' f).
Proof. ir. red. uf composeC. app arrow_extensionality. uf identityC. ir.
  rw (w_left_inverse (f a0) H).  rw (w_left_inverse a0 H0). tv.
Qed.

Lemma right_inverse_composeC:forall (a b c:Set) 
  (f:a->b) (f':b->c)(s:b->a)(s':c->b),
  is_right_inverseC s' f' -> is_right_inverseC s f ->
  is_right_inverseC (composeC s s') (composeC f' f).
Proof. ir. red. uf composeC. app arrow_extensionality. ir. uf identityC.
  rw (w_right_inverse (s' a0) H0).  rw (w_right_inverse a0 H).  tv.
Qed.

Lemma inj_right_composeC: forall (a b c:Set) (f:a->b) (f':b->c),
  injectiveC (composeC f' f) -> injectiveC f.
Proof. ir. red. ir. app H. simpl. uf composeC. ue.  
Qed.

Lemma surj_left_composeC: forall (a b c:Set) (f:a->b) (f':b->c),
  surjectiveC (composeC f' f) -> surjectiveC f'.
Proof. ir. red. ir. nin (H u).  exists (f x). am.
Qed.

Lemma surj_left_compose2C: forall (a b c:Set) (f:a->b) (f':b->c),
  surjectiveC (composeC f' f) -> injectiveC f' -> surjectiveC f.
Proof. ir. red. ir. nin (H (f' u)). exists x. app H0.
Qed.

Lemma inj_left_compose2C: forall (a b c:Set) (f:a->b) (f':b->c),
  injectiveC (composeC f' f) -> surjectiveC f -> injectiveC f'.
Proof. ir.  red. ir. nin (H0 u). nin (H0 v). wri H2 H1. wri H3 H1.
  assert (x = x0). app H.  wr H2; wr H3; rww H4.
Qed.

Lemma left_inv_compose_rfC: forall (a b c:Set) (f:a->b) (f':b->c)(r'': c->a),
  is_left_inverseC r'' (composeC f' f) -> 
  is_left_inverseC (composeC r'' f') f.
Proof. ir. red. app arrow_extensionality. ir. ap (w_left_inverse a0 H).  
Qed.

Lemma right_inv_compose_rfC :  forall (a b c:Set) (f:a->b) (f':b->c)(s'': c->a),
  is_right_inverseC s'' (composeC f' f) -> 
  is_right_inverseC (composeC f s'') f'.
Proof. ir. red. app arrow_extensionality. ir. ap (w_right_inverse a0 H). 
Qed.

Lemma left_inv_compose_rf2C: forall (a b c:Set) (f:a->b) (f':b->c)(r'': c->a),
  is_left_inverseC r'' (composeC f' f) -> surjectiveC f ->
  is_left_inverseC (composeC f r'') f'.
Proof. ir. red. assert (bijectiveC f). red. 
  assert (injectiveC (composeC f' f)). ap inj_if_exists_left_invC. 
  exists r''. am. ee. ap (inj_right_composeC H1). am.
  set (invf:= (inverseC H1)).
  assert (f' = composeC f' (composeC f invf)).  uf invf.
  rw (bij_right_inverseC H1). rww compose_id_rightC. 
  app arrow_extensionality. uf identityC. ir. uf composeC.
  assert (f' a0 = composeC f' (composeC f invf) a0). wr H2.  tv.
  ufi composeC H3. rw H3.  ufi composeC H. rw (w_left_inverse (invf a0) H). 
  uf invf. app inverseC_prb.
Qed.

Lemma right_inv_compose_rf2C : forall (a b c:Set) (f:a->b) (f':b->c)(s'': c->a),
  is_right_inverseC s'' (composeC f' f) -> injectiveC f'->
  is_right_inverseC (composeC s'' f') f.
Proof. ir. assert (bijectiveC f'). red. ee. am.
  assert(surjectiveC (composeC f' f)). ap surj_if_exists_right_invC. 
  exists s''. am.  app (surj_left_composeC H1).
  set (invf:= inverseC H1). 
  assert (f = composeC (composeC invf f') f).  uf invf.
  rw (bij_left_inverseC H1). rww compose_id_leftC. 
  red. app arrow_extensionality. ir. uf identityC.  rw H2.
  uf composeC. ufi composeC H. rw (w_right_inverse (f' a0) H).
  uf invf. app inverseC_pra.
Qed. 

Theorem compose_injective: forall f f',
  injective f-> injective f' -> composable f' f ->
  injective (compose f' f).
Proof. ir. red. ee. fct_tac.  aw. ir. awi H4; try am.
  red in H0; red in H; red in H1; ee.
  app H8. app H7. ue. ue. 
Qed.

Theorem compose_surjective: forall f f',
  surjective f-> surjective f' -> composable f' f ->
  surjective (compose f' f).
Proof. ir. app surjective_pr6. fct_tac. aw. ir. 
  nin (surjective_pr2 H0 H2). ee. assert (inc x (target f)). red in H1; ee. ue. 
  nin (surjective_pr2 H H5). ee. ex_tac. aw. ue.
Qed.

Lemma compose_bijective: forall f f',
  bijective f-> bijective f' -> composable f' f ->
  bijective (compose f' f).
Proof. ir. red. red in H; red in H0. ee. 
  app compose_injective. app compose_surjective.
Qed.

Lemma bij_right_compose: forall f f',
  composable f' f-> bijective (compose f' f) -> bijective f' ->bijective f.
Proof. ir. set (g:= inverse_fun f').  assert (bijective g). uf g.
  app inverse_bij_is_bij. 
  assert (bijective (compose g (compose f' f))). app compose_bijective.
  uf g; red; eee; aw; fct_tac.  
  wri compose_assoc H3. ufi g H3. rwi bij_left_inverse H3. red in H. ee. 
  rwi H5 H3. rwi compose_identity_left H3. am. fct_tac. am. 
  uf g. red;eee; aw;fct_tac. am.
Qed.

Lemma bij_left_compose: forall f f',
  composable f' f-> bijective (compose f' f) -> bijective f ->bijective f'.
Proof. ir. set (g:= inverse_fun f). assert (bijective g). uf g.
  app inverse_bij_is_bij. 
  assert (bijective (compose  (compose f' f) g)). app compose_bijective.
  red. aw. eee; try fct_tac. uf g; aw.
  rwi compose_assoc H3. ufi g H3. rwi bij_right_inverse H3. red in H. ee. 
  wri H5 H3. rwi compose_identity_right H3. am.  fct_tac. am. am. 
  red. eee;  try fct_tac. uf g; aw.
Qed.

Lemma left_inverse_composable: forall f f' r r',  composable f' f ->
  is_left_inverse r' f' -> is_left_inverse r f -> composable r r'.
Proof. ir. cp (target_left_inverse H0). red in H0; red in  H1. ee.
  red in H0; red in H1. ee. red. eee. red in H. ee. ue.
Qed.

Lemma right_inverse_composable: forall f f' s s',  composable f' f ->
  is_right_inverse s' f' -> is_right_inverse s f -> composable s s'.
Proof. ir. cp (source_right_inverse H1). red in H0; red in  H1. ee.
  red in H0; red in H1. ee. red. eee. red in H. ee. wrr H10.
Qed.

Theorem left_inverse_compose: forall f f' r r', composable f' f ->
  is_left_inverse r' f' -> is_left_inverse r f ->
  is_left_inverse (compose r r') (compose f' f).
Proof. ir. cp (left_inverse_composable H H0 H1).
  cp (target_left_inverse H0).
  red in H0; red in H1; ee.  red. ee. red. red in H0; ee; aw; fct_tac. 
  aw. wrr compose_assoc. rw (@compose_assoc r r' f'). rw H5.
  assert (source f' = source r). wr H3. red in  H2; ee; sy;am. rw H6.
  rww compose_id_right.  fct_tac. am.  am. red. red in H0; ee; aw; fct_tac.  
Qed.

Theorem right_inverse_compose: forall f f' s s', composable f' f ->
  is_right_inverse s' f' -> is_right_inverse s f ->
  is_right_inverse (compose s s') (compose f' f).
Proof. ir. cp (right_inverse_composable H H0 H1).
  cp (source_right_inverse H1). red in H0; red in  H1; ee.
  red. ee. red. ee.  fct_tac. fct_tac. aw. red in H1; ee; am. 
  rww compose_assoc. wr (@compose_assoc f s s'). rw H4.
  assert (target f = target s'). wr H3. red in H2; eee. rw H6.
  rww compose_id_left. aw. fct_tac. am. am. red in H1. red. eee; aw; fct_tac. 
Qed.

Theorem inj_right_compose: forall f f',
  composable f' f-> injective (compose f' f) -> injective f.
Proof. ir. red. ee. red in H; ee; am. ir. red in H0. ee. awi H4.
  app H4. aw. ue.
Qed.

Theorem surj_left_compose: forall f f',
  composable f' f-> surjective (compose f' f) -> surjective f'.
Proof. ir. app surjective_pr6. red in H;ee;am. ir.
  assert (target f' = target(compose f' f)). aw. 
  rwi H2 H1. nin (surjective_pr2 H0 H1). ee. awi H3.
  awi H4. exists (W x f). ee. red in H;ee. ue.  am. am. am.
Qed.

Theorem surj_left_compose2: forall f f',
  composable f' f-> surjective (compose f' f) -> injective f' -> surjective f.
Proof. ir. app surjective_pr6. red in H;eee. ir. red in H. ee.
  assert (inc (W y f') (target (compose f' f))). aw. nin H1. wri H4 H2. 
  fprops. nin (surjective_pr2 H0 H5). ee. awi H6.
  awi H7. exists x. ee. am. red in H1. ee. rwi H4 H8. app H8.
  fprops. red; au. am. 
Qed.

Theorem inj_left_compose2: forall f f',
  composable f' f-> injective (compose f' f) -> surjective f -> injective f'.
Proof. red. ir. ee. red in H; eee. ir.
  assert (source f' = target f). red in H; eee.
  rwi H5 H2. nin (surjective_pr2 H1 H2). ee.
  rwi H5 H3. nin (surjective_pr2 H1 H3). ee. 
  red in H0; ee.  assert (x0=x1). app H10.
  aw.  aw. aw. rw H7. rww H9. wr H7; wr H9. ue.
Qed.

Theorem left_inv_compose_rf: forall f f' r'',
  composable f' f-> is_left_inverse r'' (compose f' f) -> 
  is_left_inverse (compose r'' f') f.
Proof. ir.  cp (target_left_inverse H0). red in H0. ee. cp H.
  red in H; red in H0. ee.  awi H1. awi H5. awi H2.
  assert(composable r'' f'). red; ee; am.
  red. ee. red. eee. fct_tac.  aw. rww compose_assoc.  
Qed.

Theorem right_inv_compose_rf : forall f f' s'',
  composable f' f-> is_right_inverse s'' (compose f' f) -> 
  is_right_inverse (compose f s'') f'.
Proof. ir. cp (source_right_inverse H0). nin H0. cp H. red in H0; red in H;ee.
  awi H2; awi H1. awi H5.
  assert (composable f s''). red. ee; am. 
  split. red. eee. fct_tac.  aw. wrr compose_assoc. 
Qed.

Theorem left_inv_compose_rf2: forall f f' r'',
  composable f' f-> is_left_inverse r'' (compose f' f) -> surjective f ->
  is_left_inverse (compose f r'') f'.
Proof. ir. assert (bijective f). red. 
  assert (injective (compose f' f)). ap inj_if_exists_left_inv. exists r''. am.
  ee. ap (inj_right_compose H H2). am.
  cp (target_left_inverse H0). red in H0. ee. awi H4. awi H3.
  assert (composable f r''). red. ee. fct_tac. fct_tac. sy; am.
  assert(is_function  (compose f r'')). fct_tac.
  red. ee. red. ee. am. fct_tac. aw. red in H0; ee. awi H8. exact H8. 
  set (invf:= (inverse_fun f)).
  assert(is_function invf). uf invf. app bijective_inv_function.
  assert (source f = target invf). uf invf; aw. 
  assert (f' = compose f' (compose f invf)).  uf invf.
  rw (bij_right_inverse H2).
  red in H; ee. wr H10. rww compose_id_right. wri compose_assoc H9. rw H9.
  rw compose_assoc.  wrr (@compose_assoc r''  (compose f' f) invf). rw H4.
  aw. assert (source f = target invf). uf invf; aw. rw H10. 
  rww compose_id_left.
  uf invf. rww bij_right_inverse. aw. red.  split. fct_tac. split. am. aw. am.
  wr H9. red. red in H0. eee. fct_tac.  aw.  aw. am. uf invf.
  app composable_f_inv. 
Qed.

Theorem right_inv_compose_rf2 : forall f f' s'',
  composable f' f-> is_right_inverse s'' (compose f' f) -> injective f'->
  is_right_inverse (compose s'' f') f.
Proof. ir. assert (bijective f'). red. ee. am.
  assert(surjective (compose f' f)). ap surj_if_exists_right_inv. exists s''. 
  am.  app (surj_left_compose H H2).
  cp (source_right_inverse H0). awi H3. red in H0. ee.
  assert (composable s'' f'). red. ee.  fct_tac. fct_tac. am. 
  assert(is_function (compose s'' f')). fct_tac.
  assert(composable f (compose s'' f')). red in H0. ee. red. ee.  
  fct_tac.  am. aw.  awi H8. exact H8. cp (bijective_inv_function H2).
  set (invf:= inverse_fun f').
  assert (f = compose  invf (compose f' f)).  uf invf.
  wrr compose_assoc. rw (bij_left_inverse H2).  red in H; ee. rw H10. 
  rww compose_id_left.  app composable_inv_f.
  split. am. rw H9. rw compose_assoc. 
  wr (@compose_assoc (compose f' f)  s'' f'). rw H4. aw.
  rw compose_id_left.  uf invf. rww (bij_left_inverse H2). aw. fct_tac. am.
  am. red. uf invf. eee. fct_tac.  aw. red. red in H0; eee. aw. 
Qed. 

(** Properties of equipotency *)
Lemma equipotent_reflexive: forall x, equipotent x x.
Proof. ir. rw equipotentC.  exists (identityC x). app identityC_bijective.
Qed.
  
Lemma equipotent_symmetric:  forall a b,
  equipotent a b -> equipotent b a.
Proof. ir. rwi equipotentC H.  nin H. rw equipotentC. exists (inverseC H).
  app bijective_inverseC. 
Qed.
  
Lemma equipotent_transitive: forall a b c,
  equipotent a b -> equipotent b c -> equipotent a c.
Proof. ir. rwi equipotentC H;rwi equipotentC H0. nin H; nin H0.
  rw equipotentC. exists (composeC x0 x). app composeC_bij.
Qed.

Hint Resolve equipotent_reflexive: fprops.

(** Proposition 9  is the next 6 lemmas (each in 2 variants). Given f and g, 
when does there exists h such that the composition with f (in any order) is g *)

Lemma exists_left_composableC: forall (a b c:Set) (f:a->b)(g:a->c),
  surjectiveC g ->
  (exists h, composeC h g = f) =
  (forall (x y:a), g x = g y -> f x = f y).
Proof. ir. app iff_eq. ir. nin H0.  wr H0. uf composeC. rww H1. ir.
  pose (exists_right_inv_from_surjC H). nin e.
  exists (composeC f x). app arrow_extensionality. ir. uf composeC.
  app H0. rw (w_right_inverse (g a0) H1). tv.
Qed.

Theorem exists_left_composable: forall f g,
  is_function f -> surjective g -> source f = source g ->
  (exists h, composable  h g & compose h g = f) =
  (forall x y, inc x (source g) -> inc y (source g) -> 
    W x g = W y g -> W x f = W y f).
Proof. ir. app iff_eq. ir. nin H2. ee. wr H6. aw. rww H5.
  ir. assert (Ha: is_function g). fct_tac. cp (bcreate1_surjective Ha H0).
  set (bf:=bcreate H H1 (refl_equal (target f))).
  assert (exists h : target g -> (target f), composeC h (bcreate1 Ha) = bf).
  rw (exists_left_composableC bf H3).
  uf bf. ir. app R_inj.  do 2 rw prop_bcreate2. 
  app H2. app R_inc. app R_inc. do 2 wr (prop_bcreate1 Ha). rww H4.
  nin H4. exists (acreate x). ee. red. ee. fprops. am. aw.
  assert (acreate (composeC x (bcreate1 Ha)) = acreate bf). rww H4. 
  wri compose_acreate H5. rwi (bcreate_inv1 Ha) H5. rw H5.
  uf bf. rww bcreate_inv2.  
Qed.

Lemma exists_left_composable_auxC: forall (a b c:Set) (f:a->b) (g:a-> c) s h,
  surjectiveC g -> is_right_inverseC s g ->
  composeC h g = f -> h = composeC f s.
Proof. ir. wr H1. rw compositionC_associative. red in H0. rw H0. sy.
  app compose_id_rightC. 
Qed.

Theorem exists_left_composable_aux: forall f g s h ,
  is_function f -> surjective g -> source f = source g ->
  is_right_inverse s g ->
  composable  h g -> compose h g = f -> h = compose f s.
Proof. ir. wr H4. rw compose_assoc. red in H2. ee. rw H5. 
  assert (target g =  source h).  sy. red in H3; eee. rw H6. sy.  
  app  compose_id_right. fct_tac. am. red in H2; eee.
Qed.

Lemma exists_unique_left_composableC: forall (a b c:Set) (f:a->b)(g:a->c) h h',
  surjectiveC g -> composeC h g = f -> composeC h' g = f -> 
  h = h'.
Proof. ir. cp (exists_right_inv_from_surjC H). nin H2.
  set (exists_left_composable_auxC H H2 H1).
  set (exists_left_composable_auxC H H2 H0).
  rw e; rw e0. tv.
Qed.

Theorem exists_unique_left_composable: forall f g h h',
  is_function f -> surjective g -> source f = source g ->
  composable  h g -> compose h g = f -> 
  composable  h' g -> compose h' g = f -> h = h'.
Proof. ir. cp (exists_right_inv_from_surj H0). nin H6.
  pose (exists_left_composable_aux H H0 H1 H6 H2 H3).
  pose (exists_left_composable_aux H H0 H1 H6 H4 H5).
  rw e; rw e0. tv.
Qed.

Lemma left_composable_valueC: forall (a b c:Set) (f:a->b)(g:a->c) s h,
  surjectiveC g ->  (forall (x y:a), g x = g y -> f x = f y) ->
  is_right_inverseC s g  ->  h = composeC f s -> 
  composeC h g = f.
Proof. ir. app arrow_extensionality. ir. rw H2. uf composeC. app H0.
  rw (w_right_inverse (g a0) H1). tv.
Qed.

Theorem left_composable_value: forall f g s h,
  is_function f -> surjective g -> source f = source g ->
  (forall x y, inc x (source g) -> inc y (source g) -> 
    W x g = W y g -> W x f = W y f) ->
  is_right_inverse s g  ->  h = compose f s-> compose h g = f.
Proof. ir. red in H0; ee.
  cp (source_right_inverse H3). red in H3. ee. rw H4. 
  assert (composable f s). red. ee. am. fct_tac. red in H3; ee. rww H1.
  assert (composable (compose f s) g). red. ee;aw;fct_tac.
  app function_exten. fct_tac. sy; aw.  aw. aw. ir. aw. app H2. 
  red in H3; ee. rw H12. app inc_W_target. rw H6. fprops.
  set (w:= (W x g)).  wr compose_W. rw H7. srw. uf w.
  fprops. am. uf w. ue. ue. 
Qed.

Lemma exists_right_composable_auxC: forall (a b c:Set) (f:a->b) (g:c->b) h r,
  injectiveC g ->  is_left_inverseC r g  -> composeC g h = f
  -> h = composeC r f.
Proof. ir.  wr H1. wr compositionC_associative. rw H0. rww compose_id_leftC. 
Qed.

Theorem exists_right_composable_aux: forall f g h r,
  is_function f -> injective g -> target f = target g ->
  is_left_inverse r g  -> composable g h ->  compose g h = f
  -> h = compose r f.
Proof. ir.  wr H4. wr compose_assoc. red in H2. ee. rw H5. 
  red in H3; ee.  rw H7. rww compose_id_left. red in H2; eee. am.
Qed.

Lemma exists_right_composable_uniqueC: forall (a b c:Set)(f:a->b) (g:c->b) h h',
  injectiveC g -> composeC g h = f -> composeC g h' = f -> h = h'.
Proof. ir. app arrow_extensionality. ir.
  cp (exists_left_inv_from_injC (nonemptyT_intro (h a0))  H).  nin H2.
  assert (x (composeC g h a0) = x (composeC g h' a0)).  rw H0; rw H1; tv.
  ufi composeC H3. rwi (w_left_inverse (h a0) H2) H3.
  rwi (w_left_inverse (h' a0) H2) H3. am.
Qed.

Theorem exists_right_composable_unique: forall f g h h',
  is_function f -> injective g -> target f = target g ->
  composable g h ->  compose g h = f ->
  composable g h' ->  compose g h' = f -> h = h'.
Proof. ir.  nin (emptyset_dichot (source g)). 
  ir. app function_exten. red in H2; eee. red in H4; eee. 
  transitivity  (source f). wr H3. aw.  wr H5. aw. red in H2; ee. wr H8. 
  red in H4; ee. am. ir. red in H2; ee. assert (inc (W x h) (target h)). 
  fprops.  wri H9 H10. rwi H6 H10. nin H10. elim x0. 
  cp (exists_left_inv_from_inj H0 H6). nin H7.
  pose (exists_right_composable_aux H H0 H1 H7 H2 H3).
  pose (exists_right_composable_aux H H0 H1 H7 H4 H5). rw e; rw e0; tv.
Qed.

Lemma exists_right_composableC: forall (a b c:Set) (f:a->b) (g:c->b),
  injectiveC g ->
  (exists h, composeC g h = f) =  (forall u, exists v, g v = f u).
Proof. ir. app iff_eq. ir.  nin H0. wr H0. uf composeC. exists (x u). tv.
  ir. nin (emptyset_dichot c). 
  assert(a = emptyset). ap is_emptyset.  red. ir. 
  nin (H0 (Bo H2)). clear H3. rwi H1 x. elim x.
  symmetry in H1; symmetry in H2. cp empty_function_function.
  assert (source empty_function = a). uf empty_function. aw.
  assert (target empty_function = c). uf empty_function. aw.
  set (h:=bcreate H3 H4 H5). exists h. app arrow_extensionality. ir.
  assert False. wri H2 a0. elim a0. elim H6. nin H1.
  nin (exists_left_inv_from_injC (inc_nonempty H1) H). 
  exists (composeC x f). app arrow_extensionality.  ir. uf composeC.
  nin (H0 a0). wr H3. rww (w_left_inverse x0 H2).
Qed.

Theorem exists_right_composable: forall f g,
  is_function f -> injective g -> target f = target g ->
  (exists h, composable  g h & compose g h = f) = 
  (sub (range (graph f)) (range (graph g))).
Proof. ir. assert (Ha:is_function g). fct_tac.
  app iff_eq. ir. nin H2. nin H2. assert (source x = source f). wr H3. aw.
  red. ir. awi H5. nin H5.  cp (inc_pr1graph_source H H5). wri H4 H6.
  aw. exists (W x1 x). wr (W_pr H H5). wr H3. aw. graph_tac.
  red in H2. ee. rw H8. fprops. fprops. fprops.
  ir. nin (emptyset_dichot(source g)). nin (emptyset_dichot(source f)). 
  exists (empty_function). 
  assert (composable g empty_function). red. ee. am.
  app empty_function_function. uf empty_function. aw. ee. am. 
  app function_exten. fct_tac.
  sy;aw. uf empty_function. aw. sy;aw.  aw. ir. 
  ufi empty_function H6. awi H6. elim (emptyset_pr H6).
  nin H. nin H5. rwi H6 H4. nin H4. set (gf:=graph f) in H4. awi H4. nin H4.
  assert (inc x (range (graph g))). app H2. aw. exists y.
  am. fprops. awi H7. nin H7. cp (inc_pr1graph_source Ha H7).
  rwi H3 H8. elim (emptyset_pr H8). fprops. fprops.
  nin (exists_left_inv_from_inj H0 H3).
  cp (target_left_inverse H4). red in H4; ee.
  assert (composable x f). red. ee. fct_tac. am. ue. red in H4; eee.
  assert(is_function (compose x f)). fct_tac.
  assert (composable g (compose x f)). red. aw. auto. 
  exists  (compose x f). ee. am. ap function_exten. fct_tac.
  am. aw. sy;aw. ir. awi H10.  aw. wri (f_domain_graph H) H10. 
  set (gf:= graph f) in H10. 
  awi H10. nin H10. rw (W_pr H H10).
  assert (inc x1 (range (graph g))). app H2. aw. exists x0. am. fprops.
  awi H11. nin H11. assert (inc x2 (source g)). graph_tac.
  wr (W_pr Ha H11).  assert (W x2 (compose x g) = x2). rww H6.
  srw. awi H13. ue.  am. am. fprops. uf gf. fprops. 
Qed.

Lemma right_composable_valueC: forall (a b c:Set) (f:a->b) (g:c->b) r h,
  injectiveC g -> is_left_inverseC r g -> (forall u, exists v, g v = f u) ->
  h = composeC r f ->  composeC g h = f.
Proof. ir. rw H2. app arrow_extensionality. ir. nin (H1 a0).
  uf composeC.  wr H3. rww (w_left_inverse x H0).
Qed.

Theorem right_composable_value: forall f g r h,
  is_function f -> injective g -> target g = target f ->
  is_left_inverse r g ->
  (sub (range (graph f)) (range (graph g))) ->
  h = compose r f ->
  compose g h = f.
Proof. ir. rw H4. cp (target_left_inverse H2). red in H2; ee.
  assert (composable r f). red. ee. fct_tac. am. red in H2; ee. rww H8.
  assert (composable g (compose r f)). red.  eee. fct_tac.  fct_tac.  sy;aw.
  assert (composable g r). red. eee; fct_tac. 
  app function_exten. fct_tac. aw.  aw.  aw. ir. 
  assert (inc (W x f) (range (graph g))).
  app H3. rw range_inc_rw. exists x.  au.
  fct_tac. rwi range_inc_rw H11. nin H11. ee. aw. rw H12. 
  wr compose_W. wr compose_W.
  rww compose_assoc. rw H6. aw. srw. red. ee.
  red in H0; ee; am. fprops. aw.
  red. red in H2; eee; try fct_tac.  aw. ue. am. am.
  red in H2; ee. rw H14. fprops. fct_tac.
Qed.

(** ** EII-3-9 Functions of two arguments *)

(** Given a function f with two arguments and one argument, we obtain a function of one argument*)
Definition partial_fun2 f y :=
  BL(fun x=> W (J x y) f) (im_singleton (inverse_graph (source f)) y) (target f).

Definition partial_fun1 f x :=
  BL(fun y=> W (J x y) f)(im_singleton (source f) x) (target f).

Lemma partial_fun1_axioms: forall f x, is_function f -> is_graph(source f) ->
  transf_axioms (fun y=> W (J x y) f)(im_singleton (source f) x) (target f).
Proof. ir. red. ir. rwi im_singleton_pr H1. fprops.
Qed.

Lemma partial_fun1_function: forall f x, is_function f -> is_graph(source f) ->
  is_function (partial_fun1 f x).
Proof. ir. uf partial_fun1. app bl_function. app partial_fun1_axioms. 
Qed.

Lemma partial_fun1_W: forall f x y, is_function f -> is_graph(source f) ->
  inc (J x y) (source f) -> W y (partial_fun1 f x) = W (J x y) f.
Proof. ir. uf partial_fun1. aw. app partial_fun1_axioms.
Qed.

Lemma partial_fun2_axioms: forall f y, is_function f -> is_graph(source f) ->
  transf_axioms (fun x=> W (J x y) f)(im_singleton (inverse_graph (source f)) y)
  (target f).
Proof. ir. red. ir. rwi im_singleton_pr H1. awi H1. fprops. 
Qed.

Lemma partial_fun2_function: forall f y, is_function f -> is_graph(source f) ->
  is_function (partial_fun2 f y).
Proof. ir. uf partial_fun2. app bl_function. ap partial_fun2_axioms. am. am.
Qed.

Lemma partial_fun2_W: forall f x y, is_function f -> is_graph(source f) ->
  inc (J x y) (source f) -> W x (partial_fun2 f y) = W (J x y) f.
Proof. ir. uf partial_fun2. aw. app partial_fun2_axioms. aw. 
Qed.


(** Product of two functions *)
Definition ext_to_prod u v :=
  BL(fun z=> J (W (P z) u)(W (Q z) v))
  (product (source u)(source v))
  (product (target u)(target v)).

Lemma ext_to_prod_function: forall u v,
  is_function  u -> is_function v -> 
  is_function (ext_to_prod u v).
Proof. ir. uf ext_to_prod. app bl_function. red. ir. awi H1. ee.
  aw. eee. 
Qed.

Hint Resolve  ext_to_prod_function: fprops.

Lemma ext_to_prod_W: forall u v a b,
  is_function u -> is_function v-> inc a (source u) -> inc b (source v)->
  W (J a b) (ext_to_prod u v)  =  J (W a u) (W b v).
Proof. ir. uf ext_to_prod. aw. 
  red. ir.  awi H3. ee.  aw. eee. eee.  
Qed.

Lemma ext_to_prod_W2: forall u v c,
  is_function u -> is_function v->
  inc c (product (source u)(source v)) ->
  W c (ext_to_prod u v) =  J (W (P c) u) (W (Q c) v).
Proof. ir. awi H1. ee. 
  assert (J (P c) (Q c) =c). aw. wr H4. rww ext_to_prod_W. aw.
Qed.

Lemma ext_to_prod_range: forall u v,
  is_function u -> is_function v->
  range (graph (ext_to_prod u v)) = 
    product (range (graph u))(range (graph v)).
Proof. ir. assert (is_function (ext_to_prod u v)). fprops.
  set_extens. awi H2. nin H2. cp (W_pr H1 H2).  
  assert (inc x0 (source (ext_to_prod u v))). graph_tac. cp H4.
  ufi ext_to_prod H4. awi H4. aw. 
  rwii ext_to_prod_W2 H3. aw. ee. wr H3; fprops.
  exists (P x0). wr H3. aw. graph_tac. 
  exists (Q x0). wr H3. aw. graph_tac. aw.
  fprops. fprops. fprops.
  awi H2. ee. nin H3; nin H4. aw. 
  exists (J x0 x1). uf ext_to_prod. uf BL. aw.  uf L. aw.
  exists (J x0 x1). split. aw. ee.  fprops. graph_tac. graph_tac.
  aw. app uneq2. rw (W_pr H H3). rw (W_pr H0 H4). aw. fprops. fprops. fprops.
Qed.

Lemma ext_to_prod_propP: forall a a' (x: product a a'),  inc (P (Ro x)) a.
Proof. ir. assert (inc (Ro x) (product a a')).  app R_inc. awi H. int.
Qed.

Lemma ext_to_prod_propQ: forall a a' (x: product a a'),  inc (Q (Ro x)) a'.
Proof. ir. assert (inc (Ro x) (product a a')).  app R_inc.  awi H. int.
Qed.

Lemma ext_to_prod_propJ: forall (b b':Set) (x:b)(x':b'),
  inc (J (Ro x)(Ro x'))  (product b b').
Proof. ir. aw. ee. fprops. app R_inc. app R_inc.
Qed.
  
Definition pr1C a b:= fun x:product a b => Bo(ext_to_prod_propP x).
Definition pr2C a b:= fun x:product a b => Bo(ext_to_prod_propQ x).
Definition pairC (a b:Set) := fun (x:a)(y:b) => Bo(ext_to_prod_propJ x y).

Definition ext_to_prodC (a b a' b':Set) (u:a->a')(v:b->b') :=
  fun x => pairC (u (pr1C x)) (v (pr2C x)).

Lemma prC_prop: forall (a b:Set) (x:product a b),
  Ro x = J (Ro (pr1C x)) (Ro (pr2C x)).
Proof. ir. assert (inc (Ro x) (product a b)). app R_inc. awi H.
  ee.  uf pr1C. rw B_eq. uf pr2C. rw B_eq. aw. 
Qed.

Lemma pr1C_prop: forall (a b:Set) (x:product a b),
  Ro (pr1C x) =  P (Ro x). 
Proof. ir. rw (prC_prop x). aw. Qed.

Lemma pr2C_prop: forall (a b:Set) (x:product a b),
  Ro (pr2C x) =  Q (Ro x). 
Proof. ir. rw (prC_prop x). aw. Qed.

Lemma prJ_prop: forall (a b:Set) (x:a)(y:b),
  Ro(pairC x y) = J (Ro x) (Ro y).
Proof. ir. uf pairC. rw B_eq. tv.
Qed.

Lemma prJ_recov: forall (a b:Set) (x:product a b),
  pairC (pr1C x) (pr2C x) = x.
Proof. ir. app R_inj. rw prJ_prop. rw pr1C_prop. rw pr2C_prop. aw.
  assert (inc (Ro x) (product a b)). app R_inc. awi H. eee.
Qed.


Lemma ext_to_prod_prop:
  forall (a b a' b':Set) (u:a->a')(v:b->b') (x:a)(x':b),
  J(Ro (u x)) (Ro (v x')) = Ro(ext_to_prodC u v (pairC x x')).
Proof. ir. uf ext_to_prodC. rw prJ_prop.
  assert (x =  (pr1C (pairC x x'))). app R_inj. rw pr1C_prop. 
  rw prJ_prop. aw. wr H.
  assert (x' =  (pr2C (pairC x x'))). app R_inj. rw pr2C_prop. 
  rw prJ_prop. aw. wr H0. tv.
Qed.

(** If the two functions are a injective, surjective, bijective, 
so is the product. The inverse of the prodiuct is trivial *)

Lemma ext_to_prod_injective: forall u v,
  injective u -> injective  v-> injective (ext_to_prod u v).
Proof. ir.  nin H. nin H0. 
  red. ee. fprops. ir.  ufi ext_to_prod H3. awi H3.
  ufi ext_to_prod H4. awi H4.
  rwii ext_to_prod_W2 H5. rwii ext_to_prod_W2 H5. awi H3. awi H4. ee.
  app pair_extensionality. app H1.  inter2tac. app H2. inter2tac.  aw. aw.
Qed.

Lemma ext_to_prod_surjective: forall u v,
  surjective u -> surjective  v-> surjective (ext_to_prod u v).
Proof. ir. assert (Ha:is_function u). red in H; eee.
  assert (Hb:is_function v). red in H0; eee.
  app surjective_pr6. fprops. ir.
  ufi ext_to_prod H1.  awi H1. ee. cp (surjective_pr2 H H2). 
  cp (surjective_pr2 H0 H3).
  nin H4; nin H5;ee. exists (J x x0). ee. uf ext_to_prod. aw. ee. fprops. 
  aw. aw.
  rww ext_to_prod_W. assert(J (P y) (Q y) = y).  aw. wr H8. wr H7; wr H6. tv.
Qed.

Lemma ext_to_prod_bijective: forall u v,
  bijective u -> bijective  v-> bijective (ext_to_prod u v).
Proof. uf bijective. ir.  ee. app ext_to_prod_injective.
  app ext_to_prod_surjective.
Qed.

Lemma ext_to_prod_inverse: forall u v,
  bijective u -> bijective  v-> 
  inverse_fun (ext_to_prod u v) = 
  ext_to_prod (inverse_fun u)(inverse_fun v).
Proof. ir.
  assert (Ha:bijective (ext_to_prod u v)).  app ext_to_prod_bijective.
  assert (Hb:is_function (inverse_fun  u)).  app bijective_inv_function. 
  assert (Hc:is_function (inverse_fun  v)).  app bijective_inv_function. 
  ap function_exten.  app bijective_inv_function. 
  fprops. uf ext_to_prod. aw.  uf ext_to_prod. aw.
  aw. ir. ufi ext_to_prod H1.  awi H1.
  ee. set (Py := W (P x) (inverse_fun u)).
  assert (P x = W Py u). app W_inverse.
  set (Qy := W (Q x) (inverse_fun v)).
  assert (Q x = W Qy v). app W_inverse. 
  rww ext_to_prod_W2. fold Py. fold Qy.
  assert (inc Py (target (inverse_fun u))). uf Py. app inc_W_target. aw.
  assert (inc Qy (target (inverse_fun v))). uf Qy. app inc_W_target. aw.
  assert (inc (Q x) (source (inverse_fun v))). aw. fprops. 
  sy. ap W_inverse2. am. awi H6; awi H7; uf ext_to_prod. aw. eee.
  awi H6. awi H7. rw ext_to_prod_W. wr H4; wr H5. sy. aw.
  red in H;ee; red in H; ee;am. red in H0;ee; red in H0; eee. am.  am. bw. 
  aw. eee.
Qed.

(** Composition of products *)
Lemma composable_ext_to_prod2: forall u v u' v',
  composable u' u -> composable v' v -> 
  composable (ext_to_prod u' v') (ext_to_prod u v).
Proof. ir. red in H; red in H0. ee. red. ee. 
  fprops. fprops. uf ext_to_prod. aw. 
  rw H4; rw H2. tv.
Qed.

Lemma compose_ext_to_prod2: forall u v u' v',
  composable u' u ->   composable v' v -> 
  compose (ext_to_prod u' v') (ext_to_prod u v) =
  ext_to_prod (compose u' u)(compose v' v).
Proof. ir. assert (composable (ext_to_prod u' v') (ext_to_prod u v)).
  app  composable_ext_to_prod2.
  assert (is_function (compose u' u)). fct_tac.
  assert (is_function (compose v' v)).  fct_tac. red in H; red in H0; ee. 
  ap function_exten.  fct_tac.
  fprops.  uf ext_to_prod. aw.   uf ext_to_prod. aw.  aw. 
  ir. cp H8. ufi ext_to_prod H9. awi H9. ee.
  aw. rww ext_to_prod_W2. rww ext_to_prod_W2. rww ext_to_prod_W2. aw.
  red. au.  red; au. aw. eee. aw. eee.
  assert (product (source u') (source v')= target(ext_to_prod u v)).
  rw H7; rw H5. uf ext_to_prod. aw. rw H12. app inc_W_target.
  fprops. 
Qed.

Lemma injective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
  injectiveC u -> injectiveC  v-> injectiveC (ext_to_prodC u v).
Proof. ir. red. ir. assert (pairC (pr1C u0) (pr2C u0) = u0).
  rw prJ_recov. tv. assert (pairC (pr1C v0) (pr2C v0) = v0).
  rw prJ_recov. tv.
  assert (Ro (ext_to_prodC u v u0) = Ro (ext_to_prodC u v v0)).
  rw H1. tv. wri H2 H4. wri ext_to_prod_prop H4.
  wri H3 H4. wri ext_to_prod_prop H4.
  assert(pr1C u0 = pr1C v0). app H. app R_inj. inter2tac.
  wri H5 H3.  assert(pr2C u0 = pr2C v0). app H0. app R_inj. 
  inter2tac. wri H6 H3. wr H2; wr H3. tv.
Qed.

Lemma surjective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
  surjectiveC u -> surjectiveC  v-> surjectiveC (ext_to_prodC u v).
Proof. ir. red. ir. wr (prJ_recov u0).
  nin (H (pr1C u0)).   nin (H0 (pr2C u0)).
  exists (pairC x x0). app R_inj. wr ext_to_prod_prop.
  rw prJ_recov.  rw H1; rw H2. rw pr1C_prop. rw pr2C_prop. aw.
  assert (inc (Ro u0) (product a' b')). app R_inc. awi H3. ee. am.
Qed.

Lemma bijective_ext_to_prod2C:  forall (a b a' b':Set) (u:a->a')(v:b->b'),
  bijectiveC u -> bijectiveC  v-> bijectiveC (ext_to_prodC u v).
Proof. uf bijectiveC. ir.  ee. app injective_ext_to_prod2C.
  app surjective_ext_to_prod2C.
Qed.


Lemma compose_ext_to_prod2C: forall (a b c a' b' c':Set) (u:b-> c)(v:a->b) 
  (u':b'-> c')(v':a'->b'),
  composeC (ext_to_prodC u u') (ext_to_prodC v v') =
  ext_to_prodC (composeC u v)(composeC u' v').
Proof. ir.  uf composeC. app arrow_extensionality. ir. app R_inj.
  wr (prJ_recov a0). wr ext_to_prod_prop.
  cp (ext_to_prod_prop v v' (pr1C a0) (pr2C a0)). wri prJ_prop H.
  cp (R_inj H). wr H0. wr  ext_to_prod_prop. tv.
Qed.

Lemma inverse_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b')
  (Hu: bijectiveC u)(Hv:bijectiveC  v),
  inverseC (bijective_ext_to_prod2C Hu Hv)=
  ext_to_prodC (inverseC Hu)(inverseC Hv).
Proof. ir. app arrow_extensionality. ir. 
  assert (a0 = ext_to_prodC u v (ext_to_prodC (inverseC Hu) (inverseC Hv) a0)).
  cp ( compose_ext_to_prod2C u (inverseC Hu)  v(inverseC Hv)).
  assert (composeC (ext_to_prodC u v) 
    (ext_to_prodC (inverseC Hu) (inverseC Hv))  a0 =
      ext_to_prodC (composeC u (inverseC Hu)) (composeC v (inverseC Hv)) a0).
  rw H. tv. ufi composeC H0. rw H0. wr (prJ_recov a0). app R_inj.
  wr ext_to_prod_prop. rw inverseC_prb. rw inverseC_prb.  rw prJ_prop. tv.
  rw H. rw inverseC_pra. wrr H. 
Qed.

(** Canonical decomposition of a function *)
Lemma canonical_decomposition1: forall f g i,
  is_function f ->
  g = restriction2 f (source f) (range (graph f)) ->
  i = canonical_injection (range (graph f)) (target f) ->
  (composable i g & f = compose i g & injective i & surjective g &
  (injective f -> bijective g )).
Proof. ir. 
  assert (Ha:sub (range (graph f)) (target f)). nin H. fprops.
  assert (restriction2_axioms f (source f) (range (graph f))).
  red. ee. am.  app sub_refl. app Ha.
  uf image_by_fun. app sub_image_by_graph.
  assert (is_function g). rw H0. fprops.
  assert (is_function i). rw H1. fprops.
  assert (Hb: injective i). rw H1. app ci_injective.
  assert (Hd:source f = source g).  rw H0.  uf restriction2.  aw.
  assert (Hc:surjective g). rw H0. app restriction2_surjective. 
  uf image_of_fun. red in H; ee. rw H6. rw image_by_graph_domain. tv. 
  fprops.
  assert (composable i g). red. eee. rw H1. rw H0. 
  uf canonical_injection.  uf restriction2. aw.
  assert (f = compose i g). app function_exten. fct_tac.
  rw H0.  uf restriction2. aw. rw H1. uf canonical_injection. aw.
  ir. aw.
  rw H0. rw restriction2_W. rw H1. rw ci_W. tv. red in H; ee; red in H; ee; am. 
  rw range_inc_rw. exists x. au. am. am. am. ue.  
  eee. ir. red. ee.  apply inj_right_compose with i. am. ue. am.
Qed.

(** Restriction to its image *)

Definition imageC (a b:Set) (f:a->b) := IM (fun u:a => Ro (f u)).

Lemma imageC_inc: forall (a b:Set) (f:a->b) (x:a), inc (Ro (f x)) (imageC f).
Proof. ir. uf imageC. app IM_inc. exists x. tv. Qed.

Lemma imageC_exists: forall (a b:Set) (f:a->b) x,
  inc x (imageC f) -> exists y:a,  x = Ro (f y).
Proof. ir. ufi imageC H. cp (IM_exists H). nin H0.  exists x0. sy. am.
Qed.

Lemma sub_image_targetC: forall (a b:Set) (f:a->b), sub (imageC f) b.
Proof. ir. red. ir. cp (imageC_exists H). nin H0. rw H0. app R_inc. Qed.

Definition restriction_to_image (a b:Set) (f:a->b) :=
  fun x:a => Bo (imageC_inc f x).

Lemma restriction_to_image_pr: forall (a b:Set) (f:a->b) (x:a),
  Ro (restriction_to_image f x) = Ro (f x).
Proof. ir.  uf restriction_to_image. rw B_eq. tv. Qed.

Lemma canonical_decomposition1C: forall (a b:Set) (f:a->b)
  (g:a-> imageC f)(i:imageC f ->b),
  g = restriction_to_image f ->
  i = inclusionC (sub_image_targetC (f:=f))  ->
  (injectiveC i & surjectiveC g &
  (injectiveC f -> bijectiveC g )).
Proof. ir. assert (surjectiveC g). 
  rw H. red. ir. assert (inc (Ro u) (imageC f)). app R_inc.
  cp (imageC_exists H1).  nin H2. exists x. app R_inj.
  rw restriction_to_image_pr. sy; am. ir.
  uf restriction_to_image.
  ee. red. ir.   assert (Ro (i u) = Ro (i v)). rww H2.
  rwi H0 H3. rwi inclusionC_pr H3.  rwi inclusionC_pr H3. app R_inj. am.
  ir. red. ee.  red. ir.  assert (Ro (g u) = Ro (g v)). rw H3. tv.
  rwi H H4. rwi restriction_to_image_pr  H4. rwi restriction_to_image_pr  H4.
  app H2. app R_inj. am.
Qed.


End Bfunction. 

Export Bfunction.