Library sset4

Theory of Sets EII-6 Equivalence relations

Require Import ssreflect ssrbool eqtype ssrnat ssrfun.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset2.
Require Export sset3.

EII-6-1 Definition of an equivalence relation

Module Relation.

Definition substrate r := union2 (domain r) (range r ).

Lemma inc_pr1_substrate : forall r y,
  inc y r -> inc (P y) (substrate r).
Proof.
rewrite/substrate /domain=> r y yr; apply union2_first; aw; ex_tac.
Qed.

Lemma inc_pr2_substrate : forall r y,
  inc y r -> inc (Q y) (substrate r).
Proof.
rewrite/substrate /range=> r y yr; apply union2_second; aw; ex_tac.
Qed.

Lemma inc_arg1_substrate: forall r x y,
  related r x y -> inc x (substrate r).
Proof.
by move=> r x y rel; rewrite -(pr1_pair x y); apply inc_pr1_substrate.
Qed.

Lemma inc_arg2_substrate: forall r x y,
  related r x y -> inc y (substrate r).
Proof.
by move=> r x y rel;rewrite -(pr2_pair x y); apply inc_pr2_substrate.
Qed.

Ltac substr_tac :=
  match goal with
    | H:inc ?x ?r |- inc (P ?x) (substrate ?r)
      => apply (inc_pr1_substrate H)
    | H:inc ?x ?r |- inc (Q ?x) (substrate ?r)
      => apply (inc_pr2_substrate H)
    | H:related ?r ?x _ |- inc ?x (substrate ?r)
      => apply (inc_arg1_substrate H)
    | H:related ?r _ ?y |- inc ?y (substrate ?r)
      => apply (inc_arg2_substrate H)
    | H:inc(J ?x _ ) ?r|- inc ?x (substrate ?r)
      => apply (inc_arg1_substrate H)
    | H: inc (J _ ?y) ?r |- inc ?y (substrate ?r)
      => apply (inc_arg2_substrate H)
  end.

Lemma substrate_smallest : forall r s,
  (forall y, inc y r -> inc (P y) s) ->
  (forall y, inc y r -> inc (Q y) s) ->
  sub (substrate r) s.
Proof.
move=> r s h1 h2 x; rewrite /substrate/domain/range.
by aw; case; move=> [z [zr]] <-; [apply h1 | apply h2].
Qed.

Lemma inc_substrate_rw : forall r x,
  is_graph r -> inc x (substrate r) =
  ((exists y, inc (J x y) r) \/ (exists y, inc (J y x) r)).
Proof.
rewrite /substrate=> r x gr; aw; dw.
Qed.

Reflexivity properties for a relation

Definition reflexive_r (r: Set -> Set -> Prop) x :=
  forall y, inc y x = r y y.

Definition symmetric_r (r:Set -> Set -> Prop) :=
  forall x y, r x y -> r y x.

Definition transitive_r (r:Set -> Set -> Prop) :=
  forall x y z, r x y -> r y z -> r x z .

Definition equivalence_r (r:Set -> Set -> Prop) :=
  symmetric_r r & transitive_r r.

Definition equivalence_re (r:Set -> Set -> Prop) x :=
  equivalence_r r & reflexive_r r x.

Same definitions for a graph

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

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

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

Definition is_equivalence r :=
  is_reflexive r & is_transitive r & is_symmetric r.

Basic properties

Lemma equivalence_is_graph : forall r, is_equivalence r -> is_graph r.
Proof.
by move=> r [[res _] _]. Qed.

Hint Resolve equivalence_is_graph : fprops.

Lemma reflexive_inc_substrate : forall r x,
  is_reflexive r -> inc x (substrate r) = inc (J x x) r.
Proof.
move=> r x [g ir].
apply iff_eq; [apply ir | rewrite inc_substrate_rw//; move=> Jr; left; ex_tac].
Qed.

Lemma reflexive_ap : forall r x,
  is_reflexive r -> inc x (substrate r) -> related r x x.
Proof. by move=> r x rr xs; red; rewrite - reflexive_inc_substrate.
Qed.

Lemma reflexive_ap2 : forall r x y,
  is_reflexive r -> related r x y -> related r x x.
Proof.
by move=> r x y rr rxy; apply reflexive_ap=>//; substr_tac.
Qed.

Lemma symmetric_ap : forall r x y,
  is_symmetric r -> related r x y -> related r y x.
Proof.
by rewrite/is_symmetric=> r x y [gr sy] rxy; apply (sy _ _ rxy).
Qed.

Lemma transitive_ap : forall r x z,
  is_transitive r ->
  (exists y, related r x y & related r y z) ->
  related r x z.
Proof.
rewrite/is_symmetric=> r x z [gr tr] [y [rxy ryz]].
by apply (tr _ _ _ rxy ryz).
Qed.

Lemma symmetric_transitive_reflexive : forall r,
  is_symmetric r -> is_transitive r -> is_reflexive r.
Proof.
move=> r sr tr.
have gr: is_graph r by move: sr => [g _].
split=>// y; rewrite inc_substrate_rw//; case; move=> [z] => aux;
by apply transitive_ap=>//; rewrite /related; ex_tac; apply symmetric_ap.
Qed.

Lemma equivalence_relation_pr1 : forall r,
  is_graph r ->
  (forall x y, related r x y -> related r y x) ->
  (forall x y z, related r x y -> related r y z -> related r x z) ->
  is_equivalence r.
Proof.
move=> r gr sp tp.
have: (is_symmetric r) by auto.
have: (is_transitive r) by auto.
by red; intuition; apply symmetric_transitive_reflexive.
Qed.

Lemma symmetric_transitive_equivalence : forall r,
  is_symmetric r -> is_transitive r -> is_equivalence r.
Proof.
by move=> r sr tr; hnf; intuition; apply symmetric_transitive_reflexive.
Qed.

Lemma reflexivity_e : forall r u,
  is_equivalence r -> inc u (substrate r) -> related r u u.
Proof.
by move=> r u [rr _] us; apply reflexive_ap.
Qed.

Lemma symmetricity_e : forall r u v,
  is_equivalence r -> related r u v -> related r v u.
Proof.
by move=> r u v [_ [_ Hcsy ]]; apply symmetric_ap.
Qed.

Lemma transitivity_e : forall r u v w,
  is_equivalence r -> related r u v -> related r v w -> related r u w.
Proof.
move=> r u v w [_ [tr _]] r1 r2; apply transitive_ap=>//.
by exists v.
Qed.

Ltac equiv_tac:=
  match goal with
    | H: is_equivalence ?r, H1: inc ?u (substrate ?r) |- related ?r ?u ?u
      => apply (reflexivity_e H H1)
    | H: is_equivalence ?r |- inc (J ?u ?u) ?r
      => apply reflexivity_e
    | H:is_equivalence ?r, H1:related ?r ?u ?v |- related ?r ?v ?u
      => apply (symmetricity_e H H1)
    | H:is_equivalence ?r, H1: inc (J ?u ?v) ?r |- inc (J ?v ?u) ?r
      => apply (symmetricity_e H H1)
    | H:is_equivalence ?r, H1:related ?r ?u ?v, H2: related ?r ?v ?w
      |- related ?r ?u ?w
      => apply (transitivity_e H H1 H2)
    | H:is_equivalence ?r, H1:related ?r ?v ?u, H2: related ?r ?v ?w
      |- related ?r ?u ?w
      => apply (transitivity_e H (symmetricity_e H H1) H2)
    | H: is_equivalence ?r, H1: inc (J ?u ?v) ?r, H2: inc (J ?v ?w) ?r |-
      inc (J ?u ?w) ?r
      => apply (transitivity_e H H1 H2)
end.

Lemma domain_is_substrate: forall g,
  is_equivalence g -> domain g = substrate g.
Proof.
rewrite /substrate=> g eg.
set_extens u; first by apply union2_first.
move=> h;case (union2_or h) =>//.
have gg: is_graph g by fprops.
dw; move=> [x p]; exists x; equiv_tac.
Qed.

Lemma substrate_sub : forall r s,
  sub r s -> sub (substrate r) (substrate s).
Proof.
move=> r s rs; rewrite /substrate/range/domain/sub => x.
aw.
case; move=> [z [zr pz]]; move: (rs _ zr)=> zs; [left| right]; ex_tac.
Qed.

Lemma inc_substrate : forall r x,
  is_equivalence r ->
  inc x (substrate r) = (exists y, related r x y).
Proof.
move=> r x er; apply iff_eq => h.
  by exists x; equiv_tac.
by case h=> y py; substr_tac.
Qed.

Comparison of the two sets of definitions

Lemma reflexive_reflexive: forall r,
  is_reflexive r -> reflexive_r (related r) (substrate r).
Proof.
move=> r [gr rr] => y.
by apply iff_eq=> p; [ apply rr | substr_tac ].
Qed.

Lemma symmetric_symmetric: forall r,
  is_symmetric r -> symmetric_r (related r).
Proof. by move=> r [_]. Qed.

Lemma transitive_transitive: forall r,
  is_transitive r -> transitive_r (related r).
Proof. by move=> r [_]. Qed.

Lemma equivalence_equivalence: forall r,
  is_equivalence r -> equivalence_re (related r)(substrate r).
Proof.
move => r [ra [rb rc]].
split.
  by split; [apply symmetric_symmetric | apply transitive_transitive].
by apply reflexive_reflexive.
Qed.

We say that g is the graph of r if related g is the same function as r. We define the graph of r on x as the set of pairs of x related by r

Definition is_graph_of g (r:Set -> Set -> Prop):=
  forall u v, r u v = related g u v.

Definition graph_on (r:Set -> Set -> Prop) x:=
  Zo(product x x)(fun w => r (P w)(Q w)).

Lemma graph_on_graph: forall r x,
  is_graph(graph_on r x).
Proof.
by rewrite /graph_on=> r x y; rewrite Z_rw; aw; intuition.
Qed.

Lemma graph_on_rw0: forall r x a b,
  inc (J a b) (graph_on r x) = (inc a x & inc b x & r a b).
Proof.
by move=> r x a b; rewrite /graph_on Z_rw; aw; apply iff_eq; intuition.
Qed.

Lemma graph_on_rw1: forall r x a b,
  related (graph_on r x) a b = (inc a x & inc b x & r a b).
Proof.
by rewrite /related=> r x a b; apply graph_on_rw0.
Qed.

Lemma graph_on_substrate: forall r x,
  sub (substrate (graph_on r x)) x.
Proof.
move=> r x y; rewrite inc_substrate_rw //.
  case; move=> [z]; rewrite graph_on_rw0 ; intuition.
apply graph_on_graph.
Qed.

Lemma equivalence_has_graph0: forall r x,
  equivalence_re r x -> is_graph_of (graph_on r x) r.
Proof.
move=> r x [[rs rt] rr] u v; rewrite graph_on_rw1.
apply iff_eq; last by intuition.
move=> h.
have h1: (r v u) by apply rs.
have h2: (r u u) by apply (rt _ _ _ h h1).
have h3: (r v v) by apply (rt _ _ _ h1 h).
by rewrite (rr u)(rr v); intuition.
Qed.

Lemma graph_on_rw2: forall r x u v,
  equivalence_re r x ->
  related (graph_on r x) u v = r u v.
Proof. by move=> r x u v h; rewrite (equivalence_has_graph0 h).
Qed.

Lemma equivalence_has_graph:forall r x,
  equivalence_re r x -> exists g, is_graph_of g r.
Proof.
by move=> r x erx; exists (graph_on r x); apply equivalence_has_graph0.
Qed.

Lemma equivalence_if_has_graph:forall r g,
  is_graph g -> is_graph_of g r ->
  equivalence_r r -> equivalence_re r (domain g).
Proof.
rewrite /is_graph_of/related=> r g gg ggr [rs rt].
split=>//; move=> x; dw.
apply iff_eq.
  by move=> [y]; rewrite -ggr=> rxy; apply (rt _ _ _ rxy (rs _ _ rxy)).
by rewrite ggr; exists x.
Qed.

Lemma equivalence_if_has_graph2:forall r g,
  is_graph g -> is_graph_of g r ->
  equivalence_r r -> is_equivalence g.
Proof.
move=> r g gg gor [sr tr].
apply equivalence_relation_pr1=>//.
  by move=> x y; rewrite -2! gor; apply sr.
by move=> x y z; rewrite -3! gor; apply tr.
Qed.

Lemma equivalence_has_graph2: forall r x,
  equivalence_re r x -> exists g,
    is_equivalence g & (forall u v, r u v = related g u v).
Proof.
move=> r x ere.
have gr: is_graph (graph_on r x) by apply graph_on_graph.
have go: is_graph_of (graph_on r x) r by apply equivalence_has_graph0.
exists (graph_on r x); split.
  by move: ere => [er _]; apply (equivalence_if_has_graph2 gr go er).
by move=> u v; rewrite graph_on_rw2.
Qed.

Finest relation on a set: an element is only related to itself The correspondence is the identity, the graph is the diagonal

Definition restricted_eq x := fun u => fun v => inc u x & u = v.

Lemma diagonal_equivalence1: forall x,
  equivalence_re (restricted_eq x) x.
Proof.
rewrite /restricted_eq=> x; split.
  split.
    by move=> a b /= [ax] <-; intuition.
  by move=> a b c [au ab] [bu bc]; split =>//; ue.
move=> a; apply iff_eq; intuition.
Qed.

Lemma diagonal_equivalence2: forall x,
  is_graph_of (identity_g x) (restricted_eq x).
Proof. by move=> x y z; rewrite /related; aw. Qed.

Lemma diagonal_equivalence: forall x,
  is_equivalence (identity_g x).
Proof.
move=> x.
have gi: is_graph (identity_g x) by fprops.
move: (diagonal_equivalence2 x) => h1.
move: (diagonal_equivalence1 x)=> [h2 _].
apply (equivalence_if_has_graph2 gi h1 h2).
Qed.

Lemma diagonal_substrate: forall x, substrate(identity_g x) = x.
Proof.
move=> x; rewrite- domain_is_substrate.
  apply identity_domain.
apply diagonal_equivalence.
Qed.

The coarsest relation on a set: everything is related

Definition coarse u := product u u.

Lemma coarse_substrate : forall u, substrate (coarse u) = u.
Proof.
rewrite /coarse/substrate=> u.
transitivity (union2 u u); last by apply union2idem.
case (emptyset_dichot u); [ by move ->; srw | move=> h; dw ].
Qed.

Lemma coarse_related : forall u x y,
  related (coarse u) x y = (inc x u & inc y u).
Proof.
rewrite /coarse/related=> u x y.
aw; apply iff_eq; intuition; fprops.
Qed.

Lemma coarse_graph: forall x, is_graph (coarse x).
Proof.
rewrite /coarse=> x; apply product_is_graph.
Qed.

Lemma coarse_equivalence : forall u,
  is_equivalence (coarse u).
Proof.
move=> u.
have gc:is_graph (coarse u) by apply coarse_graph.
split.
  split =>//.
  by move => y; rewrite coarse_substrate coarse_related.
split; split => //.
  by move=> x y z; rewrite 3! coarse_related ;intuition.
  by move=> x y; rewrite 2! coarse_related ;intuition.
Qed.

Lemma inter2_is_graph1: forall x y, is_graph x ->
  is_graph (intersection2 x y).
Proof. by move=> x y gx t; aw; move => [tx _]; apply gx. Qed.

Lemma inter2_is_graph2: forall x y, is_graph y ->
  is_graph (intersection2 x y).
Proof. by move=> x y gx t; aw; move => [_ tx ]; apply gx. Qed.

Lemma union2_is_graph: forall x y, is_graph x -> is_graph y ->
  is_graph (union2 x y).
Proof.
move=> x y gx gy t tu; case (union2_or tu); [apply gx | apply gy].
Qed.

Lemma sub_graph_coarse_substrate: forall r,
  is_graph r -> sub r (coarse (substrate r)).
Proof.
rewrite /coarse=> r gr t tr.
apply product_inc; first (by apply gr); substr_tac.
Qed.

Example of an equivalence without graph: equipotency

Lemma equipotent_equivalence: equivalence_r equipotent.
Proof.
split.
by move=> x y;apply equipotent_symmetric.
move => x y z; apply equipotent_transitive.
Qed.

Example 5 page E II.114

Lemma equivalence_relation_bourbaki_ex5: forall a e, sub a e ->
  is_equivalence (
    Zo(product e e)(fun y=>
      (inc (P y)(complement e a)& (P y = Q y)) \/ (inc (P y) a & inc(Q y) a))).
Proof.
move => a e sa.
set (f := fun x y:Set =>
         (inc x (complement e a) & x = y) \/ (inc x a & inc y a)).
set (g := (Zo (product e e) (fun z => f (P z) (Q z)))); rewrite -/g.
have rgf: forall x y, inc x e -> inc y e -> (related g x y) = f x y.
  by rewrite/related/g => x y xe ye; rewrite Z_rw; aw; apply iff_eq; intuition.
have rg: forall x, inc x e -> related g x x.
  move=> x xe; rewrite rgf //.
  by case (inc_or_not x a) ;[ right | left; srw].
have sg: substrate g = e.
  apply extensionality; rewrite /g.
    by apply substrate_smallest=> y; rewrite Z_rw; aw; intuition.
  by move => t te; move: (rg _ te) => h; substr_tac.
have gg: is_graph g.
  by move=> x; rewrite /g Z_rw; aw; intuition.
have rrg :forall x y, related g x y -> (inc x e & inc y e).
  by rewrite /related/g => x y; rewrite Z_rw; aw; intuition.
split.
  split =>//; ue.
split; split=>//.
  move=> x y z r1 r2; move:(rrg _ _ r1) (rrg _ _ r2)=> [xe ye][_ ze].
  move: r1 r2; do 3 rewrite rgf //.
  case.
    by move => [_] ->.
  move=> [xa ya]; case; first by srw; move => [[_ nya] _]; contradiction.
  by move=> [_ za]; right.
move=> x y rxy; move: (rrg _ _ rxy) => [xe ye]; move: rxy.
do 2 rewrite rgf //; rewrite /f.
case (equal_or_not x y); first by move=> ->.
move => hyp; case; first by move => [_ xy]; contradiction.
by move => [xa ya]; auto.
Qed.

Intersection of equivalence relations is an equivalence

Lemma inter_rel_graph : forall z,
  nonempty z -> (forall r, inc r z -> is_graph r) ->
  is_graph (intersection z).
Proof.
move => z [t tz] alg y yi.
apply (alg _ tz).
by apply intersection_forall with z.
Qed.

Lemma inter_rel_rw : forall z x y,
  nonempty z ->
  related (intersection z) x y =
  (forall r, inc r z -> related r x y).
Proof.
rewrite /related=> z x y nez; apply iff_eq; srw.
Qed.

Lemma inter_rel_reflexive : forall z,
  nonempty z -> (forall r, inc r z -> is_reflexive r) ->
  is_reflexive (intersection z).
Proof.
move => z nez alr.
split.
  by apply inter_rel_graph=>//e rz; move: (alr _ rz)=> [g _].
move=> y; rewrite inter_rel_rw // => ys r rz.
move: (alr _ rz)=> [_ rr]; apply rr.
have ssr: (sub (intersection z) r) by apply intersection_sub.
apply (substrate_sub ssr ys).
Qed.

Lemma inter_rel_substrate : forall z e,
  nonempty z -> (forall r, inc r z -> is_reflexive r) ->
  (forall r, inc r z -> substrate r = e) ->
  substrate (intersection z) = e.
Proof.
move=> z e nez allr alls.
move: (inter_rel_reflexive nez allr)=> ir.
set_extens t => ts.
  move : ir => [_ ir]; move: (ir _ ts); rewrite /related=> aux.
  move: nez => [u uz]; move: (intersection_forall aux uz) => Ju.
  by rewrite - (alls _ uz); apply (inc_arg1_substrate Ju).
have rtt: related (intersection z) t t.
   rewrite inter_rel_rw //.
   move => r rz; rewrite - (alls _ rz) in ts.
   move: (allr _ rz)=> [_]; apply =>//.
substr_tac.
Qed.

Lemma inter_rel_transitive : forall X,
  nonempty X -> (forall r, inc r X -> is_transitive r) ->
  is_transitive (intersection X).
Proof.
move=> X neX allt; split.
  by apply inter_rel_graph=>//e rz; move: (allt _ rz)=> [g _].
move=> x y z; do 3 rewrite inter_rel_rw //; move => rxy ryz r rz.
move: (allt _ rz)(rxy _ rz) (ryz _ rz) => [_]; apply.
Qed.

Lemma inter_rel_symmetric : forall z,
  nonempty z -> (forall r, inc r z -> is_symmetric r) ->
  is_symmetric (intersection z).
Proof.
move=> X neX alls; split.
  by apply inter_rel_graph=>//e rz; move: (alls _ rz)=> [g _].
move=> x y; do 2 rewrite inter_rel_rw // ; move => rxy r rz.
move: (alls _ rz) (rxy _ rz) => [_]; apply.
Qed.

Lemma inter_rel_equivalence : forall z,
  nonempty z -> (forall r, inc r z -> is_equivalence r) ->
  is_equivalence (intersection z).
Proof.
move=> z ne alleq; apply symmetric_transitive_equivalence.
  by apply inter_rel_symmetric=>//; move => r rz; move: (alleq _ rz)=> [_ []].
by apply inter_rel_transitive=>//; move => r rz; move: (alleq _ rz)=> [_ []].
Qed.

The set of all relations or all equivalences of a set

Definition all_relations x :=
  powerset (product x x).

Lemma inc_all_relations : forall r x,
  inc r (all_relations x) = (is_graph r & sub (substrate r) x).
Proof.
move=> r x; rewrite /all_relations powerset_inc_rw.
apply iff_eq => h.
  have gr: (is_graph r) by move=>t tr; move: (h _ tr); aw; intuition.
  split =>//.
  move=> t; rewrite inc_substrate_rw//; case; move=> [y Jr]; move: (h _ Jr); aw; intuition.
move: h=> [gr srx];move=> t tr; move: (gr _ tr) => pt.
aw; split=>//;split; apply srx; substr_tac.
Qed.

Definition all_equivalence_relations x :=
  Zo (all_relations x) (fun r => (is_equivalence r)
    & (substrate r = x)).

Lemma inc_all_equivalence_relations : forall r x,
  inc r (all_equivalence_relations x) =
  (is_equivalence r & (substrate r = x)).
Proof.
rewrite/all_equivalence_relations=> r x; rewrite Z_rw.
apply iff_eq; first by intuition.
rewrite inc_all_relations; move=> [er sr]; intuition; ue.
Qed.

Lemma inc_coarse_all_equivalence_relations : forall u,
  inc (coarse u) (all_equivalence_relations u).
Proof.
move=> u; rewrite inc_all_equivalence_relations; split.
  apply coarse_equivalence.
rewrite coarse_substrate//.
Qed.

We show that an equivalence is a self-inverse projector

Lemma selfinverse_graph_symmetric: forall r,
  is_symmetric r = (r= inverse_graph r).
Proof.
move=> r; rewrite /is_symmetric/related.
apply iff_eq.
  move=> [gr sp].
  set_extens t => tr.
    by move: (gr _ tr) => aux;rewrite - aux; aw; apply sp; rewrite aux.
  move: (inverse_graph_is_graph tr)=> pt.
  move: tr; rewrite -pt; aw; apply sp.
move=> rir.
split; first by rewrite rir; fprops.
move=> x y Jr; rewrite rir; aw.
Qed.

Lemma idempotent_graph_transitive: forall r,
  is_graph r-> (is_transitive r = sub (compose_graph r r) r).
Proof.
move=> r gr; apply iff_eq.
  move=> tr t; aw. move=> [pt [y [J1r J2r]]].
  have: (J (P t) (Q t) = t) by aw.
  by move=> <-; move: tr J1r J2r => [_ ]; apply.
move => scr.
split =>//; rewrite /related => x y z Jxy Jyz.
apply scr; aw; split; [ fprops | ex_tac ].
Qed.

Theorem equivalence_pr: forall r,
  (is_equivalence r = ((compose_graph r r) = r & r= inverse_graph r)).
Proof.
move=> r; apply iff_eq => hyp.
  have gr: is_graph r by fprops.
  split.
    apply extensionality.
      by rewrite - idempotent_graph_transitive //; move: hyp=> [_ []].
    move=> x xr.
    have px: is_pair x by apply gr.
    aw;split => //.
    exists (P x); split; [ equiv_tac =>//; substr_tac | by rewrite px].
  by rewrite -selfinverse_graph_symmetric; move: hyp=> [_ []].
move: hyp=> [crr ri].
have gr: (is_graph r) by rewrite ri; fprops.
apply symmetric_transitive_equivalence.
  rewrite selfinverse_graph_symmetric //.
rewrite idempotent_graph_transitive //; ue.
Qed.

EII-6-2 Equivalence classes; quotient set

Equivalence associated to a function f by f x = f y

Definition eq_rel_associated f :=
  fun x => fun y => (inc x (source f) & (inc y (source f)) & (W x f = W y f)).

Definition equivalence_associated f :=
  compose_graph (inverse_graph (graph f)) (graph f).

Lemma ea_equivalence: forall f,
  is_function f -> equivalence_re(eq_rel_associated f)(source f).
Proof.
move=> f ff; rewrite /eq_rel_associated.
split.
  split; first by move=> x y /=; intuition.
  by move => x y z [ xs [ys Wxy][_ [zs Wyz]]]; intuition; ue.
move => x; apply iff_eq; intuition.
Qed.

Lemma graph_of_ea: forall f,
  is_function f ->
  is_graph_of (equivalence_associated f) (eq_rel_associated f).
Proof.
rewrite /equivalence_associated=> f ff u v.
have gf: is_graph (graph f) by fprops.
have gif: is_graph (inverse_graph (graph f)) by fprops.
apply iff_eq; aw.
  move=> [usf [vsf WW]].
  by exists (W u f); rewrite/related; split; [| aw; rewrite WW]; graph_tac.
move=> [y]; rewrite /related; aw; move=> [J1g J2g].
split; first by apply (related_inc_source ff J1g).
split; first by apply (related_inc_source ff J2g).
by rewrite (W_pr ff J1g) (W_pr ff J2g).
Qed.

Lemma graph_ea_equivalence: forall f,
  is_function f->
  is_equivalence (equivalence_associated f).
Proof.
move=> f ff.
move: (graph_of_ea ff) => igo.
have ge: (is_graph (equivalence_associated f)).
  by rewrite/equivalence_associated; fprops.
apply (equivalence_if_has_graph2 ge igo).
by move: (ea_equivalence ff) => [].
Qed.

Lemma graph_ea_substrate: forall f,
  is_function f->
  substrate (equivalence_associated f) = source f.
Proof.
move => f ff;
move: (graph_ea_equivalence ff)=> ea.
move: (graph_of_ea ff) => igo.
set_extens t; rewrite inc_substrate //.
  by move=> [y];rewrite -igo; case.
move=> tf; exists t; rewrite -igo; hnf; intuition.
Qed.

Lemma ea_related:forall f x y,
  is_function f ->
  related (equivalence_associated f) x y =
  (inc x (source f) & inc y (source f) & W x f = W y f).
Proof.
by move=> f x y ff; move: (graph_of_ea ff)=> <-.
Qed.

The class of x is the set of elements related to x

Definition class (r x:Set) := fun_image (Zo r (fun z => P z = x)) Q.

Lemma inc_class : forall r x y,
  is_equivalence r -> inc y (class r x) = related r x y.
Proof.
rewrite /class=> r x y er; aw.
have gr: (is_graph r) by fprops.
apply iff_eq.
  move=> [z]; rewrite Z_rw; move=>[[zr]] <- <-.
  by rewrite/related (gr _ zr).
move=> h; exists (J x y); split; try apply Z_inc;aw.
Qed.

Hint Rewrite inc_class : bw.

Lemma class_is_cut: forall r x, is_equivalence r ->
  class r x = im_singleton r x.
Proof.
by move=> r x er; set_extens t; aw; bw.
Qed.

Lemma sub_class_substrate: forall r x,
  is_equivalence r -> sub (class r x) (substrate r).
Proof.
move=> r x er t; bw=>rt; substr_tac.
Qed.

Lemma nonempty_class_symmetric : forall r x,
  is_equivalence r ->
  nonempty (class r x) = inc x (substrate r).
Proof.
move=> r x er; apply iff_eq.
  move=> [c]; bw => rcx; substr_tac.
move=> xs; exists x; bw; equiv_tac.
Qed.

Lemma related_class_eq1: forall r u v, is_equivalence r ->
  related r u v -> class r u = class r v.
Proof.
move=> r u v er ruv.
have gr: is_graph r by fprops.
set_extens x; bw=> aux; equiv_tac.
Qed.

Lemma related_class_eq : forall r u v,
  is_equivalence r ->
  related r u u ->
  related r u v = (class r u = class r v).
Proof.
move=> r u v er ruu.
apply iff_eq; first by apply related_class_eq1.
move=> crurv.
have: inc u (class r u) by bw.
rewrite crurv; bw=> h; equiv_tac.
Qed.

Definition of the quotient of an equivalence

Definition is_class r x := is_equivalence r
  & inc (rep x) (substrate r) & x = class r (rep x).

Definition quotient r := fun_image (substrate r) (class r).

Lemma inc_rep_itself:forall r x, is_equivalence r ->
  inc x (quotient r) -> inc (rep x) x.
Proof.
rewrite/quotient => r x er. aw. move=> [z [zr cz]].
by apply nonempty_rep; rewrite -cz nonempty_class_symmetric.
Qed.

Lemma non_empty_in_quotient: forall r x,
  is_equivalence r -> inc x (quotient r) -> nonempty x.
Proof.
move=> r x er xq; exists (rep x); apply (inc_rep_itself er xq).
Qed.

Lemma is_class_class : forall r x, is_equivalence r ->
  inc x (substrate r) -> is_class r (class r x).
Proof.
move=> r x er xs.
have cq: (inc (class r x) (quotient r)) by rewrite/quotient; aw;ex_tac.
move: (inc_rep_itself er cq); bw => rxr.
split =>//; split=>//; [substr_tac| apply related_class_eq1=>//].
Qed.

Lemma inc_itself_class : forall r x,
  is_equivalence r ->inc x (substrate r) -> inc x (class r x).
Proof. by move=> r rx er xs; bw; equiv_tac. Qed.

Lemma inc_quotient : forall r x, is_equivalence r ->
  inc x (quotient r) = is_class r x.
Proof.
rewrite /quotient => r x er; apply iff_eq; aw.
  by move=> [z [zs ]] <-; apply is_class_class.
by rewrite /is_class; move=> [_ [irs xv]]; ex_tac.
Qed.

Hint Rewrite inc_quotient: sw.

Lemma class_rep : forall r x, is_equivalence r ->
  inc x (quotient r) -> class r (rep x) = x.
Proof.
by move=> r x e; srw; move=> [_ [_ ]] <-.
Qed.

Lemma in_class_related : forall r y z,
  is_equivalence r ->
  related r y z = (exists x, is_class r x & inc y x & inc z x).
Proof.
move=> r y x er; apply iff_eq.
  move=> ryx;
  have ys: inc y (substrate r) by substr_tac.
  exists (class r y).
  by split; [apply is_class_class| bw; split=>//; equiv_tac].
by move =>[w [[ _ [Hb ]] []]] ->; bw; move=> [yw xw]; equiv_tac.
Qed.

Lemma related_rep_in_class:forall r x y,
  is_equivalence r -> inc x (quotient r) -> inc y x
  -> related r (rep x) y.
Proof.
move=> r x y er xq yx; rewrite in_class_related //.
exists x; rewrite -inc_quotient //; intuition.
apply (inc_rep_itself er xq).
Qed.

Lemma is_class_rw : forall r x, is_equivalence r ->
  is_class r x = (nonempty x & sub x (substrate r) &
    (forall y z, inc y x -> (inc z x = related r y z)) ).
Proof.
move=> r x er; apply iff_eq.
  move=> cx; move: (cx) => [_ [rxs xc]].
  split; first by rewrite xc; exists (rep x); bw; equiv_tac.
  split; first by move=> t; rewrite xc; apply (sub_class_substrate er).
  move=> y z yz; apply iff_eq.
    rewrite (in_class_related y z er).
     by move=> zx; exists x; intuition.
  by move: yz;rewrite xc; bw => eq1 eq2; equiv_tac.
move=> [nex [cs alr]].
move: (nonempty_rep nex) => p1.
split =>//; split; first by apply cs.
set_extens t; bw.
  by move=> tw; rewrite -alr.
by rewrite -alr.
Qed.

Hint Rewrite is_class_rw : dw.

Lemma class_dichot : forall r x y,
  is_class r x -> is_class r y -> (x = y \/ disjoint x y).
Proof.
move=> r x y cx cy.
mdi_tac xy; move: (cx) (cy)=> [er [rxs]] -> [_ [rys]]-> => z; bw => zx zy.
move: (cx) (cy); do 2 rewrite -inc_quotient //.
move=> xq yq; elim xy; rewrite -(class_rep er xq) -(class_rep er yq).
apply related_class_eq1=>//.
have p3: related r z (rep y) by equiv_tac.
equiv_tac.
Qed.

Lemma inc_class_quotient : forall r x,
  is_equivalence r -> inc x (substrate r) ->
  inc (class r x) (quotient r).
Proof.
move=> r x er xs; srw; apply is_class_class=>//.
Qed.

Lemma inc_in_quotient_substrate : forall r x y,
  is_equivalence r -> inc x y -> inc y (quotient r)
  -> inc x (substrate r).
Proof.
move=> r x y er xy; srw; rewrite is_class_rw //.
by move=> [_ [syr _]]; apply syr.
Qed.

Hint Resolve inc_class_quotient: gprops.

Lemma union_quotient : forall r,
  is_equivalence r -> union (quotient r) = substrate r.
Proof.
move=> r er; set_extens t => ts.
  move: (union_exists ts) => [z [tz zu]].
  by apply (inc_in_quotient_substrate er tz zu).
apply union_inc with (class r t); [ bw; equiv_tac | gprops].
Qed.

Lemma inc_rep_substrate : forall r x, is_equivalence r ->
  inc x (quotient r) -> inc (rep x) (substrate r).
Proof.
by move=> r x er; srw; move=> [_ [g _]].
Qed.

Hint Resolve inc_rep_substrate: fprops.

Lemma related_rep_class : forall r x, is_equivalence r ->
  inc x (substrate r) -> related r x (rep (class r x)).
Proof.
move=> r x er xs.
suff: related r (rep (class r x)) x by move=> h; equiv_tac.
apply related_rep_in_class=>//.
   by srw; apply is_class_class.
by apply inc_itself_class.
Qed.

Lemma related_rep_rep : forall r u v,
  is_equivalence r -> inc u (quotient r) -> inc v (quotient r) ->
  related r (rep u) (rep v) = (u = v).
Proof.
move =>r u v er uq vq. apply iff_eq.
  move=> h; rewrite - (class_rep er uq) -(class_rep er vq).
  by apply related_class_eq1.
move=> ->.
have rs: (inc (rep v) (substrate r)) by fprops.
equiv_tac.
Qed.

Lemma related_rw : forall r u v,
  is_equivalence r -> related r u v =
  (inc u (substrate r) & inc v (substrate r) & class r u = class r v).
Proof.
move=> r u v er; apply iff_eq.
  move=> ruv.
  by split; [substr_tac | split; [ substr_tac| apply related_class_eq1]].
by move=> [us [vs cuv]]; rewrite related_class_eq //; equiv_tac.
Qed.

Lemma is_class_pr: forall r x y,
  is_equivalence r -> inc x y -> inc y (quotient r)
  -> y = class r x.
Proof.
move=> r x y er xy yq.
have : class r (rep y) = y by apply class_rep.
move =><-; apply related_class_eq1=>//.
apply (related_rep_in_class er yq xy).
Qed.

Canonical projection on the quotient

Definition canon_proj (r:Set) := BL(fun x=> class r x)
  (substrate r) (quotient r).

Lemma canon_proj_function: forall r,
  is_equivalence r -> is_function (canon_proj r).
Proof.
rewrite/canon_proj=> r er.
apply bl_function; move=> t ts /=; gprops.
Qed.

Lemma canon_proj_source: forall r, source (canon_proj r) = substrate r.
Proof. rewrite /canon_proj => x; aw. Qed.

Lemma canon_proj_target: forall r, target (canon_proj r) = quotient r.
Proof. rewrite /canon_proj => x; aw. Qed.

Hint Rewrite canon_proj_source canon_proj_target: aw.
Hint Resolve canon_proj_function: fprops.

Lemma canon_proj_W:forall r x,
  is_equivalence r ->
  inc x (substrate r) -> W x (canon_proj r) = class r x.
Proof. rewrite /canon_proj=> r x er xs; aw; move=> t ts /=; gprops. Qed.

Hint Rewrite canon_proj_W : aw.

Lemma canon_proj_inc:forall r x,
  is_equivalence r->
  inc x (substrate r) -> inc (W x (canon_proj r)) (quotient r).
Proof. move=> r x er xs; aw; gprops. Qed.

Lemma related_graph_canon_proj: forall r x y,
  is_equivalence r -> inc x (substrate r) -> inc y (quotient r) ->
  inc (J x y) (graph (canon_proj r)) = inc x y.
Proof.
move=> r x y er xs yq.
have fc: (is_function (canon_proj r)) by fprops.
apply iff_eq => h.
  move: (W_pr fc h); aw => <-; bw; equiv_tac.
have: (y = W x (canon_proj r)).
  aw; move: (class_rep er yq) h => <-; bw; move=> rryx.
  apply related_class_eq1 =>//.
move=> ->; graph_tac; aw.
Qed.

Lemma canon_proj_show_surjective:forall r x,
  is_equivalence r-> inc x (quotient r)
  -> W (rep x)(canon_proj r) = x.
Proof.
move=> r x er xq.
have rs: (inc (rep x) (substrate r)) by fprops.
by aw; apply class_rep.
Qed.

Lemma canon_proj_surjective:forall r,
  is_equivalence r-> surjection (canon_proj r).
Proof.
move=> r er; apply surjective_pr6; first by fprops.
move=> y; aw => yr.
have rs: (inc (rep y) (substrate r)) by fprops.
by ex_tac; aw; apply class_rep.
Qed.

Lemma sub_im_canon_proj_quotient: forall r a x,
  is_equivalence r -> sub a (substrate r) ->
  inc x (image_by_fun (canon_proj r) a) ->
  inc x (quotient r).
Proof.
move=> r a x er sas xi.
have fc:is_function (canon_proj r) by fprops.
move: xi; aw; last by aw.
move=> [u [ua Wu]]; rewrite - Wu; aw; gprops.
Qed.

Criterion 55

Lemma related_e_rw: forall r u v,
is_equivalence r -> (related r u v =
   (inc u (source (canon_proj r)) &
     inc v (source (canon_proj r)) &
     W u (canon_proj r) = W v (canon_proj r))).
Proof.
move=> r u v er; rewrite related_rw //.
apply iff_eq.
  by move => [us [vs cuv]]; aw; intuition.
rewrite canon_proj_source; move => [us [vs]]; aw; intuition.
Qed.

The diagonal is the graph of equality

Lemma diagonal_class: forall x u,
  inc u x -> class (identity_g x) u = singleton u.
Proof.
move=> x u ux.
have ed: (is_equivalence (identity_g x)) by apply diagonal_equivalence.
set_extens t; bw;rewrite /related; aw.
  case; done.
by move=> ->.
Qed.

Lemma canon_proj_diagonal_bijective: forall x,
  bijection (canon_proj (identity_g x)).
Proof.
move=> x.
have ei: is_equivalence (identity_g x) by apply diagonal_equivalence.
have fc: is_function (canon_proj (identity_g x)) by fprops.
split; last by apply canon_proj_surjective.
split =>//.
aw; move=> a b ax bx; aw.
move: ax bx;rewrite diagonal_substrate => ax bx.
do 2(rewrite diagonal_class //).
apply singleton_inj.
Qed.

Relation associated to P in a product

Definition first_proj_eqr (x y:Set) :=
  eq_rel_associated(first_proj (product x y)).

Definition first_proj_eq (x y :Set) :=
  equivalence_associated (first_proj (product x y)).

Lemma first_proj_eq_pr: forall x y a b,
  first_proj_eqr x y a b =
  (inc a (product x y) & inc b (product x y) & P a = P b).
Proof.
rewrite /first_proj_eqr /eq_rel_associated => x y a b.
have gp: is_graph (product x y) by apply product_is_graph.
have: source (first_proj (product x y)) = product x y
  by rewrite /first_proj; aw.
move=> ->.
apply iff_eq; move=> [ap [bp]]; do 2 rewrite first_proj_W //; intuition.
Qed.

Lemma first_proj_graph: forall x y,
  is_graph_of(first_proj_eq x y)(first_proj_eqr x y).
Proof.
rewrite /first_proj_eq/first_proj_eqr.
move=> x y; apply graph_of_ea; apply first_proj_function.
Qed.

Lemma first_proj_equivalence: forall x y,
  is_equivalence (first_proj_eq x y).
Proof.
rewrite /first_proj_eq => x y.
apply graph_ea_equivalence; apply first_proj_function.
Qed.

Lemma first_proj_eq_related: forall x y a b,
  related (first_proj_eq x y) a b =
  (inc a (product x y) & inc b (product x y) & P a = P b).
Proof.
move=> x y a b.
move:(first_proj_graph x y).
by move=> <-; rewrite first_proj_eq_pr.
Qed.

Lemma first_proj_substrate: forall x y,
  substrate(first_proj_eq x y) = product x y.
Proof.
move=> x y; rewrite /first_proj_eq.
set f:=first_proj _ .
have ff: (is_function f) by rewrite /f;apply first_proj_function.
rewrite graph_ea_substrate // /f/first_proj; aw.
Qed.

Lemma first_proj_class:forall x y z,
  nonempty y ->
  is_class (first_proj_eq x y) z =
  exists u, inc u x & z = product (singleton u) y.
Proof.
move=> x y z ney.
set (r:=first_proj_eq x y).
have er: is_equivalence r by rewrite /r; apply first_proj_equivalence.
move: (first_proj_substrate x y)=> sr; fold r in sr.
apply iff_eq.
   rewrite is_class_rw // sr; move=> [[q qz] [szp allr]].
  exists (P q).
    split; first by move: (szp _ qz); aw; intuition.
  have aux:(forall z0, inc z0 z =
    (inc q (product x y) & inc z0 (product x y) & P q = P z0)).
    by move => z0; move: (allr q z0 qz); rewrite /r first_proj_eq_related.
  set_extens t; rewrite aux; first by aw; intuition.
  have qp: inc q (product x y) by apply szp.
  move => h; split =>//.
  awi h; move : h => [pt [Pt Qt]].
  have: (inc (P t) x) by move: qp; rewrite Pt; aw; intuition.
  by aw.
move=> [u [uz zp]]; rewrite zp; dw.
split; first by move: ney => [a ay]; exists (J u a); fprops.
split; first by rewrite sr; apply product_monotone_left; apply sub_singleton.
move => a b; rewrite first_proj_eq_related.
aw; move=> [pa [Pa Qa]]; apply iff_eq; intuition; ue.
Qed.

Lemma first_proj_equiv_proj: forall x y,
  nonempty y->
  bijection (BL (fun u => product (singleton u) y)
    x (quotient (first_proj_eq x y))).
Proof.
move=> x y ney.
set (f:=fun u => product (singleton u) y).
set (g:= (BL f x (quotient (first_proj_eq x y)))).
have efp:is_equivalence (first_proj_eq x y) by apply first_proj_equivalence.
have ta: transf_axioms f x (quotient (first_proj_eq x y)).
  by move => u ux; rewrite inc_quotient // first_proj_class //; ex_tac.
rewrite /g; apply bl_bijective => //.
  rewrite /f => u v ux vx sp.
  apply singleton_inj; rewrite - (product_domain (singleton u) ney).
  by rewrite sp product_domain.
move=>z; rewrite inc_quotient // first_proj_class //.
by move=> [u [ux ep]]; ex_tac.
Qed.

Partition of a set and induced equivalence

Definition in_same_coset f x y:=
   exists i, inc i (source f) & inc x (W i f) & inc y (W i f).

Definition partition_relation f x :=
  graph_on (in_same_coset f) x.

Lemma isc_reflexive: forall f x, is_function f ->
  partition_fam (graph f) x -> reflexive_r (in_same_coset f) x.
Proof.
move=> f x [fx [ff sf]] pf u.
rewrite /in_same_coset sf.
apply iff_eq => ux.
  by move: (partition_inc_exists pf ux)=> [y [yd uV]]; exists y.
by move: ux pf => [v [vs [Wv _]]] [_ [md]] <-; srw; ex_tac.
Qed.

Lemma isc_symmetric: forall f, symmetric_r (in_same_coset f).
Proof.
rewrite/in_same_coset=> f x y; move => [i [isf [Wx Wy]]]; ex_tac.
Qed.

Lemma partition_inc_unique1: forall f x i j y,
  is_function f -> partition_fam (graph f) x ->
  inc i (source f) -> inc y (W i f) ->
  inc j (source f) -> inc y (W j f) -> i = j.
Proof. move=> f x i j y ff; rewrite -(f_domain_graph ff).
apply partition_inc_unique.
Qed.

Lemma isc_transitive: forall f x, is_function f ->
  partition_fam (graph f) x -> transitive_r (in_same_coset f).
Proof.
move => f x ff pf a b c [i [isf [Wa Wb]]][j [jsf [Wb' Wc]]].
rewrite/in_same_coset.
ex_tac; split =>//.
by rewrite -(partition_inc_unique1 ff pf isf Wb jsf Wb').
Qed.

Lemma isc_equivalence: forall f x, is_function f ->
  partition_fam (graph f) x -> equivalence_re (in_same_coset f) x.
Proof.
move=> f x ff pf.
split; first by split; [ apply isc_symmetric | apply (isc_transitive ff pf) ].
by apply isc_reflexive.
Qed.

Lemma partition_rel_graph: forall f x,
  is_function f ->
  partition_fam (graph f) x ->
  is_graph_of (partition_relation f x) (in_same_coset f).
Proof. rewrite /partition_relation=> f x ff pf.
by apply equivalence_has_graph0; apply isc_equivalence.
Qed.

Lemma partition_relation_pr: forall f x a b,
  is_function f -> partition_fam (graph f) x ->
  related (partition_relation f x) a b = in_same_coset f a b.
Proof.
move=> f x a b ff pf; move: (partition_rel_graph ff pf)=> h.
symmetry; apply h.
Qed.

Lemma partition_is_equivalence: forall f x,
  is_function f -> partition_fam (graph f) x ->
  is_equivalence (partition_relation f x).
Proof.
move=> f x ff pf.
have pg:is_graph (partition_relation f x).
  by rewrite /partition_relation; apply graph_on_graph.
move: (partition_rel_graph ff pf)=> go.
move: (isc_equivalence ff pf)=> [eq _].
apply (equivalence_if_has_graph2 pg go eq).
Qed.

Lemma partition_relation_substrate: forall f x,
  is_function f -> partition_fam (graph f) x ->
  substrate (partition_relation f x)= x.
Proof.
move=> f x ff pf; apply extensionality.
  by rewrite /partition_relation; apply graph_on_substrate.
move: (partition_is_equivalence ff pf)=> eq.
move=> y.
rewrite (isc_reflexive ff pf) - (partition_relation_pr y y ff pf) => tmp.
substr_tac.
Qed.

Lemma partition_class_inc: forall f x a b,
  is_function f -> partition_fam (graph f) x ->
  inc a (class (partition_relation f x) b) =
   (exists i, inc i (source f) & inc b (W i f) & inc a (W i f)).
Proof.
move=> f x a b ff pf.
rewrite -[exists i, _]/(in_same_coset f b a).
rewrite -(partition_relation_pr b a ff pf); bw.
apply (partition_is_equivalence ff pf).
Qed.

Lemma partition_relation_class: forall f x a,
  is_function f -> partition_fam (graph f) x ->
  is_class (partition_relation f x) a
  -> exists u, inc u (source f) & a = W u f.
Proof.
move=> f x a ff pf [eq [rs ac]].
have: related (partition_relation f x) (rep a) (rep a) by equiv_tac.
rewrite (partition_relation_pr (rep a) (rep a) ff pf).
move=> [u [us [ru _]]]; ex_tac.
set_extens t; rewrite ac partition_class_inc //.
  move =>[i [isf [rW tW]]].
  by rewrite (partition_inc_unique1 ff pf us ru isf rW).
move=> h; ex_tac.
Qed.

Lemma partition_relation_class2: forall f x u,
  is_function f -> partition_fam (graph f) x ->
  inc u (source f) -> nonempty (W u f)
  -> is_class (partition_relation f x) (W u f) .
Proof.
move=> f x u ff pf us neW.
move: (partition_is_equivalence ff pf) => ep.
have irW: (inc (rep (W u f)) (W u f)) by apply nonempty_rep.
split =>//.
rewrite partition_relation_substrate //.
have sWx: (sub (W u f) x).
  move: pf=> [_ [_]] <-; move=> t tW.
  by apply unionb_inc with u; [ rewrite f_domain_graph // |].
split; first by apply sWx.
set_extens t; rewrite partition_class_inc //; first by move=> tW; ex_tac.
move => [i [isf [rWW tW]]].
by rewrite (partition_inc_unique1 ff pf us irW isf rWW).
Qed.

Lemma partition_fun_bijective: forall f x,
  is_function f -> partition_fam (graph f) x ->
  (forall u, inc u (source f) -> nonempty (W u f))
  -> bijection (BL (fun u => W u f)
    (source f) (quotient (partition_relation f x))).
Proof.
move=> f x ff pf alne; apply bl_bijective.
    move=> t tf; srw.
    apply partition_relation_class2 =>//; apply (alne _ tf).
    by apply partition_is_equivalence =>//.
  move=> u v us vs sW.
  move: (alne _ us)=> [y yu]; have yv: (inc y (W v f)) by rewrite -sW.
  by apply (partition_inc_unique1 ff pf us yu vs yv).
move=> y; srw ; last by apply partition_is_equivalence.
move=> ic; move: (partition_relation_class ff pf ic) => [u [us]] ->.
ex_tac.
Qed.

Lemma sub_quotient_powerset: forall r,
  is_equivalence r ->
  sub (quotient r) (powerset (substrate r)).
Proof.
move=> r er x; srw; aw; rewrite is_class_rw //; intuition.
Qed.

Lemma partition_from_equivalence: forall r,
  is_equivalence r ->
  partition(quotient r)(substrate r).
Proof.
move=> r er.
split; first by apply union_quotient.
split; first by move=> t tq; apply (non_empty_in_quotient er tq).
move=> a b; srw; apply class_dichot.
Qed.

A system of representatives for the partition f of x as a set f or a function g

Definition representative_system s f x :=
   is_function f & partition_fam (graph f) x & sub s x
  & (forall i, inc i (source f) -> is_singleton (intersection2 (W i f) s)).

Definition representative_system_function g f x :=
  injection g & (representative_system (range (graph g)) f x).

Lemma rep_sys_function_pr: forall g f x i,
  representative_system_function g f x -> inc i (source f)
  -> exists_unique (fun a=> inc a (source g) & inc (W a g) (W i f)).
Proof.
move=> g f x i [ig [ff [pf [sx alsi]]]] ins.
move: (alsi _ ins) => [u isu].
split.
  move: (singleton_inc u).
  rewrite - isu intersection2_rw range_inc_rw; try fct_tac.
  by move=> [uW [a [asg ea]]]; ex_tac; ue.
move=> a b [asg Wa][bsg Wb].
move: ig => [fg ig]; apply ig=>//.
have aux: (forall a, inc a (source g) -> inc (W a g) (W i f) -> W a g = u).
  move=> c csg Wc.
  apply singleton_eq; rewrite -isu; apply intersection2_inc =>//.
  by apply inc_W_range_graph=>//.
rewrite aux // aux //.
Qed.

Lemma rep_sys_function_pr2: forall g f x,
  injection g -> is_function f -> partition_fam (graph f) x -> sub (target g) x
  -> (forall i, inc i (source f)
    -> exists_unique (fun a=> inc a (source g) & inc (W a g) (W i f)))
  -> representative_system_function g f x.
Proof.
move=> g f x ig ff pf stx exu.
split =>//; split=>//; split=>//.
split.
  by apply sub_trans with (target g); [apply f_range_graph; fct_tac|].
move=> i isf; move: (exu _ isf) => [[a [asg Wa]] un].
move:ig=> [fg ig].
have gg: is_graph (graph g) by fprops.
exists (W a g); set_extens t;aw; dw.
  move => [tW [z Jg]]; move: (W_pr fg Jg) =>Wz; rewrite -Wz.
  suff: z = a by move=> <-.
  by apply un; split=>//; try graph_tac; ue.
move => ->; split=>//;by exists a; graph_tac.
Qed.

Lemma section_canon_proj_pr: forall g f x y r,
  r = partition_relation f x -> is_function f -> partition_fam (graph f) x
  -> is_right_inverse g (canon_proj r) ->
  inc y x ->
  related r y (W (class r y) g).
Proof.
move=> g f x y r pr ff pf ri yx.
have eq: is_equivalence r by rewrite pr; apply partition_is_equivalence.
have sr: substrate r = x by rewrite pr partition_relation_substrate //.
rewrite -sr in yx.
have cyq: inc (class r y) (quotient r) by gprops.
have sg: source g = target (canon_proj r) by apply source_right_inverse.
awi sg. rewrite -sg in cyq.
move: ri => [ccg ccpi].
have ryy: related r y y by equiv_tac.
have Wcs: inc (W (class r y) g) (substrate r).
  by move: ccg=> [_ [fg]]; aw; move=>->; apply inc_W_target.
rewrite related_class_eq //; symmetry.
rewrite - canon_proj_W // - compose_W // ccpi.
aw; srw; ue.
Qed.

Lemma section_is_representative_system_function: forall g f x,
  is_function f -> partition_fam (graph f) x
  -> is_right_inverse g (canon_proj (partition_relation f x)) ->
  (forall u, inc u (source f) -> nonempty (W u f)) ->
  representative_system_function g f x.
Proof.
move=> g f x ff pf ti alne.
have ig: injection g by apply (right_inverse_injective ti).
apply rep_sys_function_pr2=>//.
  move: ti => [ [_ [ _ eq]] _]; rewrite- eq; aw.
  by rewrite partition_relation_substrate; fprops.
move=> i isf.
set (r:=partition_relation f x) in *.
have sf: domain (graph f) =source f by apply f_domain_graph.
have er: is_equivalence r by rewrite /r; apply partition_is_equivalence.
have sr: substrate r = x by rewrite /r partition_relation_substrate.
rewrite (source_right_inverse ti).
split.
  set z:= (rep (W i f)).
  have zW: inc z (W i f) by rewrite /z; apply nonempty_rep; apply alne.
  have zx: inc z x by move: pf=>[_ [md]] <-; rewrite -sf in isf; union_tac.
  exists (class r z); split.
    aw; rewrite -sr in zx; gprops.
  move: (section_canon_proj_pr (refl_equal r) ff pf ti zx).
  rewrite partition_relation_pr //; move => [ u [usf [zW' qW]]].
  by rewrite (partition_inc_unique1 ff pf isf zW usf zW').
aw; move=> a b [atx Wa] [btx Wb].
have Wiq: inc (W i f) (quotient r).
  by aw; srw; rewrite /r; apply partition_relation_class2 =>//; by apply alne.
have aux: (forall u, inc u (quotient r) -> inc (W u g) (W i f) ->
    W i f = u).
  move=> u; srw; move=> [_ [rs eq]] iWW; rewrite eq.
  apply is_class_pr=> //.
  rewrite sr in rs.
  move: (section_canon_proj_pr (refl_equal r) ff pf ti rs).
  rewrite -eq.
  rewrite partition_relation_pr //; move => [v [usf [zW' qW]]].
  by rewrite (partition_inc_unique1 ff pf isf iWW usf qW).
by rewrite -(aux _ atx Wa) (aux _ btx Wb).
Qed.

EII-6-3 Relations compatible with an equivalence relation

A relation is compoatible if the set of objectcts satisfying the relation is a union of classes

Definition compatible_with_equiv_p (p: Set -> Prop)(r:Set) :=
forall x x', p x -> related r x x' -> p x'.

Lemma trivial_equiv: forall p x,
compatible_with_equiv_p p (identity_g x).
Proof. move=> p x u v. rewrite/related; aw. by move=> pu [ux] <-.
Qed.

A compatible relation induces a relation on the quotient

Definition relation_on_quotient p r :=
  fun t => inc t (quotient r) & exists x, inc x t & p x.

Lemma rel_on_quo_pr: forall p r t,
  is_equivalence r -> compatible_with_equiv_p p r ->
  relation_on_quotient p r t = (inc t (quotient r) & forall x, inc x t -> p x).
Proof.
move=> p r t er co.
apply iff_eq.
  move=> [tq [x [xt px]]]; split=>//.
  move => u ut; apply (co _ _ px).
  move: tq; srw.
  by rewrite in_class_related //; exists t;intuition.
move => [tq xtpx].
move: (non_empty_in_quotient er tq) => net.
have rtt: (inc (rep t) t) by apply nonempty_rep.
split =>//; ex_tac.
Qed.

Lemma rel_on_quo_pr2: forall p r y,
  is_equivalence r -> compatible_with_equiv_p p r ->
  (inc y (substrate r) & relation_on_quotient p r (W y (canon_proj r))) =
  (inc y (substrate r) & p y).
Proof.
move=> p r y er co; apply iff_eq; move => [ysr ]; aw =>//.
  move=> [tq [x [xt px]]].
  have yx: related r x y by move : xt; bw => xt; equiv_tac.
  by split =>//; apply (co _ _ px yx).
move => py; split =>//; split; gprops.
by exists y; bw; split=>//; equiv_tac.
Qed.

EII-6-4 saturated subsets

A set is satured if it is a union of classes

Definition saturated (r x:Set) := compatible_with_equiv_p (fun y=> inc y x) r.

Lemma saturated_pr: forall r x,
  is_equivalence r -> sub x (substrate r) ->
  (saturated r x) = (forall y, inc y x -> sub (class r y) x).
Proof.
move=> r x er sxs.
apply iff_eq.
  by move=> sr y yx t; bw; apply (sr _ _ yx).
by move=> yw u v ux ruv; apply (yw _ ux); bw.
Qed.

Lemma saturated_pr2: forall r x,
  is_equivalence r -> sub x (substrate r) ->
  (saturated r x) = exists y, (forall z, inc z y -> is_class r z)
    & x = union y.
Proof.
move => r x er sxs.
apply iff_eq.
  move => srx.
  exists (Zo (powerset x)(fun z => exists a, inc a x & z = class r a)).
  split.
    move=> z; rewrite Z_rw; aw; move=> [zx [a[ax]]] ->.
    by apply is_class_class =>//; apply sxs.
  set_extens t => ts.
    apply union_inc with (class r t).
      by move: (sxs _ ts)=>h; bw;equiv_tac.
    apply Z_inc; aw; [move: srx ts; rewrite saturated_pr //; apply | ex_tac].
  move: (union_exists ts ) => [y [ty]]; rewrite Z_rw; aw.
  by move=> [yx [a [ax yc]]]; apply yx.
move => [y [yp xu]]; rewrite saturated_pr // xu=> z zu.
move: (union_exists zu) =>[t [zt ty]].
move:(yp _ ty) => [_ [rs teq]] u; bw => rzu.
rewrite teq in zt; move: zt; bw => rel.
apply (union_sub ty); rewrite teq; bw; equiv_tac.
Qed.

If f is the canonical projection this defines that smallest saturated set that contains x

Definition inverse_direct_value f x :=
  image_by_fun (inverse_fun f) (image_by_fun f x).

Lemma class_is_inv_direct_value: forall r x,
  is_equivalence r -> inc x (substrate r) ->
  class r x = inverse_direct_value (canon_proj r) (singleton x).
Proof.
move=> r x er xs.
rewrite /inverse_direct_value /image_by_fun.
have fc: is_function (canon_proj r) by fprops.
set_extens t => ts.
  aw; exists (class r x); split.
    aw; exists x;split; first by fprops.
    change (inc (J x (class r x)) (graph (canon_proj r))).
    rewrite related_graph_canon_proj; gprops.
    by bw; equiv_tac.
  rewrite/inverse_fun; aw.
  move: (sub_class_substrate er ts)=> tsr.
  have: (class r x = W t (canon_proj r)).
    rewrite canon_proj_W //.
    apply related_class_eq1 =>//.
    by move: ts;bw.
  by move=> ->; graph_tac; aw.
move: ts; aw;move=> [u []]; rewrite/inverse_fun; aw.
move=> [z []]; aw=>-> xJ tJ.
move: (inc_pr1graph_source fc tJ); aw => ts.
move: (W_pr fc xJ) (W_pr fc tJ); aw; move=> -> <-; bw; equiv_tac.
Qed.

Lemma saturated_pr3: forall r x,
  is_equivalence r -> sub x (substrate r) ->
  saturated r x = (x= inverse_direct_value (canon_proj r) x).
Proof.
move=> r x er xs.
set (p:=canon_proj r).
have fp: is_function p by rewrite /p; fprops.
apply iff_eq => h.
  apply extensionality.
    rewrite /inverse_direct_value; apply inverse_direct_image =>//.
    by rewrite /p; aw.
  move => c cx.
  have hyp: (forall u v, inc u (inverse_direct_value p v) =
    inc u (image_by_graph (inverse_graph (graph p))
          (image_by_graph (graph p) v))).
    by rewrite /inverse_direct_value /image_by_fun/inverse_fun; aw.
  have: (exists a, inc a x & inc c (inverse_direct_value p (singleton a))).
    move: cx; rewrite hyp; aw; move=> [u]; rewrite image_by_graph_rw.
    move=> [[v [vx J1p]] J2p]; ex_tac; rewrite hyp; aw; ex_tac.
    by aw; ex_tac; fprops.
  move=> [a [ax ci]].
  rewrite -(class_is_inv_direct_value er (xs _ ax)) in ci.
  move: h; rewrite saturated_pr =>// h.
  by apply (h _ ax).
rewrite saturated_pr =>//.
move => y yx; rewrite h /inverse_direct_value.
have sxs: sub x (source p) by rewrite /p; aw.
have Wi:inc (W y p) (image_by_fun p x) by aw=>//; ex_tac.
move: (class_is_inv_direct_value er (xs _ yx)).
rewrite/inverse_direct_value -/p => ->.
have ys:(inc y (source (canon_proj r))) by aw; apply xs.
rewrite (image_singleton fp ys).
rewrite /image_by_fun; apply image_by_increasing.
by apply sub_singleton.
Qed.

Lemma saturated_pr4: forall r x,
  is_equivalence r -> sub x (substrate r) ->
  saturated r x = (exists b, sub b (quotient r)
    & x = image_by_fun (inverse_fun (canon_proj r)) b).
Proof.
move=> r x er xs.
have qr: quotient r = target (canon_proj r) by aw.
apply iff_eq.
  have fc: is_function (canon_proj r) by fprops.
  rewrite saturated_pr3 // /inverse_direct_value => hyp.
  exists (image_by_fun (canon_proj r) x); split =>//.
  apply sub_trans with (range (graph (canon_proj r))).
    by rewrite/ image_by_fun; apply sub_image_by_graph.
  by rewrite qr; fct_tac.
move=> [b [bq xeq]].
move: (canon_proj_surjective er)=> sj.
rewrite qr in bq; move: (direct_inv_im_surjective sj bq).
rewrite -xeq => eq.
move: (f_equal (image_by_fun (inverse_fun (canon_proj r))) eq).
by rewrite saturated_pr3 // -xeq.
Qed.

Links between saturation and union, intersection, complement

Lemma saturated_union: forall r x,
  is_equivalence r -> (forall y, inc y x -> sub y (substrate r)) ->
  (forall y, inc y x -> saturated r y) ->
  (sub (union x) (substrate r) & saturated r (union x)).
Proof.
move=> r x er als alsa.
have r1: (sub (union x) (substrate r)).
  by move => t tu; move: (union_exists tu) => [z [tz zx]]; apply (als _ zx).
split=>//.
rewrite saturated_pr //.
move=> y yu; move: (union_exists yu) => [z [yz zx]].
move: (alsa _ zx); rewrite saturated_pr // => s.
  apply sub_trans with z; first by apply (s _ yz).
  apply union_sub =>//.
by apply als.
Qed.

Lemma saturated_intersection : forall r x,
  is_equivalence r -> nonempty x ->
  (forall y, inc y x -> sub y (substrate r)) ->
  (forall y, inc y x -> saturated r y) ->
  (sub (intersection x) (substrate r) & saturated r (intersection x)).
Proof.
move=> r x er nex als alsa.
have aux: (sub (intersection x) (substrate r)).
  move: nex => [y yx].
  by apply sub_trans with y =>//; [ apply (intersection_sub yx) | apply als].
split =>//.
rewrite saturated_pr //.
move => y yi t tc; apply intersection_inc =>//.
move=> z zx; move: (als _ zx)=> alsz; move:(alsa _ zx).
rewrite saturated_pr // => s.
apply (s _ (intersection_forall yi zx)) =>//.
Qed.

Lemma saturated_complement : forall r a,
  is_equivalence r -> sub a (substrate r) -> saturated r a ->
  saturated r (complement (substrate r) a).
Proof.
move=> r a er ar.
rewrite saturated_pr4 //saturated_pr4 // ;last by apply sub_complement.
move=> [b [sq aib]]; exists (complement (quotient r) b).
split; first by apply sub_complement.
have fc: is_function (canon_proj r) by fprops.
move :(inv_image_complement b fc) aib.
rewrite /inv_image_by_fun/inverse_fun/image_by_fun/inv_image_by_graph.
by aw; move=> -> <-.
Qed.

Definition saturation_of (r x:Set):=
  inverse_direct_value (canon_proj r) x.

Lemma saturation_of_pr: forall r x,
  is_equivalence r -> sub x (substrate r) ->
  saturation_of r x =
  union (Zo (quotient r)(fun z=> exists i, inc i x & z = class r i)).
Proof.
move=> r x er sr.
have fc: is_function (canon_proj r) by fprops.
rewrite /saturation_of/inverse_direct_value.
set_extens y.
  rewrite /image_by_fun/inverse_fun; aw; move=> [u]; aw.
  move=> [[v [vx J1g]] J2g].
  have vs: inc v (source (canon_proj r)) by graph_tac.
  have ys: inc y (source (canon_proj r)) by graph_tac.
  have: inc u (target (canon_proj r)) by graph_tac.
  move: vs ys; aw => vs ys uq.
  apply union_inc with u.
    by rewrite -(related_graph_canon_proj er (x:=y)(y:=u)).
  apply Z_inc =>//; ex_tac.
  by move:(W_pr fc J1g); rewrite canon_proj_W.
rewrite union_rw; move=> [z [zy]]; rewrite Z_rw; move=> [zq [i [ix zci]]].
rewrite /image_by_fun;aw; exists z;aw; split.
  move: (sr _ ix)=>h; ex_tac; rewrite related_graph_canon_proj //.
  by rewrite zci; bw; equiv_tac.
rewrite/inverse_fun;aw.
rewrite related_graph_canon_proj //.
apply (inc_in_quotient_substrate er zy zq).
Qed.

Lemma saturation_of_smallest: forall r x,
  is_equivalence r -> sub x (substrate r) ->
  (saturated r (saturation_of r x) &
    sub x (saturation_of r x)
    & (forall y, sub y (substrate r) -> saturated r y -> sub x y
      -> sub (saturation_of r x) y)).
Proof.
move=> r x er xsr.
have fc: is_function (canon_proj r) by fprops.
split.
  rewrite saturated_pr4 //.
    exists (image_by_fun (canon_proj r) x); split =>//.
    apply sub_trans with (range (graph (canon_proj r))).
      by apply sub_image_by_graph.
    have Hw:quotient r = target (canon_proj r) by aw.
    by rewrite Hw; apply f_range_graph.
  rewrite /saturation_of/inverse_direct_value /image_by_fun/inverse_fun.
  aw; move=> t; aw; move =>[u]; aw; move=> [[v [vx Jg1]] Jg2].
  by move: (inc_pr1graph_source fc Jg2); aw.
split.
  move => t tx.
  rewrite /saturation_of/inverse_direct_value/image_by_fun; aw.
  move: (xsr _ tx) => ts.
  have h: (inc (J t (class r t)) (graph (canon_proj r))).
    by rewrite related_graph_canon_proj //; bw; [equiv_tac | gprops].
  by exists (class r t); split; [ aw; ex_tac | rewrite/inverse_fun; aw].
move=> y ys.
rewrite/saturation_of; aw; rewrite saturated_pr3 //.
move=> eq sxy; rewrite eq.
rewrite/inverse_direct_value/image_by_fun.
by do 2 apply image_by_increasing.
Qed.

Definition union_image x f:=
  union (Zo x (fun z=> exists i, inc i (source f) & z = W i f)).

Lemma saturation_of_union: forall r f g,
  is_equivalence r -> is_function f -> is_function g ->
  (forall i, inc i (source f) -> sub (W i f) (substrate r)) ->
  source f = source g ->
  (forall i, inc i (source f) -> saturation_of r (W i f) = W i g)
  -> saturation_of r (union_image (powerset(substrate r)) f) =
  union_image (powerset(substrate r)) g.
Proof.
move=>r f g er ff fg als sfsg alsat.
have fc: is_function (canon_proj r) by fprops.
rewrite/saturation_of/inverse_direct_value/union_image/image_by_fun.
rewrite /saturation_of/inverse_direct_value/image_by_fun in alsat.
set_extens x.
  aw; move=> [y]; aw; move=> [[z [zu Jg1]] Jg2].
  move: zu; srw; move=> [t [zt ]]; rewrite Z_rw; aw; move=> [tr [i [isf tw]]].
  exists (W i g); rewrite Z_rw; rewrite -sfsg; aw.
  split.
    by rewrite -(alsat _ isf) -tw; aw; exists y; split=>//; aw; exists z.
  split; last by ex_tac.
  rewrite -(alsat _ isf)=> u; aw; move=> [v [_]].
  by rewrite/inverse_fun; aw=> tmp; move: (inc_pr1graph_source fc tmp); aw.
srw; move=> [y [xy]]; rewrite Z_rw; aw; move=> [yr [i [isg yW]]].
rewrite -sfsg in isg.
move: xy; rewrite yW -(alsat _ isg); aw; move=> [u [p1 p2]].
exists u; split=>//.
move: p1;aw; move=> [v [vW ig]]; ex_tac.
apply union_inc with (W i f) =>//.
apply Z_inc; last by ex_tac.
by aw; apply als.
Qed.

EII-6-5 Mappings compatible with equivalence relations

The canonical projection is surjective, thus has a section

Definition section_canon_proj (r:Set) :=
  BL rep (quotient r) (substrate r).

Lemma section_canon_proj_axioms:forall r,
  is_equivalence r ->
  transf_axioms rep (quotient r) (substrate r).
Proof. move=> r er t ta; fprops.
Qed.

Lemma section_canon_proj_W: forall r x,
  is_equivalence r ->
  inc x (quotient r) -> W x (section_canon_proj r) = (rep x).
Proof.
rewrite/section_canon_proj=> r x er iq; aw.
by apply section_canon_proj_axioms.
Qed.

Lemma section_canon_proj_function: forall r,
  is_equivalence r -> is_function (section_canon_proj r).
Proof.
rewrite/section_canon_proj=> r er.
by apply bl_function; apply section_canon_proj_axioms.
Qed.

Lemma right_inv_canon_proj: forall r,
  is_equivalence r ->
  is_right_inverse (section_canon_proj r) (canon_proj r).
Proof.
move=> r er.
have ss: source (section_canon_proj r) = quotient r.
  by rewrite/section_canon_proj; aw.
have fs: is_function (section_canon_proj r) by apply section_canon_proj_function.
have fc: is_function (canon_proj r) by fprops.
have cpo: (canon_proj r) \coP (section_canon_proj r).
  by hnf; intuition; rewrite/ section_canon_proj; aw.
split=> //.
apply function_exten; try fct_tac; fprops; aw.
rewrite ss=> x xs.
have aux: (W x (section_canon_proj r)) = rep x.
  by rewrite section_canon_proj_W //.
aw; try ue.
rewrite identity_W // aux; apply class_rep =>//.
Qed.

A mapping is compatible with an equivalence if it is constant on classes; it is compatible with two equivalences is the image of a class is a subset of a class

Definition compatible_with_equiv f r :=
  is_function f & source f = substrate r &
  forall x x', related r x x' -> W x f = W x' f.

Definition compatible_with_equivs f r r' :=
  is_function f & target f = substrate r' &
  compatible_with_equiv (compose (canon_proj r') f) r.

Lemma compatible_with_equiv_pr: forall f r,
  is_function f -> source f = substrate r ->
  compatible_with_equiv f r =
  (forall y, compatible_with_equiv_p (fun x => y = W x f) r).
Proof.
move=> f r ff sf; rewrite/compatible_with_equiv/compatible_with_equiv_p.
apply iff_eq.
  by move=> [_ [_ hyp]] y x x' =>->; apply hyp.
by move=> hyp; intuition; apply (hyp (W x f) x x').
Qed.

Lemma compatible_constant_on_classes: forall f r x y,
  is_equivalence r ->
  compatible_with_equiv f r -> inc y (class r x) -> W x f = W y f.
Proof. move=> f r x y eq [ff [sf hyp]] yc.
by apply hyp; move: yc; bw.
Qed.

Lemma compatible_constant_on_classes2: forall f r x,
  is_equivalence r -> compatible_with_equiv f r ->
  is_constant_function(restriction f (class r x)).
Proof.
move=> f r x re [ff [sf hyp]].
have scs: sub (class r x) (substrate r) by apply sub_class_substrate.
rewrite - sf in scs.
split; first by apply restriction_function.
have sr: source (restriction f (class r x)) = class r x.
  by rewrite /restriction; aw.
rewrite sr.
move=> a b ac bc.
do 2 rewrite restriction_W //.
move: ac bc; bw=> ac bc.
apply hyp; equiv_tac.
Qed.

Lemma compatible_with_proj: forall f r x y,
  is_equivalence r -> compatible_with_equiv f r ->
  inc x (substrate r) -> inc y (substrate r) ->
  W x (canon_proj r) = W y (canon_proj r) -> W x f = W y f.
Proof.
move=> f r x y er cgt xs ys; aw => sx.
apply compatible_constant_on_classes with r=>//.
by rewrite sx; bw; equiv_tac.
Qed.

Lemma compatible_with_pr:forall r r' f x y,
  is_equivalence r -> is_equivalence r' ->
  compatible_with_equivs f r r' ->
  related r x y -> related r' (W x f) (W y f).
Proof.
move=> r r' f x y er er' [ff [sf [fc [sc hyp]] ]] rxy.
have cc: (composable (canon_proj r') f).
   by split; first (by fprops); split=>//; aw.
awi sc.
have xs: inc x (source f) by rewrite sc; substr_tac.
have ys: inc y (source f) by rewrite sc; substr_tac.
have px: (inc (W x f) (substrate r')) by rewrite -sf; apply inc_W_target.
have py: (inc (W y f) (substrate r')) by rewrite -sf; apply inc_W_target.
move: (hyp _ _ rxy); aw =>//.
by rewrite related_rw //.
Qed.

Lemma compatible_with_pr2:forall r r' f,
  is_equivalence r -> is_equivalence r' ->
  is_function f ->
  target f = substrate r'-> source f = substrate r->
  (forall x y, related r x y -> related r' (W x f) (W y f)) ->
  compatible_with_equivs f r r'.
Proof.
move=> r r' f er er' ff tf sf rr'.
have cc: composable (canon_proj r') f by hnf; intuition; symmetry; aw.
split =>//; split=>//; split; first by fct_tac.
split; first by aw.
move=> x x' rxx'; move: (rr' _ _ rxx'); rewrite related_rw //.
move => [Ws [Ws' cxx']]; aw; rewrite sf; substr_tac.
Qed.

Lemma compatible_with_proj3 :forall r r' f x y,
  is_equivalence r -> is_equivalence r' ->
  compatible_with_equivs f r r'->
  inc x (substrate r) -> inc y (substrate r) ->
  W x (canon_proj r) = W y (canon_proj r) ->
  class r' (W x f) = class r' (W y f).
Proof.
move=> r r' f x y er er' co xs ys; aw.
rewrite - related_class_eq //; try equiv_tac; move=> cxy.
apply related_class_eq1 =>//.
apply (compatible_with_pr er er' co cxy).
Qed.

A compatible mapping induces a mapping on the quotient

Definition fun_on_quotient r f :=
  f \co (section_canon_proj r).

Lemma exists_fun_on_quotient: forall f r,
  is_equivalence r -> is_function f -> source f = substrate r ->
  compatible_with_equiv f r =
  (exists h, h \coP (canon_proj r) & h \co (canon_proj r) = f).
Proof.
move=> f r er ff sf.
rewrite exists_left_composable; aw; try apply canon_proj_surjective=>//.
apply iff_eq.
  by move => co x y xs ys sW; apply (compatible_with_proj er co xs ys sW).
move=> hyp; split=>//; split=>//.
move=> x x'; rewrite related_rw //; move=> [xs [ys cc]].
apply hyp; aw.
Qed.

Lemma exists_unique_fun_on_quotient: forall f r h,
  is_equivalence r -> compatible_with_equiv f r ->
  h \coP (canon_proj r) -> h \co (canon_proj r) = f ->
  h = fun_on_quotient r f.
Proof.
move=> f r h er cfr chc chcf.
have sc: (surjection (canon_proj r)) by apply canon_proj_surjective.
move: (right_inv_canon_proj er) => ri.
have ff: is_function f by move: cfr=> [].
have sf: source f = source (canon_proj r) by aw; move: cfr=> [ _[]].
apply (exists_left_composable_aux ff sf ri chc chcf).
Qed.

Lemma compose_foq_proj :forall f r,
  is_equivalence r -> compatible_with_equiv f r ->
  (fun_on_quotient r f) \co (canon_proj r) = f.
Proof.
move=> f r er co; move: (co)=> [ff[sf hyp]].
set (g:= canon_proj r).
have sg: surjection g by rewrite/g; apply canon_proj_surjective.
have sfsg: source f = source g by rewrite /g; aw.
have sW: forall x y, inc x (source g) -> inc y (source g) ->
      W x g = W y g -> W x f = W y f.
  rewrite -sfsg sf; move=> x y xr yr h.
  by apply (compatible_with_proj er co xr yr).
apply (left_composable_value ff sg sfsg sW (right_inv_canon_proj er)
    (refl_equal (fun_on_quotient r f))).
Qed.

A mappoing compatible with two relations induces a mapping on the two quotients

Definition fun_on_rep f: Set -> Set := fun x=> f(rep x).
Definition fun_on_reps r' f := fun x=> W (f(rep x)) (canon_proj r').

Definition function_on_quotient r f b :=
  BL(fun_on_rep f)(quotient r)(b).

Definition function_on_quotients r r' f :=
  BL(fun_on_reps r' f)(quotient r)(quotient r').

Definition fun_on_quotients r r' f :=
  ((canon_proj r') \co f) \co (section_canon_proj r).

Lemma foq_axioms: forall r f b,
  is_equivalence r ->
  transf_axioms f (substrate r) b ->
  transf_axioms (fun_on_rep f) (quotient r) b.
Proof.
rewrite /transf_axioms=> r f b er h x xs.
rewrite/fun_on_rep; apply h; fprops.
Qed.

Lemma foqs_axioms: forall r r' f,
  is_equivalence r ->
  is_equivalence r' ->
  transf_axioms f (substrate r)(substrate r') ->
  transf_axioms (fun_on_reps r' f) (quotient r) (quotient r').
Proof.
rewrite /transf_axioms=> r r' f er er' h x xs.
rewrite/fun_on_reps.
have w: (inc (rep x) (substrate r)) by fprops.
aw; gprops.
Qed.

Lemma foqc_axioms: forall r f,
  is_equivalence r ->
  is_function f -> source f = substrate r ->
  f \coP (section_canon_proj r).
Proof.
move=> r f er ff sf.
split =>//; split; first by apply section_canon_proj_function.
rewrite /section_canon_proj; aw.
Qed.

Lemma foqcs_axioms:forall r r' f,
  is_equivalence r ->
  is_equivalence r' ->
  is_function f -> source f = substrate r -> target f = substrate r' ->
  (canon_proj r' \co f) \coP (section_canon_proj r).
Proof.
move=> r r' f er er' ff sf tf.
have fc: (is_function (canon_proj r')) by fprops.
split; first by fct_tac => //; symmetry; aw.
split; first by apply section_canon_proj_function.
rewrite/section_canon_proj; aw.
Qed.

Lemma foq_function:forall r f b,
  is_equivalence r ->
  transf_axioms f (substrate r) b ->
  is_function (function_on_quotient r f b).
Proof.
by rewrite /function_on_quotient=> *; apply bl_function; apply foq_axioms.
Qed.

Lemma foqs_function: forall r r' f,
  is_equivalence r ->
  is_equivalence r' ->
  transf_axioms f (substrate r)(substrate r') ->
  is_function (function_on_quotients r r' f).
Proof.
by rewrite /function_on_quotients=> *;apply bl_function; apply foqs_axioms.
Qed.

Lemma foqc_function:forall r f,
  is_equivalence r -> is_function f ->
  source f = substrate r ->
  is_function (fun_on_quotient r f).
Proof.
rewrite/fun_on_quotient=> r f er ff sf; fct_tac.
  by apply section_canon_proj_function.
by rewrite /section_canon_proj; aw.
Qed.

Lemma foqcs_function:forall r r' f,
  is_equivalence r ->
  is_equivalence r' ->
  is_function f -> source f = substrate r -> target f = substrate r' ->
  is_function (fun_on_quotients r r' f).
Proof.
rewrite/fun_on_quotients=> r r' f er er' ff sf tf.
by apply compose_function; apply foqcs_axioms.
Qed.

Lemma foq_W:forall r f b x,
  is_equivalence r ->
  transf_axioms f (substrate r) b ->
  inc x (quotient r) ->
  W x (function_on_quotient r f b) = f (rep x).
Proof.
by rewrite /function_on_quotient=> r f b x er ta xq; aw; apply foq_axioms.
Qed.

Lemma foqc_W:forall r f x,
  is_equivalence r -> is_function f ->
  source f = substrate r -> inc x (quotient r) ->
  W x (fun_on_quotient r f) = W (rep x) f.
Proof.
rewrite/fun_on_quotient=> r f x er ff sf xq; aw.
    by rewrite section_canon_proj_W.
  by apply foqc_axioms.
by rewrite /section_canon_proj; aw.
Qed.

Lemma foqs_W: forall r r' f x,
  is_equivalence r ->
  is_equivalence r' ->
  transf_axioms f (substrate r)(substrate r') ->
  inc x (quotient r) ->
  W x (function_on_quotients r r' f) = class r' (f (rep x)).
Proof.
rewrite /function_on_quotients=> r r' f x er er' ta xq; aw.
  rewrite /fun_on_reps; aw.
  by apply ta; fprops.
by apply foqs_axioms.
Qed.

Lemma foqcs_W:forall r r' f x,
  is_equivalence r ->
  is_equivalence r' ->
  is_function f -> source f = substrate r -> target f = substrate r' ->
  inc x (quotient r) ->
  W x (fun_on_quotients r r' f) = class r' (W (rep x) f).
Proof.
move=> r r' f x er er' ff sf tf xq.
rewrite /fun_on_quotients.
have fs: is_function(section_canon_proj r) by apply section_canon_proj_function.
have ccf: (canon_proj r') \coP f by hnf;intuition; symmetry;aw.
have cc2: ( (canon_proj r') \co f) \coP (section_canon_proj r).
  by split; first (by fct_tac); split=>//; rewrite /section_canon_proj; aw.
have Wt: inc (W x (section_canon_proj r)) (target (section_canon_proj r)).
  by apply inc_W_target=>//; rewrite /section_canon_proj; aw.
have irs: inc (rep x) (source f) by ue.
rewrite compose_W //; last by rewrite/section_canon_proj; aw.
rewrite section_canon_proj_W // /section_canon_proj.
aw; rewrite -tf; apply inc_W_target =>//.
Qed.

Lemma fun_on_quotient_pr: forall r f x,
  W x f = fun_on_rep (fun w => W x f) (W x (canon_proj r)).
Proof. trivial.
Qed.

Lemma fun_on_quotient_pr2: forall r r' f x,
  W (W x f) (canon_proj r') =
  fun_on_reps r' (fun w => W x f) (W x (canon_proj r)).
Proof. trivial.
Qed.

Lemma composable_fun_proj: forall r f b,
  is_equivalence r ->
  transf_axioms f (substrate r) b ->
  (function_on_quotient r f b) \coP (canon_proj r).
Proof.
move=> r f b er ta.
split; first by apply foq_function.
split; fprops; rewrite/function_on_quotient; aw.
Qed.

Lemma composable_fun_projs: forall r r' f,
  is_equivalence r ->
  is_equivalence r' ->
  transf_axioms f (substrate r) (substrate r') ->
  (function_on_quotients r r' f) \coP (canon_proj r).
Proof.
move=> r r' f er er' ta.
split; first by apply foqs_function.
split; fprops; rewrite/function_on_quotients; aw.
Qed.

Lemma composable_fun_projc: forall r f,
  is_equivalence r ->
  compatible_with_equiv f r ->
  (fun_on_quotient r f) \coP (canon_proj r).
Proof.
move=> r f er [ff [sf h]].
split; first by apply foqc_function.
split; fprops; rewrite/fun_on_quotient/section_canon_proj; aw.
Qed.

Lemma composable_fun_projcs: forall r r' f,
  is_equivalence r -> is_equivalence r' ->
  compatible_with_equivs f r r'->
  (fun_on_quotients r r' f) \coP (canon_proj r).
Proof.
move=> r r' f er er' [ff [sf [fg [sg h]]]].
split; first by awi sg; apply foqcs_function.
split; fprops; rewrite/fun_on_quotients/section_canon_proj; aw.
Qed.

Lemma fun_on_quotient_pr3: forall r f x,
  is_equivalence r -> inc x (substrate r) ->
  compatible_with_equiv f r ->
  W x f = W (W x (canon_proj r)) (fun_on_quotient r f).
Proof.
move=> r f x er xs co; rewrite - compose_W; last by aw.
  by rewrite compose_foq_proj.
by apply composable_fun_projc.
Qed.

Figure 3 (French version only)

Lemma fun_on_quotient_pr4: forall r r' f,
  is_equivalence r -> is_equivalence r' ->
  compatible_with_equivs f r r'->
  (canon_proj r') \co f = (fun_on_quotients r r' f) \co (canon_proj r).
Proof.
rewrite/fun_on_quotients; move=> r r' f er er' [ff [sf h]].
symmetry. apply (compose_foq_proj er h).
Qed.

Lemma fun_on_quotient_pr5: forall r r' f x,
  is_equivalence r -> is_equivalence r' ->
  compatible_with_equivs f r r'->
  inc x (substrate r) ->
  W (W x f) (canon_proj r') =
  W (W x (canon_proj r)) (fun_on_quotients r r' f).
Proof.
move => r r' f x er er' co xs.
move: (co)=> [ff [sf [fg [sg h]]]]; awi sg.
have cc: composable (canon_proj r') f by hnf; intuition; symmetry; aw.
rewrite - compose_W //; try ue.
rewrite - compose_W //; last by aw.
  by rewrite -fun_on_quotient_pr4 //.
by apply composable_fun_projcs=>//.
Qed.

Lemma compose_fun_proj_ev: forall r f b x,
  is_equivalence r ->
  compatible_with_equiv (BL f (substrate r) b) r ->
  inc x (substrate r) ->
  transf_axioms f (substrate r) b ->
  W x (function_on_quotient r f b \co canon_proj r) = f x.
Proof.
move=> r f b x er co xr ta.
have cq: (inc (class r x) (quotient r)) by gprops.
aw; try apply composable_fun_proj =>//; last by aw.
have rrx: related r (rep (class r x)) x.
  by apply symmetricity_e=>//; apply related_rep_class=>//.
rewrite foq_W //.
by move: co=> [_ [_ h]]; move: (h _ _ rrx); aw; fprops.
Qed.

Lemma compose_fun_proj_ev2: forall r r' f x,
  is_equivalence r ->
  is_equivalence r' ->
  compatible_with_equivs (BL f (substrate r) (substrate r')) r r' ->
  transf_axioms f (substrate r) (substrate r') ->
  inc x (substrate r) ->
  inc (f x) (substrate r') ->
  W (f x) (canon_proj r') =
  W x (function_on_quotients r r' f \co canon_proj r).
Proof.
move=> r r' f x er er' co ta xs fxs.
aw; try apply composable_fun_projs =>//; last by aw.
set (y:= (W x (canon_proj r))).
have : (W y (function_on_quotients r r' f)
    = (W y (fun_on_quotients r r' (BL f (substrate r) (substrate r'))))).
  have ys: inc y (quotient r) by rewrite /y; aw; gprops.
  rewrite foqs_W // foqcs_W //; aw.
    by apply inc_rep_substrate =>//.
  by apply bl_function.
rewrite - fun_on_quotient_pr5 // /y; aw.
by move => ->.
Qed.

Lemma compose_fun_proj_eq: forall r f b,
  is_equivalence r ->
  compatible_with_equiv (BL f (substrate r) b) r ->
  transf_axioms f (substrate r) b ->
  (function_on_quotient r f b) \co (canon_proj r) =
    BL f (substrate r) b.
Proof.
move=> r f b er co ta.
apply function_exten; try solve [ rewrite/function_on_quotient; aw].
    apply compose_function.
    apply composable_fun_proj=>//.
  apply bl_function =>//.
rewrite /function_on_quotient; aw.
by move =>x xs; rewrite compose_fun_proj_ev=>//; aw.
Qed.

Lemma compose_fun_proj_eq2: forall r r' f,
  is_equivalence r ->
  is_equivalence r' ->
  transf_axioms f (substrate r) (substrate r') ->
  compatible_with_equivs (BL f (substrate r) (substrate r')) r r'->
  (function_on_quotients r r' f) \co (canon_proj r) =
  (canon_proj r') \co (BL f (substrate r) (substrate r')).
Proof.
move=> r r' f er er' ta co.
have ffoq:is_function (function_on_quotients r r' f) by apply foqs_function.
have fa: is_function (BL f (substrate r) (substrate r')) by apply bl_function.
have cn: (function_on_quotients r r' f) \coP (canon_proj r).
  by hnf; intuition; rewrite/ function_on_quotients; aw.
have cc: (canon_proj r') \coP (BL f (substrate r) (substrate r')).
  by hnf; intuition; aw.
apply function_exten; try fct_tac; aw.
  rewrite /function_on_quotients; aw.
move => x xs.
have aux: (inc (f x) (substrate r')) by apply ta.
rewrite -compose_fun_proj_ev2 //; aw.
Qed.

Lemma compatible_ea: forall f,
  is_function f ->
  compatible_with_equiv f (equivalence_associated f).
Proof.
move=> f ff.
split=>//; split; first by rewrite graph_ea_substrate.
by move=> x x';rewrite ea_related //; intuition.
Qed.

Lemma ea_foq_injective: forall f,
  is_function f ->
  injection (fun_on_quotient (equivalence_associated f) f).
Proof.
move=> f ff.
set (g:= equivalence_associated f).
have eg: is_equivalence g by rewrite /g; apply graph_ea_equivalence.
have sf:source f = substrate g by rewrite /g graph_ea_substrate.
split; first by apply foqc_function.
have: source (fun_on_quotient g f) = (quotient g)
  by rewrite/fun_on_quotient/section_canon_proj; aw.
move => -> x y xq yq.
rewrite foqc_W // foqc_W // => h.
move: (inc_rep_substrate eg xq) (inc_rep_substrate eg yq) => xs ys.
have: (related g (rep x) (rep y)) by rewrite /g ea_related // sf; intuition.
by rewrite related_rep_rep.
Qed.

Lemma ea_foq_on_im_bijective: forall f,
  is_function f ->
  bijection (restriction2 (fun_on_quotient (equivalence_associated f) f)
    (quotient (equivalence_associated f)) (range (graph f))).
Proof.
move=> f ff.
set (g:= equivalence_associated f).
set (h:= fun_on_quotient g f).
have eg: is_equivalence g by rewrite /g; apply graph_ea_equivalence.
have sfsg : source f = substrate g by rewrite /g graph_ea_substrate.
have ih: injection h by rewrite /h/g; apply ea_foq_injective.
have fh: is_function h by fct_tac.
have qg: quotient g = source h.
   by rewrite /h/fun_on_quotient/section_canon_proj; aw.
have rg: range (graph f) = image_by_fun h (source h).
  rewrite /h; set_extens t.
    aw;dw; fprops.
    move=> [x Jg].
    have xsf: (inc x (source f)) by graph_tac.
    rewrite sfsg in xsf.
    have gxq: inc (class g x) (quotient g) by gprops.
    exists (class g x); split; [ ue | rewrite foqc_W // ].
    rewrite - (W_pr ff Jg).
    have : (related g x (rep (class g x))) by apply related_rep_class.
    rewrite (ea_related x (rep (class g x)) ff).
    by symmetry; intuition.
  dw; aw; fprops; move=> [u [us]].
  have uq: (inc u (quotient g)).
    by move:us; rewrite /fun_on_quotient /section_canon_proj; aw.
  rewrite foqc_W //; move => <-.
  by exists (rep u); graph_tac; rewrite sfsg; apply inc_rep_substrate.
rewrite rg qg restriction1_pr //.
apply restriction1_bijective; fprops.
Qed.

Canonical decomposition of a function as a surjection, a bijection and an ionjection

Lemma canonical_decompositiona: forall f,
  is_function f ->
  let r:= equivalence_associated f in
    is_function ((restriction2 (fun_on_quotient r f)
      (quotient r) (range (graph f)))
     \co (canon_proj r)).
Proof.
move=> f ff r.
set (g:= canon_proj r).
set (a:=range (graph f)).
set (j:=canonical_injection a (target f)).
set (k:=restriction2 (fun_on_quotient r f) (quotient r) a).
have er: is_equivalence r by rewrite /r; apply graph_ea_equivalence.
have sr: source f = substrate r by rewrite /r graph_ea_substrate.
have sat: sub a (target f) by rewrite /a; apply f_range_graph.
have fj: is_function j by rewrite /j; apply ci_function.
have ffo: is_function (fun_on_quotient r f) by apply foqc_function.
have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) a.
  split=>//.
  split; first by rewrite/fun_on_quotient/section_canon_proj; aw.
  split; first by rewrite/fun_on_quotient/section_canon_proj; aw.
  rewrite /image_by_fun; move=> x; aw; move=> [y [yq Jg]].
  rewrite -(W_pr ffo Jg) /a range_inc_rw //.
  exists (rep y).
  by rewrite sr; split;fprops; rewrite foqc_W.
have fk:is_function k by rewrite /k; apply restriction2_function.
have ckg: k \coP g.
  rewrite /k/g; split; first by apply restriction2_function.
  by split; fprops; rewrite /restriction2;aw.
fct_tac.
Qed.

Lemma canonical_decomposition: forall f,
  is_function f ->
  let r:= equivalence_associated f in
  f = (canonical_injection (range (graph f))(target f))
      \co (restriction2 (fun_on_quotient r f) (quotient r) (range (graph f))
           \co (canon_proj r)).
Proof.
move=> f ff r.
set (g:= canon_proj r).
set (a:=range (graph f)).
set (j:=canonical_injection a (target f)).
set (k:=restriction2 (fun_on_quotient r f) (quotient r) a).
have er: is_equivalence r by rewrite/r; apply graph_ea_equivalence.
have sr: source f = substrate r by rewrite /r graph_ea_substrate.
have sat: sub a (target f) by rewrite /a ; apply f_range_graph.
have fj:is_function j by rewrite /j;apply ci_function.
have foq: is_function (fun_on_quotient r f) by apply foqc_function.
have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) a.
  split=>//.
  split; first by rewrite/fun_on_quotient/section_canon_proj; aw.
  split; first by rewrite/fun_on_quotient/section_canon_proj; aw.
  rewrite /image_by_fun; move=> x; aw; move=> [y [yq Jg]].
  rewrite -(W_pr foq Jg) /a range_inc_rw //.
  exists (rep y).
  by rewrite sr; split;fprops; rewrite foqc_W.
have fk:is_function k by rewrite /k; apply restriction2_function.
have ckg:k \coP g.
  rewrite /k/g; split; first by apply restriction2_function.
  by split; fprops; rewrite /restriction2;aw.
have sfg: source f = source g by rewrite /g; aw.
have fkg: is_function (compose k g) by fct_tac.
have cjkg: j \coP (k \co g).
  by hnf; intuition; rewrite/j/k/canonical_injection/restriction2; aw.
apply function_exten=>//; try fct_tac; aw.
  by rewrite/j/canonical_injection; aw.
move=> x xsf.
  move: (xsf); rewrite sr=> xsr; rewrite sfg in xsf.
  have a1: (quotient r = target g) by rewrite /g;aw.
  have W1q: inc (W x g) (quotient r).
    by rewrite a1;apply inc_W_target =>//; fct_tac.
  have p1: inc (W (W x g) k) a.
    have: (a = target k) by rewrite/k/restriction2; aw.
    by move=> ->; apply inc_W_target =>//; rewrite /k/restriction2; aw; ue.
aw.
rewrite /j ci_W // /k restriction2_W // foqc_W // /g; aw.
have rxr: (related r x (rep (class r x))) by apply related_rep_class.
rewrite (ea_related x (rep (class r x)) ff) in rxr.
intuition.
Qed.

Lemma surjective_pr7: forall f,
  surjection f ->
  canonical_injection (range (graph f))(target f) = identity (target f).
Proof.
move=> f sf. rewrite surjective_pr3 //.
Qed.

Lemma canonical_decomposition_surj: forall f,
  surjection f ->
  let r:= equivalence_associated f in
  f = (restriction2 (fun_on_quotient r f) (quotient r) (target f))
       \co (canon_proj r).
Proof.
move=> f sf r.
move: (surjective_pr7 sf) (surjective_pr3 sf) => p1 p2.
move: sf => [sf _].
move: (canonical_decomposition sf); simpl; rewrite p1 p2; fold r.
set (g:= (restriction2 (fun_on_quotient r f) (quotient r) (target f))).
set (h:= g \co (canon_proj r)).
move=> ->.
have: (target f = target h) by rewrite /h/g/restriction2; aw.
move =>->.
apply compose_id_left.
by rewrite /h/g/r -p2; apply canonical_decompositiona.
Qed.

Lemma canonical_decompositionb: forall f,
  is_function f ->
  let r:= equivalence_associated f in
    restriction2 (fun_on_quotient r f) (quotient r) (target f) =
    (fun_on_quotient r f).
Proof.
move=> f ff r.
set (k:=restriction2 (fun_on_quotient r f) (quotient r) (target f)).
have er: is_equivalence r by rewrite /r; apply graph_ea_equivalence.
have sf: source f = substrate r by rewrite /r graph_ea_substrate.
have ffoq: is_function (fun_on_quotient r f) by apply foqc_function.
have ra: restriction2_axioms (fun_on_quotient r f) (quotient r) (target f).
  split=>//.
  split; first by rewrite/fun_on_quotient/section_canon_proj; aw.
  split; first by rewrite/fun_on_quotient/section_canon_proj; aw.
  rewrite /image_by_fun; move=> x; aw; move=> [y [yq Jg]].
  rewrite -(W_pr ffoq Jg) .
  rewrite foqc_W //; apply inc_W_target =>//; rewrite sf; fprops.
have fk: is_function k by rewrite /k; apply restriction2_function.
have sk: source k = quotient r by rewrite /k/restriction2; aw.
apply function_exten =>//; rewrite/k.
     rewrite /restriction2/fun_on_quotient/section_canon_proj; aw.
  by rewrite/restriction2/fun_on_quotient; aw.
move=> x; rewrite sk => xq; rewrite restriction2_W //.
Qed.

Lemma canonical_decomposition_surj2: forall f,
  surjection f ->
  let r:= equivalence_associated f in
  f = (fun_on_quotient r f) \co (canon_proj r).
Proof.
move=> f sf r; move: (canonical_decomposition_surj sf).
move: sf => [ff _]; move: (canonical_decompositionb ff).
by simpl; move => -> <-.
Qed.

EII-6-6 Inverse image of an equivalence relation; induced equivalence relation

We have an equivalence on the source induced by the equivalence on the target

Definition inv_image_relation f r :=
  equivalence_associated (canon_proj r \co f).

Definition iirel_axioms f r :=
  is_function f & is_equivalence r & substrate r = target f.

Lemma iirel_function: forall f r,
   iirel_axioms f r -> is_function (canon_proj r \co f).
Proof.
move=> f r [ff [er tf]]; fct_tac; [ fprops | aw].
Qed.

Lemma iirel_relation: forall f r,
  iirel_axioms f r -> is_equivalence (inv_image_relation f r).
Proof.
move=> f r ia; rewrite /inv_image_relation.
by apply graph_ea_equivalence; apply iirel_function.
Qed.

Lemma iirel_substrate: forall f r,
  iirel_axioms f r -> substrate (inv_image_relation f r) = source f.
Proof.
move=> f fr ia; rewrite /inv_image_relation graph_ea_substrate; aw.
by apply iirel_function.
Qed.

Lemma iirel_related: forall f r x y,
  iirel_axioms f r ->
  related (inv_image_relation f r) x y =
  (inc x (source f) & inc y (source f) & related r (W x f) (W y f)).
Proof.
move=> f r x y ia.
have fc : is_function (compose (canon_proj r) f) by apply iirel_function.
move: ia => [ff [er tf]].
rewrite /inv_image_relation.
have cct: (composable (canon_proj r) f).
  by hnf; intuition; aw; rewrite ea_related.
have iWs: forall u, inc u (source f) -> inc (W u f) (substrate r).
  by move=> u; rewrite tf; fprops.
rewrite ea_related // compose_source.
apply iff_eq; move => [xs [ys h]]; move: (iWs _ xs) (iWs _ ys)=> p1 p2;
  split=>//; split =>//.
  by move: h; aw; rewrite related_class_eq //; equiv_tac.
by aw; apply related_class_eq1.
Qed.

Lemma iirel_class: forall f r x,
  iirel_axioms f r ->
  is_class (inv_image_relation f r) x =
  exists y, is_class r y
    & nonempty (intersection2 y (range (graph f)))
    & x = inv_image_by_fun f y.
Proof.
move=> f r x ia; move: (ia) => [ff [er tf]].
apply iff_eq.
  rewrite is_class_rw; last by apply iirel_relation.
  rewrite iirel_substrate //; move => [[y yx] [xf p]].
  have iWs: inc (W y f) (substrate r) by rewrite tf; move: (xf _ yx); fprops.
  exists (class r (W y f)).
  split; first by apply is_class_class.
  split.
    exists (W y f); apply intersection2_inc; first by bw; equiv_tac.
    by dw; fprops; exists y; graph_tac.
  set_extens x0; rewrite /inv_image_by_fun (p y x0 yx).
    rewrite iirel_related //; move=> [ysf [x0sf ryx0]].
    aw; exists (W x0 f); bw; split=>//; graph_tac.
  aw; move=> [u [uc Jg]].
  rewrite iirel_related //; split; first by apply xf.
  split; [ graph_tac | rewrite (W_pr ff Jg); move: uc; bw ].

move=> [y [cy [[u ui]] xi]].
move: ui; aw; rewrite range_inc_rw; fprops.
move=> [uy [v [vsf uw]]].
have sx: sub x (source f).
  by rewrite xi /inv_image_by_fun; move => t; aw; move=> [w [_ wg]]; graph_tac.
rewrite is_class_rw //; last by apply iirel_relation.
split.
  exists v; rewrite xi /inv_image_by_fun; aw;ex_tac; rewrite uw; graph_tac.
split; first by rewrite iirel_substrate //.
move=> w z wx.
rewrite iirel_related //; apply iff_eq.
  move=> zx; split; first (by apply sx); split; first by apply sx.
  move: wx; rewrite xi/inv_image_by_fun; aw.
  move=> [w' [w'y Jg1]]; rewrite (W_pr ff Jg1).
  move: zx; rewrite xi/inv_image_by_fun; aw.
  move=> [z' [z'y Jg2]]; rewrite (W_pr ff Jg2).
  by rewrite in_class_related //; exists y.
move=> [xs [zs rwz]].
move: wx; rewrite xi/inv_image_by_fun; aw.
move=> [w' [w'y Jg1]]; rewrite (W_pr ff Jg1) in rwz.
exists (W z f).
split; last by graph_tac.
move: cy; rewrite is_class_rw //; move=> [ney [yr hyp]].
by rewrite (hyp _ (W z f) w'y) .
Qed.

Equivalence induced on a subset of the substrate

Definition induced_relation (r a:Set) :=
  inv_image_relation (canonical_injection a (substrate r)) r.

Definition induced_rel_axioms(r a :Set) :=
   is_equivalence r & sub a (substrate r).

Lemma induced_rel_iirel_axioms : forall r a,
  induced_rel_axioms r a ->
  iirel_axioms (canonical_injection a (substrate r)) r.
Proof.
move=> r a [er ar]; hnf; intuition; fprops.
rewrite/canonical_injection; aw.
Qed.

Lemma induced_rel_equivalence: forall r a,
  induced_rel_axioms r a -> is_equivalence (induced_relation r a).
Proof.
rewrite /induced_relation=> r a ia;
by apply iirel_relation; apply induced_rel_iirel_axioms.
Qed.

Lemma induced_rel_substrate: forall r a,
  induced_rel_axioms r a -> substrate (induced_relation r a) = a.
Proof.
move=> r a ia; rewrite /induced_relation iirel_substrate.
  rewrite/canonical_injection; aw.
by apply induced_rel_iirel_axioms.
Qed.

Lemma induced_rel_related: forall r a u v,
  induced_rel_axioms r a ->
  related (induced_relation r a) u v =
  (inc u a & inc v a & related r u v).
Proof.
move=> r a u v ia.
move: (induced_rel_iirel_axioms ia) => iia.
move: ia=> [er ar].
rewrite/induced_relation iirel_related //.
have: source (canonical_injection a (substrate r)) = a.
  by rewrite /canonical_injection; aw.
move=> ->.
apply iff_eq; move=> [ua [va h]];
  split=>//; split=>// ; move: h; rewrite ci_W //ci_W //.
Qed.

Lemma induced_rel_class: forall r a x,
  induced_rel_axioms r a ->
  is_class (induced_relation r a) x =
  exists y, is_class r y
    & nonempty (intersection2 y a)
    & x = (intersection2 y a).
Proof.
move=> r a x ia.
move: (induced_rel_iirel_axioms ia) => iia.
rewrite/induced_relation iirel_class //.
move: ia=> [er ar].
rewrite ci_range /inv_image_by_fun /canonical_injection; aw.
have p: (forall y,inv_image_by_graph (identity_g a) y = intersection2 y a).
  move=> y;set_extens t; aw.
    move=> [u [uy]]; rewrite inc_pair_diagonal.
    move=> [ta eq]; split=>//; ue.
  by move=> [ty ta]; ex_tac; rewrite inc_pair_diagonal.
apply iff_eq; move=> [y [cy [p1 p2]]]; exists y; split=>//;split=>//.
  by rewrite -p.
by rewrite p.
Qed.

Lemma compatible_injection_induced_rel: forall r a,
  induced_rel_axioms r a ->
  compatible_with_equivs (canonical_injection a (substrate r))
  (induced_relation r a) r.
Proof.
move=> r a ia; move: (ia)=> [er sa].
apply compatible_with_pr2 =>//.
        by apply induced_rel_equivalence.
      by apply ci_function.
    rewrite/canonical_injection; aw.
  by rewrite/canonical_injection;aw; rewrite induced_rel_substrate.
move=> x y; rewrite induced_rel_related //; move => [xa [ya rxy]].
rewrite ci_W // ci_W //.
Qed.

Lemma foq_induced_rel_injective: forall r a,
  induced_rel_axioms r a ->
  injection (fun_on_quotients (induced_relation r a) r
    (canonical_injection a (substrate r))).
Proof.
move=> r a ia; move: (ia)=> [er sa].
set (f := (canonical_injection a (substrate r))).
move: (induced_rel_equivalence ia) =>ei.
have ff: is_function f by rewrite /f;apply ci_function.
have tf: target f = substrate r by rewrite /f /canonical_injection; aw.
have sf: source f = substrate (induced_relation r a).
  rewrite /f induced_rel_substrate // /canonical_injection; aw.
split; first by apply foqcs_function.
have : (source (fun_on_quotients (induced_relation r a) r f) =
    quotient (induced_relation r a) ).
  rewrite/fun_on_quotients /section_canon_proj; aw.
move=>->.
move=> x y xs ys; rewrite foqcs_W // foqcs_W //.
have eq: a = substrate (induced_relation r a) by rewrite induced_rel_substrate.
have rxa: inc (rep x) a by rewrite eq; fprops.
have rya: inc (rep y) a by rewrite eq; fprops.
rewrite ci_W // ci_W // => cc.
have: (related (induced_relation r a) (rep x) (rep y)).
  rewrite induced_rel_related //; intuition.
  by rewrite related_rw //; intuition; apply sa.
by rewrite related_rep_rep.
Qed.

Lemma foq_induced_rel_image: forall r a,
  induced_rel_axioms r a ->
  image_by_fun (fun_on_quotients (induced_relation r a) r
    (canonical_injection a (substrate r))) (quotient (induced_relation r a))
  = image_by_fun (canon_proj r) a.
Proof.
move=> r a ia; move: (ia)=> [er sa].
rewrite/image_by_fun.
set (ci := canonical_injection a (substrate r)).
have fci: is_function ci by rewrite /ci; apply ci_function.
have sci: source ci = substrate (induced_relation r a).
   by rewrite induced_rel_substrate /ci /canonical_injection; aw.
set (f:= fun_on_quotients (induced_relation r a) r ci).
move: (foq_induced_rel_injective ia).
rewrite -/ci -/f; move => inf.
have ff: is_function f by fct_tac.
have ei: is_equivalence (induced_relation r a) by apply induced_rel_equivalence.
have gf: is_graph (graph f) by fprops.
have tci: target ci = substrate r by rewrite /ci/canonical_injection; aw.
have fc: is_function (canon_proj r) by fprops.
set_extens x.
  aw; move=> [y [yq Jg]].
  move: (yq); srw; rewrite induced_rel_class //; move=> [z [cz [nei yi]]].
  move: (W_pr ff Jg); rewrite foqcs_W //.
  move => cx.
  have: (inc (rep y) (intersection2 z a)).
    by rewrite -yi; apply nonempty_rep; rewrite yi.
  aw; move=> [ryz rya]; rewrite ci_W // in cx.
  move: nei=> [u ]; aw;move=>[uz ua]; exists u; split=>//.
  have ryu: (related r (rep y) u) by rewrite in_class_related //; exists z.
  move: (sa _ ua) => us.
  have: x = W u (canon_proj r) by aw; rewrite -cx; apply related_class_eq1=> //.
  by move=>->; graph_tac; aw.

aw; move=> [y [ya Jg]]; move: (sa _ ya)=> yu.
move: (W_pr fc Jg); aw; move => cx.
have yx: (inc y x) by rewrite -cx; bw; equiv_tac.
set (z:= intersection2 x a).
have ney: nonempty z by rewrite /z; exists y; apply intersection2_inc.
have zq: inc z (quotient (induced_relation r a)).
  srw; rewrite induced_rel_class //; exists x.
  by intuition; rewrite -cx; apply is_class_class =>//.
ex_tac.
have: (inc (rep z) (intersection2 x a)) by rewrite /z; apply nonempty_rep.
aw; move => [rzx rza].
have ryr: (related r y (rep z)).
  rewrite in_class_related //; exists x.
  split; [ rewrite -cx; apply is_class_class =>// | auto].
have Wi: x = W (intersection2 x a) f.
  rewrite /f foqcs_W// ci_W // -/z -cx.
  by rewrite related_rw in ryr; intuition.
rewrite Wi; fold z; graph_tac.
rewrite/f/fun_on_quotients/section_canon_proj; aw.
Qed.

Definition canonical_foq_induced_rel r a :=
  restriction2 (fun_on_quotients (induced_relation r a) r
    (canonical_injection a (substrate r)))
  (quotient (induced_relation r a))
  (image_by_fun (canon_proj r) a).

Lemma canonical_foq_induced_rel_bijective: forall r a,
  induced_rel_axioms r a -> bijection (canonical_foq_induced_rel r a).
Proof.
move=> r a ia.
set ci:= (canonical_injection a (substrate r)).
have sf: source
    (fun_on_quotients (induced_relation r a) r
      ci) = quotient (induced_relation r a).
  rewrite /fun_on_quotients/section_canon_proj; aw.
have ra:restriction2_axioms
     (fun_on_quotients (induced_relation r a) r ci)
     (quotient (induced_relation r a)) (image_by_fun (canon_proj r) a).
  move: (foq_induced_rel_injective ia) => ifoq.
  split; first by fct_tac.
  split; first by rewrite /fun_on_quotients/section_canon_proj; aw.
  split.
    rewrite /fun_on_quotients; aw; move=> t ts; move: ia=> [er ar].
    by apply (sub_im_canon_proj_quotient er ar ts).
  by rewrite foq_induced_rel_image; fprops.
rewrite /canonical_foq_induced_rel.
split.
  by apply restriction2_injective=>//; apply foq_induced_rel_injective.
apply restriction2_surjective=>//.
rewrite/fun_on_quotients/section_canon_proj.
rewrite - foq_induced_rel_image // /image_of_fun; aw.
Qed.

EII-6-7 Quotients of equivalence relations

Definition of a finer equivalence

Definition finer_equivalence (s r:Set):=
  forall x y, related s x y -> related r x y.

Definition finer_axioms(s r:Set):=
  is_equivalence s &
  is_equivalence r &
  substrate r = substrate s.

Lemma finer_sub_equiv: forall s r,
  finer_axioms s r ->
  (finer_equivalence s r) = (sub s r).
Proof.
move=> s r [es [er srss]].
apply iff_eq.
  move=> fe t ts.
  have gs: (is_graph s) by fprops.
  by rewrite -(gs _ ts); apply fe; red; rewrite (gs _ ts).
move => t x y; rewrite /related; apply t.
Qed.

Lemma finer_sub_equiv2: forall s r,
  finer_axioms s r ->
  (finer_equivalence s r) =
  (forall x, exists y, sub(class s x)(class r y)).
Proof.
move=> s r [es [er srss]].
apply iff_eq.
  by move=> fsr x; exists x; move=> u; bw; apply fsr.
move=> h x y rxy.
move:(h x)=> [z sxz].
have xs: inc x (substrate s) by substr_tac.
have ixc: inc x (class s x) by bw; equiv_tac.
have ys: inc y (class s x) by bw.
move: (sxz _ ixc)(sxz _ ys); bw; move => r1 r2; equiv_tac.
Qed.

Lemma finer_sub_equiv3: forall s r,
  finer_axioms s r ->
  (finer_equivalence s r) =
  (forall y, saturated s (class r y)).
Proof.
move=> s r fa; move: (fa)=>[es [er srss]].
apply iff_eq.
  move=> fe y.
  rewrite saturated_pr //; last by rewrite -srss; apply sub_class_substrate.
  move => z zc; rewrite finer_sub_equiv2 // in fe.
  move: (fe z)=> [x cxy].
  have zs: (inc z (substrate s)) by rewrite -srss; move: zc; bw=> q; substr_tac.
  have zcx: (inc z (class r x)) by apply cxy; bw; equiv_tac.
  move: zc zcx; bw; move => p1 p2.
  have p3: related r z y by equiv_tac.
  have p4: related r x y by equiv_tac.
  suff: (class r x = class r y) by move=> <-.
  rewrite - related_class_eq //.
  have aa: (inc x (substrate r)) by substr_tac.
  by equiv_tac.
move=> p x y re; move: (p x).
rewrite saturated_pr //; last by rewrite -srss; apply sub_class_substrate.
move => h.
have p1: inc x (substrate s) by substr_tac.
have p2: inc x (class r x) by bw; rewrite -srss in p1; equiv_tac.
have p3: inc y (class s x) by bw.
by move:((h _ p2) _ p3); bw.
Qed.

Lemma finest_equivalence: forall r,
   is_equivalence r -> finer_equivalence (identity_g (substrate r)) r.
Proof. by move=> r er x t; rewrite /related; aw; move=> [xs] <-; equiv_tac.
Qed.

Lemma coarsest_equivalence: forall r,
   is_equivalence r -> finer_equivalence r (coarse (substrate r)).
Proof. move=> r er x y;rewrite coarse_related // related_rw; intuition.
Qed.

Lemma compatible_with_finer: forall s r,
  finer_axioms s r ->
  finer_equivalence s r ->
  compatible_with_equiv (canon_proj r) s.
Proof.
move=> s r [es [er fh]] fe.
split; fprops; split;aw => x y rxy.
move: (fe _ _ rxy); rewrite related_rw //; move => [p1 [p2 h]]; aw.
Qed.

Lemma foq_finer_function: forall s r,
  finer_axioms s r ->
  finer_equivalence s r -> is_function(fun_on_quotient s (canon_proj r)).
Proof.
move=> s r [es [er fh]] fe; apply foqc_function; fprops; aw.
Qed.

Lemma foq_finer_W: forall s r x,
  finer_axioms s r -> finer_equivalence s r -> inc x (quotient s) ->
  W x (fun_on_quotient s (canon_proj r)) = class r (rep x).
Proof.
move=> s r x [es [er fh]] fe xq; rewrite foqc_W //; aw; fprops.
rewrite fh; fprops.
Qed.

Lemma foq_finer_surjective: forall s r,
  finer_axioms s r ->
  finer_equivalence s r -> surjection(fun_on_quotient s (canon_proj r)).
Proof.
move=> s r fa fe.
apply surjective_pr6; first by apply foq_finer_function.
move: fa=> [es [er ss]] y yt.
have yq:inc y (quotient r) by move:yt; rewrite/fun_on_quotient; aw.
have rys:(inc (rep y) (substrate r)) by fprops.
have sfo:source (fun_on_quotient s (canon_proj r)) = (quotient s).
  by rewrite /fun_on_quotient/section_canon_proj; aw.
set(x := class s (rep y)).
have xq: (inc x (quotient s))by rewrite /x; rewrite ss in rys; gprops.
rewrite sfo; ex_tac.
rewrite foq_finer_W //.
have cry: (class r (rep y) = y) by apply class_rep=>//.
rewrite -cry; apply related_class_eq1 =>//;apply fe.
move: xq; rewrite inc_quotient // is_class_rw //.
move=> [ny [sxs hh]]; rewrite - hh; last by apply nonempty_rep.
by rewrite /x; bw; rewrite ss in rys; equiv_tac.
Qed.

Quotient of a relation by a finer one

Definition quotient_of_relations (r s:Set):=
  equivalence_associated (fun_on_quotient s (canon_proj r)).

Lemma quotient_of_relations_equivalence:
  forall r s, finer_axioms s r -> finer_equivalence s r ->
    is_equivalence (quotient_of_relations r s).
Proof.
rewrite/quotient_of_relations=> r s fa fe.
apply graph_ea_equivalence.
move: (foq_finer_surjective fa fe)=> inj; fct_tac.
Qed.

Lemma quotient_of_relations_substrate:
  forall r s, finer_axioms s r -> finer_equivalence s r ->
    substrate (quotient_of_relations r s) = (quotient s).
Proof.
move=> r s fa fe.
rewrite /quotient_of_relations graph_ea_substrate //.
  rewrite/fun_on_quotient/section_canon_proj; aw.
apply(surj_is_function (foq_finer_surjective fa fe)).
Qed.

Lemma quotient_of_relations_related: forall r s x y,
  finer_axioms s r -> finer_equivalence s r ->
  related (quotient_of_relations r s) x y =
  (inc x (quotient s) & inc y (quotient s) &
    related r (rep x) (rep y)).
Proof.
move=>r s x y fa fe.
have foq: is_function (fun_on_quotient s (canon_proj r)).
  by apply(surj_is_function (foq_finer_surjective fa fe)).
rewrite/quotient_of_relations ea_related //.
move: fa =>[es [er ss]].
have fc: is_function (canon_proj r) by fprops.
have: source (fun_on_quotient s (canon_proj r)) = quotient s.
  rewrite /fun_on_quotient/section_canon_proj; aw.
move=>->.
have sc:source (canon_proj r) = substrate s by aw.
apply iff_eq; move => [xq [yq h]]; split=>//; split=>//.
  have p1: (inc (rep x) (substrate r)) by rewrite ss; fprops.
  have p2: (inc (rep y) (substrate r)) by rewrite ss; fprops.
  move: h; rewrite foqc_W // foqc_W //; aw.
  rewrite related_rw //; intuition.
have p1: (inc (rep x) (substrate r)) by rewrite ss; fprops.
have p2: (inc (rep y) (substrate r)) by rewrite ss; fprops.
rewrite foqc_W // foqc_W //; aw.
by rewrite related_rw in h; intuition.
Qed.

Lemma quotient_of_relations_related_bis: forall r s x y,
  finer_axioms s r -> finer_equivalence s r ->
  inc x (substrate s) -> inc y (substrate s) ->
  related (quotient_of_relations r s) (class s x) (class s y)
  = related r x y.
Proof.
move=> r s x y fa fe xs ys.
rewrite quotient_of_relations_related //.
move: fa =>[es [er ss]].
have p1:(related r x (rep (class s x))) by apply fe; apply related_rep_class.
have p2:(related r y (rep (class s y))) by apply fe; apply related_rep_class.
apply iff_eq.
  move=> [ixs [iys rxy]].
  apply transitivity_e with (rep (class s x)) =>//.
  apply transitivity_e with (rep (class s y)) =>//.
  equiv_tac.
move=> h; split; gprops; split; gprops.
apply transitivity_e with x=>//.
apply symmetricity_e=>//.
equiv_tac.
Qed.

Lemma nonempty_image: forall f x,
  is_function f -> nonempty x -> sub x (source f) ->
  nonempty (image_by_fun f x).
Proof.
move=> f x ff [z zx] xf.
exists (W z f); rewrite/image_by_fun; aw; ex_tac; graph_tac.
Qed.

Lemma cqr_aux: forall s x y u,
  is_equivalence s -> sub y (substrate s) ->
  x = image_by_fun (canon_proj s) y ->
  inc u x = (exists v, inc v y & u = class s v).
Proof.
move=> s x y u es ys xi.
apply iff_eq.
  rewrite xi /image_by_fun => ui.
  move:(sub_im_canon_proj_quotient es ys ui) => uqs.
  move: ui; aw; move=> [z [zy Jg]]; move : (ys _ zy) => zs.
  rewrite related_graph_canon_proj // in Jg.
  ex_tac.
  have aux: (class s (rep u) = u) by (apply class_rep).
  have ruz: related s (rep u) z by rewrite - inc_class // aux.
  rewrite related_rw // in ruz.
  rewrite -aux; intuition.
have fc: is_function (canon_proj s) by fprops.
move=> [v [vy ]]->; move: (ys _ vy) => vs; rewrite xi /image_by_fun.
aw; ex_tac; rewrite related_graph_canon_proj //.
  apply inc_itself_class =>//.
by srw; apply is_class_class.
Qed.

Lemma quotient_of_relations_class_bis: forall r s x,
  finer_axioms s r -> finer_equivalence s r ->
  inc x (quotient (quotient_of_relations r s)) =
  exists y, inc y (quotient r) & x = image_by_fun (canon_proj s) y.
Proof.
move=> r s x fa fe.
move: (quotient_of_relations_equivalence fa fe)=> eq.
move: (fa) =>[es [er ss]].
have fc: is_function (canon_proj s) by fprops.
srw; apply iff_eq. rewrite is_class_rw //.
  rewrite quotient_of_relations_substrate //.
  move=> [ne [sxq hyp]].
  set(y:= Zo (substrate r) (fun v => exists u, inc u x & inc v u)).
  have ney: (nonempty y).
    move :ne=> [u ux].
    have uq: (inc u (quotient s)) by apply sxq.
    move: (inc_rep_itself es uq)=> ru.
    by exists (rep u); rewrite /y ss Z_rw; split =>//; fprops; ex_tac.
  have ys: sub y (substrate r) by rewrite/y ss; apply Z_sub.
  exists y; split.
    srw; rewrite is_class_rw //; split=>//; split=>//.
    move=> a b; rewrite /y Z_rw Z_rw.
    move=> [asr [u [ux au]]].
    apply iff_eq.
      move =>[bsr [v [vx bv]]].
      move: vx; rewrite (hyp u v ux) quotient_of_relations_related //.
      move => [uq [vq ruv]].
      apply transitivity_e with (rep u)=>//.
        apply fe.
        rewrite in_class_related //.
        exists u; move: uq; srw; intuition.
        by apply nonempty_rep; ex_tac.
      apply transitivity_e with (rep v) =>//.
      apply fe.
      rewrite in_class_related //.
      exists v; move: vq; srw; intuition.
      by apply nonempty_rep; ex_tac.
    move=> rab.
    move: (inc_arg2_substrate rab) => bsr.
    move: rab.
    rewrite -(quotient_of_relations_related_bis (r:=r) (s:=s)) //; try ue.
    rewrite -hyp.
      move => cbr;split=>//; exists (class s b); split =>//.
      by apply inc_itself_class=> //; ue.
    have uq: (inc u (quotient s)) by apply sxq.
    by rewrite - (is_class_pr es au uq).
  set (xx := image_by_fun (canon_proj s) y).

  rewrite ss in ys.
  set_extens u; rewrite (cqr_aux u es ys (refl_equal xx)).
    move => ux.
    have yq: (inc u (quotient s)) by apply sxq.
    move: (inc_rep_itself es yq) => ur.
    exists (rep u); split.
      rewrite /y; apply Z_inc; first (by rewrite ss; fprops); ex_tac.
    by symmetry; apply class_rep.
  move=> [v [vy]] ->.
  move: vy; rewrite /y Z_rw; move=> [vr [w [wx vw]]].
  have wq: (inc w (quotient s)) by apply sxq.
  move: (related_rep_in_class es wq vw).
  rewrite related_rw //; move=> [rws [vd]].
  by move: (class_rep es wq) => -> <-.

move=> [y []].
rewrite inc_quotient // is_class_rw //.
move=> [[u uy] [ysr hyp]] xd; move: (ysr); rewrite ss=> yss.
have us: (inc u (substrate s)) by apply yss.
rewrite is_class_rw //.
split; first by rewrite xd; apply nonempty_image=>//; [ ex_tac| aw ].
split.
  rewrite xd quotient_of_relations_substrate //.
  by move=> z zi; apply (sub_im_canon_proj_quotient es yss zi).
move=> a b.
rewrite (cqr_aux a es yss xd) (cqr_aux b es yss xd).
move=> [v [vy asv]].
apply iff_eq.
  move=> [w [wy asw]].
  rewrite asv asw quotient_of_relations_related_bis //; try ue.
  by rewrite -(hyp v w vy).
rewrite quotient_of_relations_related //.
move=> [aq [bq rab]].
exists (rep b); split.
  rewrite (hyp v (rep b) vy).
  apply transitivity_e with (rep a)=>//.
    apply fe; rewrite in_class_related //.
    exists a;split;first by rewrite asv; apply is_class_class =>//; apply yss.
    rewrite asv; split; first by apply inc_itself_class =>//; apply yss.
  rewrite -asv;apply nonempty_rep; apply(non_empty_in_quotient es aq).
by symmetry; apply class_rep.
Qed.

Lemma quotient_canonical_decomposition: forall r s,
  let f := fun_on_quotient s (canon_proj r) in
    let qr := quotient_of_relations r s in
  finer_axioms s r -> finer_equivalence s r ->
  f = (fun_on_quotient qr f) \co (canon_proj qr).
Proof.
move=> r s f qr fa fe.
have sj: (surjection f) by rewrite /f;apply foq_finer_surjective.
apply (canonical_decomposition_surj2 sj).
Qed.

Lemma quotient_of_relations_pr: forall s t,
  let r := inv_image_relation (canon_proj s) t in
  is_equivalence s -> is_equivalence t -> substrate t = quotient s ->
  t = quotient_of_relations r s.
Proof.
move=>s t r es et st.
have iaa: iirel_axioms (canon_proj s) t.
  by split;fprops; split=>//; aw.
have er: is_equivalence r by rewrite /r; apply iirel_relation.
have fa:finer_axioms s r.
  by split=>//; split =>//; rewrite /r iirel_substrate //; aw.
have fe: finer_equivalence s r.
  move => x y sxy; rewrite /r iirel_related //.
  have xs: inc x (substrate s) by substr_tac.
  have ys: inc y (substrate s) by substr_tac.
  aw;split=>//; split=>//.
  have scxy: (class s x =class s y).
   by rewrite -related_class_eq //; equiv_tac.
  rewrite scxy; apply reflexivity_e=>//.
  by rewrite st; gprops.
have eq: (is_equivalence (quotient_of_relations r s)).
  apply quotient_of_relations_equivalence=> //.
rewrite graph_exten; fprops.
move=> u v; rewrite quotient_of_relations_related //.
apply iff_eq.
  move=> tuv.
  have us: (inc u (quotient s)) by rewrite -st; substr_tac.
  have vs: (inc v (quotient s)) by rewrite -st; substr_tac.
  have rus: (inc (rep u) (substrate s)) by fprops.
  have rvs: (inc (rep v) (substrate s)) by fprops.
  split=>//; split=>//; rewrite iirel_related//.
  by aw; split=>//; split=>//; rewrite class_rep // class_rep.
move=> [uq [vq]]; rewrite iirel_related// ;rewrite canon_proj_source.
move=> [ru [rv]].
aw; rewrite class_rep // class_rep //.
Qed.

EII-6-8 Product of two equivalence relations

Definition substrate_for_prod(r r':Set) :=
  product(substrate r)(substrate r').

Definition prod_of_relation(r r':Set):=
  Zo(product(substrate_for_prod r r')(substrate_for_prod r r'))
  (fun y=> inc (J(P (P y))(P (Q y))) r & inc (J(Q (P y))(Q (Q y))) r').

Lemma prod_of_rel_is_rel: forall r r', is_graph (prod_of_relation r r').
Proof.
move=> r r' t; rewrite/prod_of_relation Z_rw; aw; intuition.
Qed.

Lemma substrate_prod_of_rel1:
  forall r r',
    sub (substrate (prod_of_relation r r'))(substrate_for_prod r r').
Proof.
move=> r r' x.
have g: is_graph (prod_of_relation r r') by apply prod_of_rel_is_rel.
rewrite (inc_substrate_rw x g).
rewrite/prod_of_relation.
case; move=> [y]; rewrite Z_rw; aw; intuition.
Qed.

Lemma prod_of_rel_pr: forall r r' a b,
  related (prod_of_relation r r') a b =
  ( is_pair a & is_pair b & related r (P a) (P b) & related r' (Q a) (Q b)).
Proof.
move=> r r' a b.
apply iff_eq; rewrite /prod_of_relation /related Z_rw /substrate_for_prod; aw.
  intuition.
move=> [pa [pnb [Jar Jbr]]]; intuition; substr_tac.
Qed.

Lemma substrate_prod_of_rel2:
  forall r r', is_symmetric r -> is_symmetric r' ->
    substrate (prod_of_relation r r') = substrate_for_prod r r'.
Proof.
move=> r r' sr sr'.
apply extensionality; first by apply substrate_prod_of_rel1.
move=> x; rewrite {1} /substrate_for_prod; aw.
set r'':=prod_of_relation r r'.
move: sr sr'=> [gr sr][gr' sr'].
move=> [px [ pxs qxs]].
have [u p1]: (exists u, inc (J (P x) u) r).
  move: pxs; rewrite (inc_substrate_rw (P x) gr); case => //.
  by move=> [y]; exists y;apply sr.
have [v p2]: (exists u, inc (J (Q x) u) r').
  move: qxs; rewrite (inc_substrate_rw (Q x) gr'); case => //.
  by move=> [y]; exists y;apply sr'.
have rr: related r'' x (J u v) by rewrite /r'' -px prod_of_rel_pr; aw; fprops.
substr_tac.
Qed.

Lemma prod_of_rel_refl:
  forall r r', is_reflexive r -> is_reflexive r' ->
   is_reflexive (prod_of_relation r r').
Proof.
move=> r r' rr rr'.
split; first by apply prod_of_rel_is_rel.
move=> y ys.
have: inc y (substrate_for_prod r r') by apply substrate_prod_of_rel1.
rewrite /substrate_for_prod; aw; move => [py [yp yq]].
rewrite prod_of_rel_pr.
move:rr rr'=> [_ rr][_ rr'].
intuition.
Qed.

Lemma prod_of_rel_sym:
  forall r r', is_symmetric r -> is_symmetric r' ->
   is_symmetric (prod_of_relation r r').
Proof.
move=> r r' sr sr'.
split; first by apply prod_of_rel_is_rel.
move=> x y. rewrite 2! prod_of_rel_pr.
move:sr sr'=> [_ sr][_ sr'].
intuition.
Qed.

Lemma prod_of_rel_trans:
  forall r r', is_transitive r -> is_transitive r' ->
   is_transitive (prod_of_relation r r').
Proof.
move=> r r' tr tr'.
split; first by apply prod_of_rel_is_rel.
move=> x y z. rewrite 3! prod_of_rel_pr.
move:tr tr'=> [_ tr][_ tr'].
move=> [px [py [rxy rxy']]][_ [pz [ryz ryz']]].
intuition.
  apply (tr _ _ _ rxy ryz).
apply (tr' _ _ _ rxy' ryz').
Qed.

Lemma substrate_prod_of_rel: forall r r',
  is_equivalence r ->is_equivalence r' ->
  substrate (prod_of_relation r r') = product(substrate r)(substrate r').
Proof.
move=>r r' [_[_ sr]] [_[_ sr']].
apply (substrate_prod_of_rel2 sr sr').
Qed.

Lemma equivalence_prod_of_rel: forall r r',
  is_equivalence r -> is_equivalence r' ->
  is_equivalence (prod_of_relation r r').
Proof.
move=> r r' [rr [tr sr]] [rr' [tr' sr']].
split; first by apply prod_of_rel_refl.
by split; [apply prod_of_rel_trans |apply prod_of_rel_sym].
Qed.

Lemma related_prod_of_rel1: forall r r' x x' v,
  is_equivalence r -> is_equivalence r' ->
  inc x (substrate r) -> inc x' (substrate r') ->
  related (prod_of_relation r r') (J x x') v =
  (exists y, exists y', v = J y y' & related r x y & related r' x' y').
Proof.
move=> r r' x x' v er er' xs xs'.
rewrite prod_of_rel_pr.
apply iff_eq ;aw.
  aw; move=> [_ [pv [r1 r2]]].
  by exists (P v); exists (Q v); intuition; symmetry; aw.
move=> [y [y' [eq [r1 r2]]]]; rewrite eq; aw; fprops.
Qed.

Lemma related_prod_of_rel2: forall r r' x x' v,
  is_equivalence r -> is_equivalence r' ->
  inc x (substrate r) -> inc x' (substrate r') ->
  related (prod_of_relation r r') (J x x') v =
  inc v (product (im_singleton r x) (im_singleton r' x')).
Proof.
move=> r r' x x' v er er' xs xs'.
rewrite related_prod_of_rel1 //; aw.
apply iff_eq.
  move=> [y [y' [eq [r1 r2]]]]; rewrite eq; aw; fprops.
move => [pv [Jr Jr']].
exists (P v); exists (Q v); aw; auto.
Qed.

Lemma class_prod_of_rel2: forall r r' x,
  is_equivalence r -> is_equivalence r' ->
  is_class (prod_of_relation r r') x =
  exists u, exists v, is_class r u & is_class r' v & x = product u v.
Proof.
move=> r r' x er er'.
move:(equivalence_prod_of_rel er er')=> er''.
apply iff_eq.
  rewrite is_class_rw //; move => [[y yx] [sxs hyp]].
  move: sxs; rewrite substrate_prod_of_rel // => sxs.
  have: inc y (product (substrate r) (substrate r')) by apply sxs.
  aw; move=> [yp [py qy]].
  exists (class r (P y)); exists (class r' (Q y)).
  intuition; try apply is_class_class =>//.
  set_extens v.
    rewrite (hyp y v yx) prod_of_rel_pr; move=> [_ [pv [r1 r2]]].
    by aw; split=> //; split; bw.
  aw; move=> [pv [r1 r2]]; rewrite (hyp y v yx).
  rewrite prod_of_rel_pr; split=>//; split=>//.
  by rewrite - inc_class // - inc_class //.
move=> [u [v [c1 []]]]; move:c1.
do 3!rewrite is_class_rw //.
move=> [[u1 u1u] [sur hyp1]][[v1 v1v] [svr hyp2]] eq.
rewrite eq.
split; first by exists (J u1 v1); fprops.
rewrite substrate_prod_of_rel //.
split; first by apply product_monotone.
move=> y z. aw. rewrite prod_of_rel_pr.
move=> [yp [py qy]] ; apply iff_eq.
  move=> [zp [pz qz]]; intuition; [ by rewrite -hyp1| by rewrite - hyp2].
move=> [_ [pz [ ]]]; rewrite -hyp1 // - hyp2 //.
Qed.

Lemma ext_to_prod_rel_function: forall r r',
  is_equivalence r -> is_equivalence r' ->
  is_function (ext_to_prod(canon_proj r)(canon_proj r')).
Proof. move=> r r' er er'; apply ext_to_prod_function; fprops.
Qed.

Lemma ext_to_prod_rel_W: forall r r' x x',
  is_equivalence r -> is_equivalence r' ->
  inc x (substrate r) -> inc x' (substrate r') ->
  W (J x x') (ext_to_prod(canon_proj r)(canon_proj r')) =
  J (class r x) (class r' x').
Proof.
move=> r r' x x' er er' xs xs'.
rewrite ext_to_prod_W; fprops; aw.
Qed.

Lemma compatible_ext_to_prod: forall r r',
  is_equivalence r -> is_equivalence r' ->
   compatible_with_equiv (ext_to_prod (canon_proj r) (canon_proj r'))
     (prod_of_relation r r').
Proof.
move=> r r' er er'.
have fc: is_function (canon_proj r) by fprops.
have fc': is_function (canon_proj r') by fprops.
split; first by apply ext_to_prod_function.
split; first by rewrite substrate_prod_of_rel // /ext_to_prod; aw.
move=> x x'.
rewrite prod_of_rel_pr; move=> [px [px' []]].
rewrite related_rw // related_rw //; move=> [pxs [qx cx]][pys [qy cy]].
have q1: (J (P x)(Q x) = x) by aw.
have q2: (J (P x')(Q x') = x') by aw.
rewrite -q1 ext_to_prod_W //; aw.
rewrite -q2 ext_to_prod_W //; aw.
by rewrite cx cy.
Qed.

Lemma compatible_ext_to_prod_inv: forall r r' x x',
  is_equivalence r -> is_equivalence r' ->
  is_pair x -> inc (P x) (substrate r) -> inc (Q x) (substrate r') ->
  is_pair x' -> inc (P x') (substrate r) -> inc (Q x') (substrate r') ->
  W x (ext_to_prod (canon_proj r) (canon_proj r')) =
  W x' (ext_to_prod (canon_proj r) (canon_proj r'))
  -> related (prod_of_relation r r') x x'.
Proof.
move=> r r' x x' er er' px Px Qx px' Px' Qx'.
have p1: (J (P x) (Q x) = x) by aw.
have p2: (J (P x') (Q x') = x') by aw.
rewrite -p1 -p2 ext_to_prod_rel_W // ext_to_prod_rel_W //.
rewrite prod_of_rel_pr.
move=> Jeq; move: (pr1_def Jeq) (pr2_def Jeq)=> eq1 eq2.
rewrite related_rw // related_rw //.
aw; rewrite eq1 eq2; intuition.
Qed.

Lemma related_ext_to_prod_rel: forall r r',
  is_equivalence r -> is_equivalence r' ->
  equivalence_associated (ext_to_prod(canon_proj r)(canon_proj r')) =
  prod_of_relation r r'.
Proof.
move=> r r' er er'.
move:(compatible_ext_to_prod er er')=> [fe [se re]].
have eq: is_equivalence (prod_of_relation r r')by apply equivalence_prod_of_rel.
have eq':(is_equivalence
    (equivalence_associated (ext_to_prod (canon_proj r) (canon_proj r')))).
  apply graph_ea_equivalence.
  apply ext_to_prod_function; fprops.
rewrite graph_exten; fprops.
have f1: is_function (canon_proj r) by fprops.
have f2: is_function (canon_proj r') by fprops.

move=> u v; rewrite ea_related //.
apply iff_eq; rewrite {1 2} /ext_to_prod bl_source 2! product_inc_rw.
  move=> [[up [Pu Qu]] [ [vp [Pv Qv]]]].
  have r1: (J (P u)(Q u) = u) by aw.
  have r2: (J (P v)(Q v) = v) by aw.
  rewrite -r1 -r2 ext_to_prod_W // ext_to_prod_W //.
  move: Pu Qu Pv Qv; rewrite 2! canon_proj_source => Pu Qu Pv Qv.
  aw; move=> neq; move: (pr1_def neq) (pr2_def neq)=> eq1 eq2.
  by rewrite prod_of_rel_pr related_rw // related_rw //; aw;ee.
move=> hyp; move: (hyp).
rewrite prod_of_rel_pr; move=> [pu [pv]]; rewrite related_rw // related_rw //.
move => [[Pu [Pv c1]] [Qu [Qv c2]]].
split; first (by intuition; aw). split; first by intuition;aw.
by apply re.
Qed.

Lemma decomposable_ext_to_prod_rel:forall r r',
  is_equivalence r -> is_equivalence r' ->
  exists h, bijection h &
    source h = quotient (prod_of_relation r r') &
    target h = product (quotient r) (quotient r')&
    h \co (canon_proj (prod_of_relation r r')) =
    ext_to_prod(canon_proj r)(canon_proj r').
Proof.
move=> r r' er er'.
set (r'':=prod_of_relation r r').
set (f'':=ext_to_prod (canon_proj r) (canon_proj r')).
set (h:=fun_on_quotient r'' f'').
have er'': is_equivalence r'' by rewrite /r''; apply equivalence_prod_of_rel.
have co: compatible_with_equiv f'' r''.
  rewrite /f'' /r''; apply compatible_ext_to_prod=>//.
move :(compose_foq_proj er'' co); rewrite -/h => cop.
have sh: source h = quotient r''.
   by rewrite /h /fun_on_quotient/section_canon_proj; aw.
have th: target h = product (quotient r) (quotient r').
  rewrite /h/fun_on_quotient/ f'' /ext_to_prod; aw.
have fh: is_function h.
  rewrite /h /f''; apply foqc_function =>//.
    apply ext_to_prod_function; fprops.
  by rewrite /r'' substrate_prod_of_rel // /ext_to_prod; aw.
have ff'': is_function f'' by rewrite /f''; apply ext_to_prod_rel_function.
have sf'': source f'' = substrate r''.
  rewrite /f'' /r''/ext_to_prod substrate_prod_of_rel; aw.
have ih: injection h.
  split=>//.
  move=> x y; rewrite sh /h => xs ys. rewrite foqc_W // . rewrite foqc_W //.
  move: (inc_rep_substrate er'' xs)(inc_rep_substrate er'' ys).
  rewrite substrate_prod_of_rel //. aw.
  move=> [px [Px Qx]] [py [Py Qy]] WW.
  move: (compatible_ext_to_prod_inv er er' px Px Qx py Py Qy WW).
  by rewrite related_rep_rep.
exists h. intuition.
split=>//; apply surjective_pr6=>//.
move=> y; rewrite th; aw; move=> [py [Py Qy]].
have p1: (inc (J (rep (P y)) (rep (Q y))) (substrate r'')).
  by rewrite /r'' substrate_prod_of_rel //; aw; split; fprops.
set (x:= class r'' (J (rep (P y)) (rep (Q y)))).
have xq: inc x (quotient r'') by rewrite /x; gprops.
have rxs: inc (rep x) (substrate r'') by fprops.
move: (related_rep_class er'' p1).
move: rxs; rewrite substrate_prod_of_rel; aw; move=> [ pr [Pr Qr]].
move: p1; rewrite substrate_prod_of_rel; aw; move=> [_ [Py' Qy']].
rewrite -/x related_prod_of_rel1 //.
move=> [u [v [e1 [e2 e3]]]].
exists x; rewrite sh.
split=>//.
rewrite /h foqc_W //.
have aux: (J (P (rep x)) (Q (rep x)) = (rep x)) by aw.
rewrite -aux /f'' ext_to_prod_rel_W //.
have aux2: (J (P y) (Q y) = y) by aw.
rewrite -aux2.
have res1: (P y = class r (P (rep x))) .
  apply is_class_pr =>//; rewrite e1; aw.
  move:Py; srw; rewrite is_class_rw //; move=> [neP [sP hyp]].
  have aux4:(inc (rep (P y)) (P y)) by apply nonempty_rep.
  by rewrite (hyp (rep (P y)) u aux4).
have res2: (Q y = class r' (Q (rep x))) .
  apply is_class_pr =>//; rewrite e1; aw.
  move:Qy; srw; rewrite is_class_rw //; move=> [neP [sP hyp]].
  have aux4:(inc (rep (Q y)) (Q y)) by apply nonempty_rep.
  by rewrite (hyp (rep (Q y)) v aux4).
by rewrite -res1 -res2.
Qed.

End Relation.
Export Relation.