Library sset3

Theory of Sets: EII-4 Union and intersection of a family of sets

Copyright INRIA (2009-2013) (Apics) Marelle Team (Jose Grimm).

Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
Require Export sset2.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Module Bunion.

EII-4-1 Definition of the union and intersection of a family of sets

Three definitions of union: a map of type I-> Set, a map of type Set -> Set and a functional graph. The definition is similar to that of a union of a set. There are also three definitions of intersection

Definition intersectiont (I:Set) (f : I->Set):=
  Zo (uniont f) (fun y => forall z : I, inc y (f z)).

Definition unionf (x:Set)(f: fterm) := uniont (fun a:x => f (Ro a)).
Definition unionb g := unionf (domain g)(Vg g).
Definition intersectionf (x:Set)(f: fterm) :=
  intersectiont (fun a:x => f (Ro a)).
Definition intersectionb g := intersectionf (domain g) (Vg g).

Basic properties of union

Lemma setUf_P x i f:
  inc x (unionf i f) <-> exists2 y, inc y i & inc x (f y).
Proof.
split;first by move/setUt_P=> [z zp]; exists (Ro z) =>//; apply: R_inc.
by move=>[y yi xf]; apply/setUt_P; exists (Bo yi); rewrite B_eq.
Qed.

Lemma setUb_P x f:
  inc x (unionb f) <-> exists2 y, inc y (domain f) & inc x (Vg f y).
Proof. exact: setUf_P. Qed.

Lemma setUb_P1 x a f:
   inc x (unionb (Lg a f)) <-> exists2 y, inc y a & inc x (f y).
Proof.
split.
  move /setUb_P; bw; move => [y ya]; bw => yf; ex_tac.
move => [y ya xf]; apply /setUb_P; bw;ex_tac; bw.
Qed.

Lemma setUt_i (I:Set) (f : I->Set) y x:
  inc x (f y) -> inc x (uniont f).
Proof. by move=> h;apply/setUt_P; exists y. Qed.

Lemma setUf_i x y i f:
  inc y i -> inc x (f y) -> inc x (unionf i f).
Proof. by move=> yi xf;apply/setUf_P; exists y. Qed.

Lemma setUb_i x y f:
  inc y (domain f) -> inc x (Vg f y) -> inc x (unionb f).
Proof. by move=> yd xv; apply/setUb_P; ex_tac. Qed.

Lemma setUf_hi x i f:
  inc x (unionf i f) -> exists2 y, inc y i & inc x (f y).
Proof. by move/setUf_P. Qed.

Lemma setUb_hi x f:
  inc x (unionb f) -> exists2 y, inc y (domain f) & inc x (Vg f y).
Proof. by move/setUb_P. Qed.

Ltac union_tac:=
  match goal with
    | H:inc ?x (?f ?y) |- inc ?x (uniont ?f)
      => apply: (setUt_i H)
    | Ha : inc ?i (domain ?g), Hb : inc ?x (Vg ?g ?i) |- inc ?x (unionb ?g)
      => apply: (setUb_i Ha Hb)
    | Ha : inc ?x ?y, Hb : inc ?y ?a |- inc ?x (union ?a)
      => apply: (setU_i Ha Hb)
    | Ha : inc ?y ?i, Hb : inc ?x (?f ?y) |- inc ?x (unionf ?i ?f)
      => apply: (setUf_i _ Ha Hb)
    | Ha : inc ?y ?i |- inc ?x (unionf ?i ?f)
      => apply: (setUf_i Ha); fprops
    | Hb : inc ?x (?f ?y) |- inc ?x (unionf ?i ?f)
      => apply: (setUf_i _ Hb); fprops
    | Ha : inc ?i (domain ?g) |- inc ?x (unionb ?g)
      => apply: (setUb_i Ha); fprops
    | Hb : inc ?x (Vg ?g ?i) |- inc ?x (unionb ?g)
      => apply: (setUb_i _ Hb); fprops
    | Hb : inc ?z ?X |- inc ?x (union ?X)
      => apply: (setU_i _ Hb); fprops
    | Ha : inc ?x ?z |- inc ?x (union ?X)
      => apply: (setU_i Ha); fprops
  end.

If the index set is empty so are the union and intersection

Lemma setUt_0 (I:Set) (f:I-> Set): I = emptyset -> uniont f = emptyset.
Proof.
move => ie; apply /set0_P => t /setUt_P [x].
move: (R_inc x); rewrite {2} ie; case; case.
Qed.

Lemma setUf_0 f: unionf emptyset f = emptyset.
Proof. by apply: setUt_0. Qed.

Lemma setUb_0: unionb emptyset = emptyset.
Proof. rewrite /unionb domain_set0; apply/setUf_0. Qed.

Lemma setIt_0 (I:Set) (f:I-> Set):
  I = emptyset -> intersectiont f = emptyset.
Proof.
move=> Ie; apply /set0_P => t /Zo_P; rewrite (setUt_0 _ Ie);case; case; case.
Qed.

Lemma setIf_0 f: intersectionf emptyset f = emptyset.
Proof. by apply: setIt_0. Qed.

Lemma setIb_0: intersectionb emptyset = emptyset.
Proof. rewrite /intersectionb domain_set0; apply/setIf_0. Qed.

Basic properties of the intersection in the non-trivial case

Lemma setIt_P (I:Set) (f:I-> Set): nonempty I -> forall x,
  (inc x (intersectiont f) <-> (forall j, inc x (f j))).
Proof.
move=> [i [ix _]];split; first by move /Zo_hi.
move => h1; apply: Zo_i => //; move: (h1 ix); apply: setUt_i.
Qed.

Lemma setIf_P I f: nonempty I -> forall x,
  (inc x (intersectionf I f) <-> (forall j, inc j I -> inc x (f j))).
Proof.
move => h x; split; first by move/(setIt_P _ h) => aux j [ji <-]; apply: aux.
move => aux; apply/(setIt_P _ h) => j; apply: aux; apply: R_inc.
Qed.

Lemma setIb_P g: nonempty g -> forall x,
  (inc x (intersectionb g) <-> (forall i, inc i (domain g) -> inc x (Vg g i))).
Proof. move/domain_set0P => h x; exact: (setIf_P _ h). Qed.

Lemma setI_P y: nonempty y -> forall x,
  (inc x (intersection y) <-> (forall i, inc i y -> inc x i)).
Proof.
by move=> ney; split; [ move=> xi iy; apply: setI_hi | apply: setI_i].
Qed.

Lemma setIt_i (I:Set) (f:I-> Set) x: nonempty I ->
  (forall j, inc x (f j)) -> inc x (intersectiont f).
Proof. by move=> pa pb; apply/setIt_P. Qed.

Lemma setIt_hi (I:Set) (f:I-> Set) x j:
  inc x (intersectiont f) -> inc x (f j).
Proof. move /(setIt_P _ (nonempty_intro (R_inc j))); apply. Qed.

Lemma setIf_i I f x: nonempty I ->
  (forall j, inc j I -> inc x (f j)) -> inc x (intersectionf I f).
Proof. by move=> pa pb; apply/setIf_P. Qed.

Lemma setIf_hi I f x j:
  inc x (intersectionf I f) -> inc j I -> inc x (f j).
Proof. move => pa pb; move /(setIf_P): pa; apply => //; ex_tac. Qed.

Lemma setIb_i g x: nonempty g ->
  (forall i, inc i (domain g) -> inc x (Vg g i)) -> inc x (intersectionb g).
Proof. by move=> neg h; apply/setIb_P. Qed.

Lemma setIb_hi g x i:
  inc x (intersectionb g) -> inc i (domain g) -> inc x (Vg g i).
Proof.
by move => /setIb_P pa pb; apply: pa => //; apply /domain_set0P; ex_tac.
Qed.

Lemma setUt_exten (I:Set) (f: I-> Set) (f':I->Set):
  f =1 f' -> uniont f = uniont f'.
Proof.
move=> hyp; set_extens t; move/setUt_P=> [z zi]; apply/setUt_P; exists z.
  by rewrite -hyp.
by rewrite hyp.
Qed.

Lemma setUf_exten sf f f':
  {inc sf, f =1 f'} -> unionf sf f = unionf sf f'.
Proof.
move=> hyp; set_extens t;move/setUf_P=> [z zi tf]; apply/setUf_P; ex_tac.
  by rewrite -hyp.
by rewrite hyp.
Qed.

Lemma setIt_exten (I:Set) (f f':I-> Set):
   f =1 f' -> (intersectiont f) = (intersectiont f').
Proof.
move=> hyp; case: (emptyset_dichot I) => ie.
  by rewrite !(setIt_0 _ ie).
set_extens t; move/(setIt_P _ ie) => h; apply/(setIt_P _ ie) => j.
  rewrite - hyp; apply: h.
rewrite hyp; apply: h.
Qed.

Lemma setIf_exten I f f': {inc I, f =1 f'} ->
  intersectionf I f = intersectionf I f'.
Proof.
move=> h; apply: setIt_exten => a;apply: h; apply: R_inc.
Qed.

Lemma setUt_s1 (I:Set) (f: I-> Set) i: sub (f i) (uniont f).
Proof. move=> t tf; union_tac. Qed.

Lemma setIt_s1 (I:Set) (f: I-> Set) i: sub (intersectiont f) (f i).
Proof. move=> t; apply: setIt_hi. Qed.

Lemma setUt_s2 (I:Set) (f: I-> Set) x:
  (forall i, sub (f i) x) -> sub (uniont f) x.
Proof. by move=> hyp t; move/setUt_P=> [z tfz]; apply: (hyp z). Qed.

Lemma setIt_s2 (I:Set) (f: I-> Set) x:
  nonempty I ->
  (forall i, sub x (f i)) -> sub x (intersectiont f).
Proof. by move=> ne hyp t tx; apply/setIt_P => // j; apply: hyp. Qed.

Lemma setIt_sub2 (I:Set) (f: I-> Set) x:
  (forall i, sub (f i) x) -> sub (intersectiont f) x.
Proof.
move=> hyp t ti.
case: (emptyset_dichot I) => ie.
  by move: ti; rewrite setIt_0 // => /in_set0.
case: ie => y; case => z _; apply: (hyp z); move: ti;apply:setIt_s1.
Qed.

Lemma setUt_sub2 (I:Set) (f: I-> Set) x:
  nonempty I -> (forall i, sub x (f i)) -> sub x (uniont f).
Proof. by move=> [y yI] hyp t tx; apply/setUt_P; exists (Bo yI);apply: hyp. Qed.

Proposition 1 : union (compose g f) = union g

Theorem setUt_rewrite (I K:Set) (f: K->I) (g:I ->Set):
  surjectiveC f ->
  uniont g = uniont (g \o f).
Proof.
move=> sf; set_extens t; move/setUt_P=> [z zp]; apply/setUt_P.
  by move: (sf z) => [v fv] /=; exists v; ue.
by exists (f z).
Qed.

Theorem setIt_rewrite (I K:Set) (f: K->I) (g:I ->Set):
  surjectiveC f ->
  intersectiont g = intersectiont (g \o f).
Proof.
move=> sf; case: (emptyset_dichot I) => ei.
  rewrite ! setIt_0 =>//; apply /set0_P => y [x _].
  move: (f x); rewrite ei; case.
have nek: nonempty K.
  move: ei => [k [i]] _; move: (sf i)=> [j _]; exists (Ro j); apply: R_inc.
set_extens t; move/setIt_P=> h; apply/setIt_P => // j; first by apply: (h ei).
move: (sf j) => [k <-]; exact: (h nek k).
Qed.

Lemma setUb_rewrite f g:
  fgraph f -> range f = domain g ->
  unionb g = unionb (g \cf f).
Proof.
rewrite /composef=> fgf rfsg.
set_extens t; move/setUb_P => [a pa pb]; apply/setUb_P.
  move: pa; rewrite- rfsg; move /(range_gP fgf) => [x xd etc].
  bw; ex_tac; bw; ue.
move: pa; bw => pa; move: pb; bw; rewrite- rfsg => ta; exists (Vg f a); fprops.
Qed.

Lemma setUb_rewrite1 f g:
  function f -> fgraph g -> range (graph f) = domain g ->
  unionb g = unionb (g \cf (graph f)).
Proof.
move=> [_ fgf _] fgg rfg.
have fc: g \cfP (graph f) by split => //; ue.
by apply: setUb_rewrite.
Qed.

Lemma setIb_rewrite f g:
  fgraph f -> range f = domain g ->
  intersectionb g = intersectionb (g \cf f).
Proof.
move=> fgf rfdg.
case: (emptyset_dichot g) => gp.
  have -> //: (g \cf f = g).
  rewrite gp; apply /set0_P => t /funI_P [z zd _].
  have :(inc (Vg f z) (range f)) by fprops.
  rewrite rfdg gp domain_set0; apply: in_set0.
have nec: (nonempty (g \cf f)).
  move: gp => [x xg].
  have : (inc (P x) (range f)) by rewrite rfdg; fprops.
  move/(range_gP fgf) => [y ydf etc].
  exists (J y (Vg g (Vg f y))); apply/funI_P; ex_tac.
set_extens t.
  move/(setIb_P gp) => h; apply/(setIb_P nec); rewrite /composef; bw => j jdf.
  bw; apply: h; rewrite - rfdg; apply range_gP => //; ex_tac.
move/(setIb_P nec) => h; apply/(setIb_P gp) => i; rewrite -rfdg.
move/(range_gP fgf) => [x xdf ->]; move: (h x);rewrite /composef; bw.
by apply.
Qed.

Union and intersection of a function with singleton range

Lemma setUt_constant (I:Set) (f:I ->Set) (x:I):
  constantp f -> uniont f = f x.
Proof.
move=> cf.
by set_extens t; [move/setUt_P => [z]; rewrite (cf x z) | move=> tp;union_tac].
Qed.

Lemma setIt_constant (I:Set) (f:I ->Set) (x:I):
  constantp f -> intersectiont f = f x.
Proof.
have neI: nonempty I by exists (Ro x); apply: R_inc.
move => cf;apply: extensionality; first by apply:setIt_s1.
by move => h j;apply: setIt_i => // k; rewrite (cf k x).
Qed.

Lemma setUt_1 (a:Set) (x:a) (f: singleton (Ro x) -> Set):
  uniont f = f (Bo (set1_1 (Ro x))).
Proof.
set_extens t => pt; last by union_tac.
move /setUt_P: pt => [y tfy].
have <- //: (y = (Bo (set1_1 (Ro x)))).
by apply: R_inj; move: (R_inc y) => /set1_P ->; rewrite B_eq.
Qed.

Lemma setIt_1 (a:Set)(x:a) (f: singleton (Ro x) -> Set):
  intersectiont f = f (Bo (set1_1 (Ro x))).
Proof.
apply: extensionality; first by apply:setIt_s1.
move => t ti; apply: setIt_i;[by fprops | move=> j].
have -> //: (j = (Bo (set1_1 (Ro x)))).
by apply: R_inj; move: (R_inc j) => /set1_P ->; rewrite B_eq.
Qed.

Lemma setUf_1 f x: unionf (singleton x) f = f x.
Proof.
by set_extens t => tp; [ move: (setUf_hi tp)=> [y /set1_P ->] | union_tac ].
Qed.

Lemma setIf_1 f x: intersectionf (singleton x) f = f x.
Proof.
set_extens t => tx; first by exact :(setIf_hi tx (set1_1 x)).
apply: setIf_i; [ fprops | by move=> j; move/set1_P => ->].
Qed.

Lemma setUg_constant f x: constantgp f -> inc x (domain f) ->
  unionb f = Vg f x.
Proof.
move => p1 p2; set_extens t; last by move => p3; union_tac.
by move /setUb_P => [y y1 y2]; rewrite (proj2 p1 _ _ p2 y1).
Qed.

Lemma setIg_constant f x: constantgp f -> inc x (domain f) ->
  intersectionb f = Vg f x.
Proof.
move => p1 p2.
have nef: nonempty f by apply /domain_set0P; ex_tac.
set_extens t; first by move /(setIb_P nef); apply.
by move => h; apply /(setIb_P nef) => i idf;rewrite (proj2 p1 _ _ idf p2).
Qed.

Link between union and unionb

Lemma setU_prop x: union x = unionf x id.
Proof. by apply: setUt_exten => t. Qed.

Lemma setI_prop x: intersection x = intersectionf x id.
Proof.
case: (emptyset_dichot x) => xe; first by rewrite xe setI_0 setIf_0.
set_extens t; first by move/(setI_P xe) =>h; apply:setIf_i.
by move/(setIf_P _ xe) =>h;apply:setI_i.
Qed.

Lemma setUb_alt f: fgraph f -> unionb f = union (range f).
Proof.
move=> fgf.
set_extens t; first by move/setUb_P=> [y ty yx]; union_tac.
move/setU_P => [z te]; move/(range_gP fgf) => [x xd eq]; union_tac; ue.
Qed.

Lemma setUb_identity x: unionb (identity_g x) = union x.
Proof.
rewrite /unionb identity_d setU_prop.
by apply: setUf_exten; move=> i ix /=; rewrite identity_ev.
Qed.

Lemma setIb_alt f: fgraph f -> intersectionb f = intersection (range f).
Proof.
move => fgf; case: (emptyset_dichot f) => fe.
  by rewrite fe range_set0 setI_0 setIb_0.
set_extens t.
  move => ti; apply:setI_i.
    move: fe => [w tf]; exists (Q w); apply/funI_P; ex_tac.
  move=> y /(range_gP fgf) [x xdf ->]; exact: (setIb_hi ti xdf).
move => ti; apply:setIb_i => // i idf; apply: (setI_hi ti).
apply /(range_gP fgf); ex_tac.
Qed.

Lemma setIb_identity x: intersectionb (identity_g x) = intersection x.
Proof.
rewrite /intersectionb identity_d setI_prop.
by apply: setIf_exten; move=> i ix /=; rewrite identity_ev.
Qed.

EII-4-2 Properties of union and intersection

Monotony properties

Lemma setUt_S (I:Set) (f g:I->Set):
  (forall i, sub (f i) (g i)) -> sub (uniont f) (uniont g).
Proof.
by move=> su t /setUt_P [z tf]; apply/setUt_P; exists z; apply: su.
Qed.

Lemma setIt_S (I:Set) (f g:I->Set):
  (forall i, sub (f i) (g i)) -> sub (intersectiont f) (intersectiont g).
Proof.
move=> su.
case: (emptyset_dichot I) => i2; first by rewrite !setIt_0.
move=> t/(setIt_P _ i2) hyp; apply/setIt_P => //j; apply: su;apply: hyp.
Qed.

Lemma setUf_S2 f: {compat (unionf ^~ f) : x y / sub x y }.
Proof. move => x y /= sab t /setUf_P [z yA tfy]; union_tac. Qed.

Lemma setIf_S f:
  {compat (intersectionf ^~ f) : x y / sub x y /\ nonempty x >-> sub y x}.
Proof.
move=> A B [sAB neA].
have neB: (nonempty B) by move:neA=> [x]; exists x; apply: sAB.
by move=> x /(setIf_P _ neB) p; apply:(setIf_i neA) =>j jA; apply:p; apply: sAB.
Qed.

Associativity of union and intersection

Theorem setUf_A sg f g:
  unionf (unionf sg g) f = unionf sg (fun l => unionf (g l) f).
Proof.
set_extens t; move /setUf_P=> [y yu tfy]; [ move: yu | move: tfy];
  move/setUf_P => [z zsg ygz]; apply/setUf_P; exists z =>//; union_tac.
Qed.

Theorem setIf_A sg f g:
  (alls sg (fun i => (nonempty (g i)))) ->
  intersectionf (unionf sg g) f
   = intersectionf sg (fun l => intersectionf (g l) f).
Proof.
move=> neall.
case: (emptyset_dichot sg) => sgp.
  by rewrite sgp setUf_0 // 2! setIf_0.
have neu: (nonempty (unionf sg g)).
  by move: sgp=> [x xsg]; move: (neall _ xsg)=> [y iy]; exists y; union_tac.
set_extens t.
   move/(setIf_P _ neu) => h; apply: (setIf_i sgp) => j jsg.
   apply: (setIf_i (neall _ jsg)) => k kj; apply: h; union_tac.
move/(setIf_P _ sgp) => h; apply: (setIf_i neu) => j /setUf_P [y ysg jgy].
exact (setIf_hi (h _ ysg) jgy).
Qed.

EII-4-3 Images of a union and an intersection


Theorem dirim_setUt (I:Set) (f:I->Set) g:
  direct_image g (uniont f) = uniont (fun i => direct_image g (f i)).
Proof.
set_extens t.
  move /dirim_P=> [x /setUt_P [y xfy] Ju]; apply /setUt_P.
  exists y; apply/dirim_P; ex_tac.
move /setUt_P => [z /dirim_P [x xf Jg]].
apply /dirim_P;ex_tac; union_tac.
Qed.

Theorem dirim_setIt (I:Set) (f:I->Set) g:
  sub (direct_image g (intersectiont f))
  (intersectiont (fun i => direct_image g (f i))).
Proof.
move => t /dirim_P [x].
case: (emptyset_dichot I) => neI; first by rewrite (setIt_0 _ neI); case; case.
move => ta tb; apply: (setIt_i neI) => j; apply/dirim_P; ex_tac.
apply: (setIt_hi _ ta).
Qed.

Theorem iim_fun_setIt (I:Set) (f:I->Set) g:
  function g ->
  (inv_image_by_fun g (intersectiont f)) =
  (intersectiont (fun i => inv_image_by_fun g (f i))).
Proof.
move=> fg.
apply: extensionality; first by rewrite iim_fun_pr; apply:dirim_setIt.
case: (emptyset_dichot I) => ie; first by rewrite (setIt_0 _ ie); fprops.
move => t /(setIt_P _ ie) aj.
move: (ie)=> [x [z _]]; move: (aj z) => /iim_fun_P[u ufz Jg].
apply/iim_fun_P; ex_tac; apply: (setIt_i ie) => v.
move: (aj v) => /iim_graph_P [u' ufx Jg'].
by rewrite (Vf_pr fg Jg); rewrite - (Vf_pr fg Jg').
Qed.

Lemma inj_image_setIt (I:Set) (f:I->Set) g:
  injection g ->
  (image_by_fun g (intersectiont f))
  = (intersectiont (fun i => image_by_fun g (f i))).
Proof.
move=> ig; move: (proj1 ig) => fg.
have [_ _ _ _ aux]:= (canonical_decomposition1 fg).
have sf := (iim_fun_r fg).
rewrite sf iim_fun_setIt; last by apply: (bijective_inv_f (aux ig)).
by apply: setIt_exten.
Qed.

EII-4-4 complement of unions and intersections


Theorem setCUt2 (I:Set) (f:I-> Set) x: nonempty I ->
  x -s (uniont f) = intersectiont (fun i=> x -s (f i)).
Proof.
move=>neI; set_extens z.
  move /setC_P =>[zx zu];apply:(setIt_i neI) => j; apply setC_i => //.
  dneg t; union_tac.
move: neI=> [_ [i _]] xi; move: (setIt_hi i xi) => /setC_P [zx zu].
apply: setC_i => //;move /setUt_P => [j zj].
by move: (setIt_hi j xi) => /setC_P [_].
Qed.

Theorem setCIt2 (I:Set) (f:I-> Set) x: nonempty I ->
  x -s (intersectiont f) = uniont (fun i=> x -s (f i)).
Proof.
move=> neI.
set_extens t.
  move/setC_P => [tx ti]; apply/setUt_P; ex_middle bad.
  case: ti; apply /(setIt_P _ neI) => j; ex_middle bad2.
  case: bad; exists j; apply: setC_i => //.
move/setUt_P => [z /setC_P [tx tf]];apply: setC_i => //; dneg h.
exact (setIt_hi z h).
Qed.

Lemma setCUf2 sf f x: nonempty sf ->
  x -s (unionf sf f) = intersectionf sf (fun i=> x -s (f i)).
Proof. by apply: setCUt2. Qed.

Lemma setCIf2 sf f x: nonempty sf ->
  x -s (intersectionf sf f) = unionf sf (fun i=> x -s (f i)).
Proof. by apply: setCIt2. Qed.

EII-4-5 union and intersection of two sets


Lemma setUf2f x y f:
  unionf (doubleton x y) f = (f x) \cup (f y).
Proof.
set_extens t.
  move/setUf_P => [z /set2_P []] -> h; fprops.
case /setU2_P=> tf; union_tac.
Qed.

Lemma setIf2f x y f:
  intersectionf (doubleton x y) f = (f x) \cap (f y).
Proof.
move: (set2_ne x y) => ned.
set_extens z.
  move /(setIf_P _ ned) => h; apply setI2_i; apply: h; fprops.
by move/setI2_P => [zx zy]; apply: (setIf_i ned) => j; case/set2_P => ->.
Qed.

Lemma setUf2 x y: unionf (doubleton x y) id = x \cup y.
Proof. by rewrite setUf2f. Qed.

Lemma setIf2 x y: intersectionf (doubleton x y) id = x \cap y.
Proof. by rewrite setIf2f. Qed.

Lemma dirim_setU2 g: {morph (direct_image g): x y / x \cup y}.
Proof. by move => x y /=; rewrite - setUf2f - setUf2 dirim_setUt. Qed.

Lemma dirim_setI2 g x y:
  sub (direct_image g (x \cap y))
  ((direct_image g x) \cap (direct_image g y)).
Proof. rewrite - setIf2f - setIf2; apply: dirim_setIt. Qed.

Lemma iim_fun_setI2 g: function g ->
  {morph (inv_image_by_fun g): x y / x \cap y}.
Proof.
by move => fg x y /=; rewrite - setIf2f - setIf2; apply iim_fun_setIt.
Qed.

Lemma iim_fun_C1 f: function f ->
 {when eq^~ (target f) & sub^~ (target f),
   {morph inv_image_by_fun f : a b / a -s b}}.
Proof.
move => ff a b -> btf.
set_extens t.
  move/iim_fun_P=> [u /setC_P [utf ux] Jg];apply: setC_i.
    apply/iim_fun_P;ex_tac.
  by move/iim_fun_P=>[v vx Jvg]; case: ux;rewrite (Vf_pr ff Jg) -(Vf_pr ff Jvg).
move/setC_P => [/iim_fun_P [u ut Jg] ne]; apply/iim_fun_P; ex_tac.
apply/setC_i => //;dneg h; apply/iim_fun_P; ex_tac.
Qed.

Lemma inj_image_C f: injection f ->
 {when eq^~ (source f) & sub^~ (source f),
   {morph image_by_fun f : a b / a -s b}}.
Proof.
move=> ig a b ->; move: (proj1 ig) => fg.
have [_ fv _ _ aux] := (canonical_decomposition1 fg).
rewrite 3! (iim_fun_r fg).
have ->: source f = target (inverse_fun (restriction_to_image f)).
  by rewrite {1} fv; aw.
by apply: iim_fun_C1 => //; apply: (bijective_inv_f (aux ig)).
Qed.

EII-4-6 Coverings

We define a covering for a map, a function, and a set of sets

Definition covering f x := fgraph f /\ sub x (unionb f).
Definition covering_s f x := sub x (union f).

Lemma covering_P f x: fgraph f ->
   (covering f x <-> covering_s (range f) x).
Proof.
move => fgf; rewrite /covering/covering_s setUb_alt //.
split; [ by case | by split ].
Qed.

Two definitions, second one will be used in set5

Definition coarser_cg f g :=
  [/\ fgraph f, fgraph g &
  forall j, inc j (domain g)
    -> exists2 i, inc i (domain f) & sub (Vg g j) (Vg f i)].

Definition coarser_cs y y':=
  forall a, inc a y' -> exists2 b, inc b y & sub a b.

Lemma coarser_cP f g: fgraph f -> fgraph g ->
  (coarser_cg f g <-> coarser_cs (range f) (range g)).
Proof.
move => fgf fgg;split.
  move=> [_ _ cc j]; move/(range_gP fgg) => [i id ->].
  move: (cc _ id) => [k kdf h];exists (Vg f k) => //.
  apply/(range_gP fgf); ex_tac.
move => cc; split => // j jdg.
move: (cc _ (inc_V_range fgg jdg)) => [i /(range_gP fgf) [k kdf ->] h].
ex_tac.
Qed.

Lemma sub_covering f I x (g := restr f I):
  (sub I (domain f)) -> covering f x -> covering g x ->
  coarser_cg f g.
Proof.
move => sd [fgf cf] [fgg cg]; split => // j; rewrite restr_d => jJ.
move: (sd _ jJ) => jdf; ex_tac; rewrite /g restr_ev //.
Qed.

We consider the family of intersections of two families

Definition intersection_covering f g :=
  Lg ((domain f) \times (domain g))
    (fun z => (Vg f (P z)) \cap (Vg g (Q z))).

Definition intersection_covering2 x y:=
  range (intersection_covering (identity_g x) (identity_g y)).

Lemma setI_covering2_P x y z:
  inc z (intersection_covering2 x y) <->
  exists a b, [/\ inc a x, inc b y & a \cap b = z].
Proof.
rewrite /intersection_covering2 /intersection_covering 2! identity_d.
set g := Lg _ _.
have fgg: fgraph g by rewrite /g; fprops.
rewrite /g;split.
  move/Lg_range_P => [b /setX_P [pb Pb Qb] ->].
  by rewrite identity_ev // identity_ev //; exists (P b); exists (Q b).
move => [a [b [ax iby <-]]]; apply/Lg_range_P.
exists (J a b); [ fprops | aw;rewrite identity_ev // identity_ev //].
Qed.

Lemma setI_covering E: {compat intersection_covering : x & / covering x E}.
Proof.
move => f g [fgf c1] [fgg c2].
rewrite /intersection_covering; split; first by fprops.
move => u ux; move /setUb_P: (c1 _ ux) => [a af uf].
move/setUb_P:(c2 _ ux)=> [b bg ug].
apply/setUb_P;bw;exists (J a b); [ fprops | bw; aw; fprops].
Qed.

Lemma setI_coarser_cl f g x:
  covering f x -> covering g x ->
  coarser_cg f (intersection_covering f g).
Proof.
move=> [fgf c1] [fgg c2].
rewrite /intersection_covering; red; bw; split; fprops.
move => j ji; move /setX_P:(ji)=> [pj Pj Qj]; ex_tac => t; bw; apply: setI2_1.
Qed.

Lemma setI_coarser_cr f g x:
  covering f x -> covering g x ->
  coarser_cg g (intersection_covering f g).
Proof.
move=> [fgf c1] [fgg c2].
rewrite /intersection_covering; red; bw;split; fprops.
move => j ji;move /setX_P: (ji)=> [pj Pj Qj]; ex_tac => t; bw; apply: setI2_2.
Qed.

Lemma setI_coarser_clr h x:
  covering h x -> {when covering ^~ x &,
      {compat intersection_covering : f & / coarser_cg f h}}.
Proof.
move => c3 f g c1 c2 [fgf fhg cc1] [fgg _ cc2].
rewrite /intersection_covering /coarser_cg; bw.
split;[ fprops | exact | move => u udh ].
move: (cc1 _ udh); move: (cc2 _ udh); move=> [i isg s1] [j jsf s2].
exists (J j i); bw; fprops; aw.
by move=> v vh; apply/setI2_i; [apply: s2 |apply: s1].
Qed.

Next four lemmas are a rewrite of above; they say that intersection_covering2 is the supremum of both args

Lemma setI_covering2 E:
  {compat intersection_covering2 : x & / covering_s x E}.
Proof.
move=> u v c1 c2 z zu.
move /setU_P: (c1 _ zu) =>[y zy yu].
move /setU_P: (c2 _ zu) =>[y' xzy' yv].
apply/setU_P;exists (y \cap y'); first by fprops.
by apply/ setI_covering2_P; exists y, y'.
Qed.

Lemma setI_coarser2_cl f g x:
  covering_s f x -> covering_s g x ->
  coarser_cs f (intersection_covering2 f g).
Proof.
move=> c1 c2 z; move/setI_covering2_P=> [a [b [af bg <-]]].
ex_tac; apply: subsetI2l.
Qed.

Lemma setI_coarser2_cr f g x:
  covering_s f x -> covering_s g x ->
  coarser_cs g (intersection_covering2 f g).
Proof.
move=> c1 c2 z; move/setI_covering2_P=> [a [b [af bg <-]]].
ex_tac; apply: subsetI2r.
Qed.

Lemma setI_coarser2_clr h x:
  covering_s h x -> {when covering_s ^~ x &,
      {compat intersection_covering2 : f & / coarser_cs f h}}.
Proof.
move=> c23 f g c1 c2 cc1 cc2 t th.
move: (cc1 _ th)=> [b bf tb]; move: (cc2 _ th)=> [b' bg tb'].
exists (b \cap b').
  by apply/setI_covering2_P; exists b; exists b'.
by apply: setI2_12S.
Qed.

We consider the direct and inverse image of a covering, and the product of two coverings

Lemma image_of_covering f g:
  surjection g -> covering f (source g)
  -> covering (Lg (domain f) (fun w => image_by_fun g (Vg f w))) (target g).
Proof.
move=> [fg sg] [fgf cf]; split; first by fprops.
move => x xtg; move: (sg _ xtg)=> [y ys vg].
move:(setUf_hi (cf _ ys)) => [z zsf yfz].
apply/setUb_P; bw; ex_tac; bw; rewrite -vg; apply/dirim_P; ex_tac; Wtac.
Qed.

Lemma inv_image_of_covering f g:
  function g -> covering f (target g)
  -> covering (Lg(domain f) (fun w => inv_image_by_fun g (Vg f w))) (source g).
Proof.
move=> fg [fgf cf]; split; first by fprops.
move => x xs; apply/setUb_P; bw.
have Wt: (inc (Vf g x) (target g)) by fprops.
move /setUb_P: (cf _ Wt) => [y ysf Wf]; ex_tac; bw.
apply/iim_fun_P; ex_tac; Wtac.
Qed.

Lemma product_of_covering f g x y:
  covering f x -> covering g y ->
  covering (Lg ((domain f) \times (domain g))
        (fun z => (Vg f (P z)) \times (Vg g (Q z))))
  (x \times y).
Proof.
move=> [fgf c1] [fgg c2]; split; first by fprops.
move => z /setX_P [zp px qy].
move /setUb_P: (c1 _ px) => [a asf pa].
move /setUb_P: (c2 _ qy) => [b bsg ab].
have pc: inc (J a b) ((domain f) \times (domain g)) by fprops.
by apply/setUb_P;exists (J a b); bw; aw;apply:setX_i.
Qed.

If two functions agree on each element of a cobvering of X, they agree on X

Lemma agrees_on_covering f x g g':
  covering f x -> function g -> function g' ->
  source g = x -> source g' = x ->
  (forall i, inc i (domain f) -> agrees_on (x \cap (Vg f i)) g g') ->
  agrees_on x g g'.
Proof.
move=> [fgf c] fg fg' sg sg' ag.
hnf; rewrite sg sg';split; fprops.
move=> a ax; move /setUb_P: (c _ ax) => [y ysf afy].
by move: (ag _ ysf)=> [ _ _ ]; apply; apply: setI2_i.
Qed.

We consider the fonction whose source is the union of a family f, the target is t, the graph is the union of all h i, which are functions defined V i f with a compatibility condition

Definition common_ext f h t:=
  triple (unionb f) t (unionb (Lg (domain f) (fun i => (graph (h i))))).

Definition function_prop_sub f s t:=
  [/\ function f, source f = s & sub (target f) t].

Lemma extension_covering f t h
  (d:= domain f) (g := common_ext f h t) :
  (forall i, inc i d -> function_prop (h i) (Vg f i) t) ->
  (forall i j, inc i d -> inc j d ->
    agrees_on ((Vg f i) \cap (Vg f j)) (h i) (h j)) ->
  [/\ function_prop g (unionb f) t,
    graph g = (unionb (Lg d (fun i => (graph (h i))))),
    range (graph g) = unionb (Lg d (fun i => (range (graph (h i))))) &
    (forall i, inc i d -> agrees_on (Vg f i) g (h i))].
Proof.
move=> afp aag.
have sg: (source g = unionb f) by rewrite /g /common_ext; aw.
have tg: (target g = t) by rewrite /g/common_ext; aw.
set u1:= unionb (Lg _ _).
have gg: graph g = u1 by rewrite /u1/g/common_ext; aw.
have gu: sgraph u1.
  move=> z /setUb_P; bw;move=> [y yd]; bw => zd.
  by move: (afp _ yd) => [ff _ _]; move: (function_sgraph ff); apply.
have fgf: fgraph u1.
  rewrite /u1;split=>//.
  move => x y /setUb_P [u usf xghu] /setUb_P [v vsf yghv] sp.
  move: usf vsf; bw => usf vsf; move:xghu yghv; bw => xghu yghv.
  move:(afp _ usf) => [fu shu _]; move:(afp _ vsf) => [fv shv _].
  move: (Vf_pr2 fu xghu) => qx; move: (Vf_pr2 fv yghv)=>qy.
  apply: pair_exten=>//.
    by apply: (function_sgraph fu).
    by apply: (function_sgraph fv).
  rewrite qx qy sp; move: (aag _ _ usf vsf)=> [_ _]; apply.
  by rewrite - shu - shv; apply: setI2_i ;[ rewrite - sp|]; Wtac.
have fg: function g.
  rewrite /g/common_ext; apply: function_pr=>//.
    move=> z /funI_P [x /setUb_P]; bw;move=> [y ysf]; bw => Jg ->.
    by move: (afp _ ysf)=> [fhy _ <-]; Wtac.
  set_extens z.
    move /setUb_P=> [y ysf zfy]; apply/(domainP gu); exists (Vf (h y) z).
    move: (afp _ ysf) => [fhy shy _].
    apply /setUb_P; bw; exists y;bw; apply: Vf_pr3 => //; ue.
  move/(domainP gu) => [y]; move/setUb_P; bw;move=> [x xsf]; bw => jg.
  move: (afp _ xsf) => [fhx shx _]; apply/setUb_P;ex_tac; rewrite - shx; Wtac.
split => //.
  rewrite /g/common_ext; aw; set_extens zs.
    move/(rangeP gu)=> [x] /setUb_P; bw; move =>[y ysf]; bw => zfy.
    apply/setUb_P;move: (afp _ ysf) => [fhy shy _]; bw; ex_tac; bw;ex_tac.
  move/setUb_P; bw; move=> [y ysf]; bw.
  move: (afp _ ysf) => [fhy shy _].
  move /(rangeP (function_sgraph fhy)) => [x Jg].
  apply/(rangeP gu); exists x; apply/setUb_P; bw; exists y; bw.
move=> y ysf; move: (afp _ ysf) => [fhy shy _].
split; first by rewrite sg; move=> x xfy; union_tac.
  by rewrite shy; fprops.
move=> a afy /=; symmetry;apply: Vf_pr => //.
rewrite gg; apply /setUb_P; bw; ex_tac; bw; Wtac; ue.
Qed.

Lemma extension_covering_thm f t h (d:= domain f):
  (forall i, inc i d -> function_prop (h i) (Vg f i) t) ->
  (forall i j, inc i d -> inc j d ->
    agrees_on ( (Vg f i) \cap (Vg f j)) (h i) (h j)) ->
  fgraph f ->
  exists! g, (function_prop g (unionb f) t /\
    (forall i, inc i d -> agrees_on (Vg f i) g (h i))).
Proof.
move=> afp aag fgf; apply /unique_existence;split.
  move: (extension_covering afp aag)=> [p1 p2 p3 p4].
  by exists (common_ext f h t).
rewrite /function_prop=> x y [[fx sx tx] agx] [[fy sy ty] agy].
apply: function_exten=>//; try ue.
have c: (covering f (unionb f)) by split => //.
suff agi: (forall i, inc i d -> agrees_on ((unionb f) \cap (Vg f i)) x y).
  move:(agrees_on_covering c fx fy sx sy agi)=>p.
  move:p => [_ _]; rewrite sx; apply.
move=> i isf; hnf.
split;first by rewrite sx;apply: subsetI2l.
  by rewrite sy;apply: subsetI2l.
move => a /setI2_P; move: (agx _ isf) (agy _ isf).
rewrite /agrees_on; move=> [_ _ p1][_ _ p2] [_ afi].
by rewrite (p1 _ afi) (p2 _ afi).
Qed.

EII-4-7 Partitions

A partition is a kind of covering formed of mutually disjoint sets. We may assume the sets non-empty

Definition nonempty_fam f := allf f nonempty.

Definition mutually_disjoint f :=
  (forall i j, inc i (domain f) -> inc j (domain f) ->
    i = j \/ (disjoint (Vg f i) (Vg f j))).

Definition partition_w y x:=
  (union y = x) /\
  (forall a b, inc a y -> inc b y -> disjointVeq a b).

Definition partition_s y x:= partition_w y x /\ (alls y nonempty).

Definition partition_w_fam f x:=
  [/\ fgraph f, mutually_disjoint f & unionb f = x].

Definition partition_s_fam f x:=
  partition_w_fam f x /\ nonempty_fam f.

Lemma mutually_disjoint_prop f:
  (forall i j y, inc i (domain f) -> inc j (domain f) ->
    inc y (Vg f i) -> inc y (Vg f j) -> i = j) ->
  mutually_disjoint f.
Proof.
move=> hyp i j idf jdf; mdi_tac nij => u ui uj; case: nij; exact: (hyp _ _ u).
Qed.

Lemma mutually_disjoint_prop1 f: function f ->
  (forall i j y, inc i (source f) -> inc j (source f) ->
    inc y (Vf f i) -> inc y (Vf f j) -> i = j) ->
  mutually_disjoint (graph f).
Proof.
by move=> ff hyp; apply: mutually_disjoint_prop; rewrite f_domain_graph.
Qed.

Lemma mutually_disjoint_prop2 x f:
  (forall i j y, inc i x -> inc j x ->
    inc y (f i) -> inc y (f j) -> i = j) ->
  mutually_disjoint (Lg x f).
Proof.
move=> hyp; apply: mutually_disjoint_prop. bw.
by move=> i j y ix jy; bw; apply: hyp.
Qed.

Lemma partition_same y x:
  partition_w y x -> partition_w_fam (identity_g y) x.
Proof.
move=> [un di]; hnf; rewrite setUb_identity.
split => //; first (by apply: identity_fgraph).
hnf; rewrite identity_d; move=> i j iy jy.
by do 2 rewrite identity_ev //; apply: di.
Qed.

Lemma partition_same2 y x:
  partition_w_fam y x -> partition_w (range y) x.
Proof.
move=> [fg md uyx]; split; first by rewrite - setUb_alt.
move=> a b /(range_gP fg) [u ud ->] /(range_gP fg) [v vd ->].
by case: (md _ _ ud vd) ;[ move=>->|]; [left | right].
Qed.

Lemma partitions_is_covering y x:
  partition_w y x -> covering_s y x.
Proof. by move=> [u d] a ax; ue. Qed.

Lemma partition_fam_is_covering y x:
  partition_w_fam y x -> covering y x.
Proof. move=> [fg md uyx];split=>//; rewrite uyx; fprops. Qed.

If f is a partition of x each element of x is uniquely V i f

Definition cover_at f y := select (fun i => inc y (Vg f i)) (domain f).

Lemma cover_at_in f x y (i := cover_at f y):
  partition_w_fam f x -> inc y x ->
  (inc y (Vg f i) /\ inc i (domain f)).
Proof.
move=> [fg md ufx] yx; apply: select_pr.
  by move: yx; rewrite - ufx; move/setUb_P.
move=> k j id yif jd yjf.
have yi: (inc y ((Vg f k) \cap (Vg f j))) by fprops.
case: (md k j id jd)=>// di;empty_tac1 y.
Qed.

Lemma cover_at_pr f x y i:
   partition_w_fam f x -> inc i (domain f) -> inc y (Vg f i) ->
   cover_at f y = i.
Proof.
move => h idf yv.
move: (h)=> [q1 q2 q3].
have zx: inc y x by rewrite -q3; union_tac.
move: (cover_at_in h zx) => [q4 q5].
case: (q2 _ _ q5 idf) => // di; empty_tac1 y.
Qed.

Lemma same_cover_at f x y z (i := cover_at f y):
  partition_w_fam f x -> inc y x -> inc z (Vg f i) -> cover_at f z = i.
Proof.
move => h yx zi.
move: (cover_at_in h yx); rewrite -/i; move => [pa pb].
apply: (cover_at_pr h pb zi).
Qed.

coarser is an ordering of partitions

Lemma coarserT: transitive_r coarser_cs.
Proof.
move=> z x y c1 c2 u uy.
move: (c2 _ uy)=> [v zy uz]; move: (c1 _ zy)=> [t ty zt].
by ex_tac; apply: (sub_trans uz zt).
Qed.

Lemma coarserR: reflexive_r coarser_cs.
Proof. by move=> s x xy; ex_tac. Qed.

Lemma coarserA x:
  {when partition_s ^~ x &, antisymmetric_r coarser_cs}.
Proof.
suff: (forall y y', partition_s y x -> partition_s y' x ->
       coarser_cs y y' -> coarser_cs y' y -> sub y y').
  move=> hyp u v p1 p2 c1 c2.
  apply: extensionality; first apply: (hyp _ _ p1 p2 c1 c2).
  by apply: (hyp _ _ p2 p1 c2 c1).
move=> y y' [p1 ne] _ c1 c2 t ty.
move: (c2 _ ty) => [b biy tb]; move: (c1 _ biy) => [a ay ba].
move: (ne _ ty)=> [z zt].
case: ((proj2 p1) _ _ ty ay) => eq; last by empty_tac1 z.
have -> //: t = b by apply: extensionality=>//; rewrite eq.
Qed.

We consider that function that associates x to a and y to anything else. This is generally defined on doubleton a b

Definition variant a x y := (fun z:Set => Yo (z = a) x y).
Definition variantL a b x y := Lg (doubleton a b) (variant a x y).

Lemma variant_true a x y z:
  z = a -> variant a x y z = x.
Proof. by move=> za; rewrite /variant Y_true. Qed.

Lemma variant_false a x y z:
  z <> a -> variant a x y z = y.
Proof. by move=> za; rewrite /variant Y_false. Qed.

We consider here the functions that maps elements of a to x, anything else to y

Definition varianti x a b := fun z => Yo (inc z x) a b.

Lemma varianti_in z x a b: inc z x -> (varianti x a b z) = a.
Proof. by move=> zx; rewrite /varianti; Ytac0. Qed.

Lemma varianti_out z x a b: ~ inc z x -> (varianti x a b z) = b.
Proof. by move=> zx; rewrite /varianti; Ytac0. Qed.

Lemma variant_V_a a b x y: Vg (variantL a b x y) a = x.
Proof. by rewrite /variantL; bw; fprops; apply: variant_true. Qed.

Lemma variant_V_b a b x y: b <> a -> Vg (variantL a b x y) b = y.
Proof. by rewrite /variantL;bw; fprops; apply: variant_false. Qed.

Lemma variant_fgraph a b x y: fgraph (variantL a b x y).
Proof. rewrite/variantL;fprops. Qed.

Lemma variant_d a b x y: domain (variantL a b x y) = doubleton a b.
Proof. rewrite/variantL; bw. Qed.

Definition variantLc f g:= variantL C0 C1 f g.

Lemma variantLc_fgraph x y: fgraph (variantLc x y).
Proof. rewrite/variantLc/variantL; fprops. Qed.

Hint Resolve variant_fgraph variantLc_fgraph: fprops.

Lemma variantLc_d f g: domain (variantLc f g) = C2.
Proof. rewrite/variantLc/variantL; bw. Qed.

Hint Rewrite variantLc_d: bw.

Lemma variantLc_domain_ne f g: nonempty (domain (variantLc f g)).
Proof. bw; exists C0; fprops. Qed.

Lemma variant_V_ca x y: Vg (variantLc x y) C0 = x.
Proof. by rewrite /variantLc/variantL; bw;[ apply: variant_true |fprops]. Qed.

Lemma variant_V_cb x y: Vg (variantLc x y) C1 = y.
Proof.
rewrite /variantLc/variantL; bw;[ apply: variant_false;apply: TP_ne1 |fprops].
Qed.

Hint Rewrite variant_V_ca variant_V_cb: bw.

Ltac try_lvariant u:= move:u;move/C2_P; case => ->; bw.

Lemma variant_true1 x y: variant C0 x y C0 = x.
Proof. rewrite variant_true //. Qed.

Lemma variant_false1 x y: variant C0 x y C1 = y.
Proof. rewrite variant_false //; apply: TP_ne1. Qed.

Hint Rewrite variant_true1 variant_false1 : bw.

Lemma variantLc_comp a b f:
 variantLc (f a) (f b) =
  Lg (domain (variantLc a b))(fun z => f (Vg (variantLc a b) z)).
Proof.
apply: fgraph_exten; fprops; bw.
move=> x xtp; try_lvariant xtp; fprops.
Qed.

We have a partition of a set by selecting a subset and its complement

Definition partition_with_complement x j :=
  variantLc j (x -s j).

Lemma is_partition_with_complement x j:
  sub j x -> partition_w_fam (partition_with_complement x j) x.
Proof.
rewrite /partition_with_complement=> jx; split.
    by apply: variantLc_fgraph.
  move=> a b; bw;case /C2_P => -> ;case /C2_P => ->; fprops;
  right; bw; [ | apply (disjoint_S)];apply:set_I2Cr.
by rewrite/unionb /variantLc variant_d setUf2f; bw; apply:setU2_Cr.
Qed.

Greatest and least partition for covering order

Definition greatest_partition x := fun_image x singleton.
Definition least_partition x := (singleton x).

Lemma least_is_partition x:
   nonempty x -> partition_s (least_partition x) x.
Proof.
rewrite /least_partition=>ne.
split; last by move=> a /set1_P ->.
split; first by apply: setU_1.
by move=> a b /set1_P -> /set1_P ->; left.
Qed.

Lemma greatest_partition_P x z:
  inc z (greatest_partition x) <-> exists2 w, inc w x & z = singleton w .
Proof. apply/funI_P. Qed.

Lemma greatest_is_partition x: partition_s (greatest_partition x) x.
Proof.
split; last by move=> a /greatest_partition_P [w wx ->]; apply: set1_ne.
split.
  set_extens t.
    move /setU_P => [y yt /greatest_partition_P [w wx swy]].
    by move: yt; rewrite swy; move/set1_P => ->.
  move=> tx; apply/setU_P;exists (singleton t); fprops.
  apply /greatest_partition_P; ex_tac.
move=> a b/greatest_partition_P [w wx] -> /greatest_partition_P [w' wx'] ->.
mdi_tac ww => u /set1_P -> /set1_P sw; case: ww; ue.
Qed.

A strict partition is an injective functional graph

Definition injective_graph f:=
  fgraph f /\ {inc domain f &, injective (Vg f)}.

Lemma injective_partition f x:
  partition_s_fam f x -> injective_graph f.
Proof.
move=> [[fgf md ux] hyp]; split=>//.
move=> a b ad bd sV; move: (md _ _ ad bd) (hyp _ bd)=> [] //.
rewrite /disjoint sV setI2_id => -> [_ [[]]].
Qed.

Lemma partition_fam_partition f x:
  partition_s_fam f x -> partition_s (range f) x.
Proof.
move=> [pf hyp]; move: (partition_same2 pf)=> [ur di].
move:pf=> [fgf md _]; split=>//.
move=> a /(rangeP (proj1 fgf)) [b bf]; move: (pr2_V fgf bf); aw => ->.
apply: hyp;ex_tac.
Qed.

Lemma inv_image_disjoint g : function g ->
  {compat (inv_image_by_fun g) : x y / disjoint x y}.
Proof.
move=> fg x y dxy; rewrite /disjoint -iim_fun_setI2 //.
by apply /set0_P => t /iim_fun_P [u]; rewrite dxy => /in_set0.
Qed.

Given a partition, a function on each subset can be uniquely extended; We give two variants, in one case the targets may be different

Lemma extension_partition_aux f x t h:
  partition_w_fam f x ->
  (forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) ->
  (forall i j, inc i (domain f) -> inc j (domain f) ->
    agrees_on ((Vg f i) \cap (Vg f j)) (h i) (h j)).
Proof.
move=> [fgf mdf ufx] afp.
move=> i j id jd; case: (mdf _ _ id jd).
  move=> ->; rewrite setI2_id; move: (afp _ jd)=> [_ shj _].
  red; rewrite shj; split;fprops => s //.
rewrite/disjoint=> ->; red; split; try split; fprops.
by move=> a /in_set0.
Qed.

Lemma extension_partition1 f x t h (g := common_ext f h t):
  partition_w_fam f x ->
  (forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) ->
  (function_prop g x t /\
    (forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i))).
Proof.
move => pfa afp.
move: (extension_partition_aux pfa afp) => aah.
move: (extension_covering afp aah).
by move: pfa => [fgf mdf ufx]; rewrite -/g - ufx; move => [h1 _ h2 h3].
Qed.

Lemma extension_partition2 f x t h
  (g:= common_ext f (fun i => (triple (Vg f i) t (graph (h i)))) t):
  partition_w_fam f x ->
  (forall i, inc i (domain f) -> function_prop_sub (h i) (Vg f i) t) ->
  ( function_prop g x t /\
    forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i)).
Proof.
move=> pf prop.
pose nh i := triple (Vg f i) t (graph (h i)).
have afp: forall i, inc i (domain f) -> function_prop (nh i) (Vg f i) t.
  move=> i id; move: (prop _ id) => [fgh sg th];rewrite /nh;split; aw.
  apply: function_pr; fprops.
    by apply: sub_trans th; apply: f_range_graph.
  by rewrite f_domain_graph.
move: (extension_partition1 pf afp).
move => [fpg aag]; split=>//.
move=> i idf; move: (aag _ idf)=> [aa cc bb];split=>//.
  by move: (prop _ idf) => [_ -> _]; fprops.
move=> a aV; move: (bb _ aV) => ->; rewrite /nh /Vf; aw.
Qed.

Theorem extension_partition_thm f x t h:
  partition_w_fam f x ->
  (forall i, inc i (domain f) -> function_prop (h i) (Vg f i) t) ->
  exists! g, (function_prop g x t /\
    (forall i, inc i (domain f) -> agrees_on (Vg f i) g (h i))).
Proof.
move => pfa afp.
move: (extension_partition_aux pfa afp) => aah.
move: pfa => [fgf mdf <-]; exact: (extension_covering_thm afp aah fgf).
Qed.

EII-4-8 Sum of a family of sets

Given a family X, we construct a family Y that satisfies the previous theorem; the unionb Y is called the disjoint union

Definition disjointU_fam f := Lg (domain f)(fun i => (Vg f i) *s1 i).
Definition disjointU f := unionb (disjointU_fam f).

Lemma disjointU_disjoint f:
  mutually_disjoint (disjointU_fam f).
Proof.
move=> i j; rewrite /disjointU_fam Lg_domain=> id jd; bw.
by mdi_tac t => u /indexed_P [_ _] qu /indexed_P [_ _]; rewrite qu.
Qed.

Hint Resolve disjointU_disjoint: fprops.

Lemma disjointU_fgraph f: fgraph (disjointU_fam f).
Proof. rewrite /disjointU_fam; fprops. Qed.

Lemma disjointU_d f: domain (disjointU_fam f) = domain f.
Proof. rewrite /disjointU_fam; bw. Qed.

Hint Resolve disjointU_fgraph: fprops.

Theorem disjoint_union_lemma f:
  exists g x,
    [/\ fgraph g, x = unionb g,
    (forall i, inc i (domain f) -> (Vg f i) \Eq (Vg g i))
    & mutually_disjoint g].
Proof.
exists (disjointU_fam f), (disjointU f); split;fprops.
move=> i idf; rewrite /disjointU_fam; bw; apply:equipotent_indexed.
Qed.

Lemma partition_disjointU f:
  partition_w_fam (disjointU_fam f) (disjointU f).
Proof.
split; [fprops | by apply: disjointU_disjoint | done ].
Qed.

Lemma disjointU_hi f x: inc x (disjointU f) ->
  [/\ inc (Q x) (domain f), inc (P x) (Vg f (Q x)) & pairp x].
Proof.
move/setUb_P => [t]; rewrite disjointU_d => td.
by rewrite /disjointU_fam; bw; move /indexed_P => [pa pb ->].
Qed.

Lemma disjointU_P f x: inc x (disjointU f) <->
  [/\ inc (Q x) (domain f), inc (P x) (Vg f (Q x)) & pairp x].
Proof.
split; first by apply: disjointU_hi.
move => [pa pb pc]; apply/setUb_P; rewrite disjointU_d; ex_tac.
rewrite /disjointU_fam; bw; rewrite - {1} pc; apply/setXp_i; fprops.
Qed.

Lemma disjointU_pi f x y:
  inc y (domain f) -> inc x (Vg f y) ->
  inc (J x y) (disjointU f).
Proof. move => ta tb;apply/disjointU_P; aw; split; fprops. Qed.

Lemma disjointU2_rw a b x y: y <> x ->
  disjointU (variantL x y a b) = (a *s1 x) \cup (b *s1 y).
Proof.
move=> yx.
rewrite/disjointU /disjointU_fam.
have dv: domain (variantL x y a b) = doubleton x y by rewrite/ variantL; bw.
set_extens z; rewrite dv.
  move/setUb_P; bw; move => [u ud]; bw; move/setX_P => [pz Pz Qz].
  rewrite -pz; move/set1_P: Qz ->; apply/setU2_P; move: Pz.
  case /set2_P: ud=> ->; rewrite ?variant_V_a ? (variant_V_b _ _ yx);
    [left | right]; apply: setXp_i => //; fprops.
move=> h.
have Qz: (inc (Q z) (doubleton x y)).
  case /setU2_P :h => /setX_P [_ _] /set1_P ->; fprops.
apply/setUb_P; bw; exists (Q z); bw.
by case/setU2_P: h => /setX_P [pz Pz w]; move/set1_P: (w) ->;
  apply: setX_i; fprops; rewrite ?variant_V_a ? variant_V_b.
Qed.

Lemma disjointU2_rw1 a b:
  disjointU (variantLc a b) = (a *s1 C0) \cup (b *s1 C1).
Proof. rewrite/variantLc disjointU2_rw //; fprops. Qed.

There is a canonical mapping from the disjoint union onto the union; It is bijective if the family is disjoint

Theorem disjointU_pr f
  (h := fun i => Lf P ((Vg f i) *s1 i) (unionb f))
  (g := common_ext (disjointU_fam f) h (unionb f)):
  [/\ source g = disjointU f,
    target g = unionb f,
    surjection g &
    (mutually_disjoint f -> bijection g)].
Proof.
set aux:= (Lg (domain f) (fun i => (Vg f i) *s1 i)).
move: (partition_disjointU f) =>pf.
have da: (domain aux = domain f) by rewrite /aux; bw.
have tap: forall i, inc i (domain aux) -> lf_axiom P ((Vg f i) *s1 i)(unionb f).
  by move => i id x; move/setX_P=> [_ pv Qi]; union_tac; ue.
have fpi: (forall i, inc i (domain aux) ->
    function_prop (h i) (Vg aux i)(unionb f)).
  move=> i id; hnf;rewrite /h/aux; aw; bw; last by ue.
  split => //; by apply: lf_function; apply: tap.
move:(extension_partition1 pf fpi).
rewrite -/g; move => [fpg aag].
move: aag; bw; rewrite/disjointU_fam; bw; move=> aag.
move: fpg=> [fg sg tg].
have sug: (surjection g).
  apply: surjective_pr5=>//; rewrite /related.
  rewrite tg sg; move=> y; move /setUb_P=> [z zdf yg].
  set (t:= J y z).
  have tsg: inc t (disjointU f) by rewrite /t; apply: disjointU_pi.
  exists t => //.
  suff: y = Vf g t by move=>->; apply: Vf_pr3 =>//; rewrite sg.
  have ps: inc t ((Vg f z) *s1 z) by rewrite /t/indexed ; aw; fprops.
  move: (aag _ zdf); bw.
  rewrite /agrees_on; move=> [_ _ sv]; move: (sv _ ps).
  rewrite /h; aw.
    by move=> ->; rewrite /t; aw.
    by apply: tap; ue.
split=>//.
move=> mf; split=>//; split => //.
move=> x y; rewrite sg; move=> xsg ysg.
move: (disjointU_hi xsg)=> [qxd pV xp].
move: (disjointU_hi ysg)=> [qyd pyV yp].
move: (aag _ qxd); bw; move=> [ _ _ ax].
move: (aag _ qyd); bw; move=> [ _ _ ay].
have xs: inc x ((Vg f (Q x)) *s1 (Q x)) by apply: setX_i; fprops.
have ys: inc y ((Vg f (Q y)) *s1 (Q y)) by apply: setX_i; fprops.
rewrite (ax _ xs) (ay _ ys).
rewrite/h ;aw ; fprops; try apply: tap; try rewrite da=>//.
move=> sp;move: (mf _ _ qxd qyd).
case=> sq; [by apply: pair_exten | by empty_tac1 (P x);rewrite sp].
Qed.

Definition canonical_du2 a b := disjointU (variantLc a b).

Lemma candu2_rw a b:
  canonical_du2 a b = (a *s1 C0) \cup (b *s1 C1).
Proof. by rewrite /canonical_du2 disjointU2_rw1. Qed.

Lemma candu2P a b x:
  inc x (canonical_du2 a b) <-> (pairp x /\
  ((inc (P x) a /\ Q x = C0) \/ (inc (P x) b /\ Q x = C1))).
Proof.
rewrite candu2_rw; split.
  case /setU2_P; move /indexed_P => [pa pb]; fprops.
by move => [pa [] [h1 h2]]; apply/setU2_P; [left | right ]; apply /indexed_P.
Qed.

Lemma candu2_pr2 a b x:
  inc x (canonical_du2 a b) -> (Q x = C0 \/ Q x = C1).
Proof. by move /candu2P => [_]; case => [] [_]; [left | right]. Qed.

Lemma candu2_pra a b x:
  inc x a -> inc (J x C0) (canonical_du2 a b).
Proof. by move=> xa; apply /candu2P; split;fprops; left; aw. Qed.

Lemma candu2_prb a b x:
  inc x b -> inc (J x C1) (canonical_du2 a b).
Proof. by move => xb; apply /candu2P; split; fprops ; right; aw. Qed.

EII-5 Product of a family of sets

EII-5-1 The axiom of the set of subsets

Bourbaki has an axiom (not needed here) that says that the powerset exists
Canonical extension of f:E->F to powerset E -> powerset F

Definition extension_to_parts f :=
  Lf (image_by_fun f) (powerset (source f)) (powerset (target f)).

Lemma etp_axiom f: correspondence f ->
  lf_axiom (image_by_fun f) (powerset (source f)) (powerset (target f)).
Proof.
move=> cf x; move/setP_P => xs; apply/setP_P.
apply: (@sub_trans (range (graph f))); fprops; apply: dirim_Sr.
Qed.

Lemma etp_f f: correspondence f -> function (extension_to_parts f).
Proof.
move => cf; apply: lf_function;by apply: etp_axiom.
Qed.

Lemma etp_V f x:
  correspondence f -> sub x (source f)
  -> Vf (extension_to_parts f) x = image_by_fun f x.
Proof.
by rewrite /extension_to_parts=> cf s; aw; [apply: etp_axiom | apply/setP_P ].
Qed.

Hint Resolve etp_f : fprops.

Morphism properties of extension

Lemma etp_composable f g:
  composableC g f ->
  (extension_to_parts g) \coP (extension_to_parts f).
Proof.
move=> [cf cg cfg]; split; fprops.
rewrite /extension_to_parts;aw; ue.
Qed.

Lemma etp_compose:
  {when: composableC, {morph extension_to_parts: x y / x \co y }}.
Proof.
move=> g f /= cgf.
move: (etp_composable cgf)=>cegf.
move: cgf=> [cf cg cfg].
have ccg: (correspondence (g \co f)) by apply: compf_correspondence.
symmetry;apply: function_exten; try (fct_tac; fprops); fprops.
    by rewrite /extension_to_parts; aw.
  by rewrite /extension_to_parts; aw.
aw;move => x xs.
have xs1: sub x (source f).
  by move: xs;rewrite /extension_to_parts; aw; move/setP_P.
have xs2: sub x (source (g \co f)) by aw.
symmetry; aw; do 3 rewrite etp_V=>//.
  rewrite /compose/image_by_fun ; aw; apply:compg_image.
rewrite cfg /image_by_fun; apply: (@sub_trans (range (graph f))); fprops.
apply: dirim_Sr.
Qed.

Lemma etp_identity x:
  extension_to_parts (identity x) = identity (powerset x).
Proof.
move:(@identity_corresp x)=> ic.
apply: function_exten; fprops; try solve [rewrite/extension_to_parts; aw].
move=> y /=; rewrite {1} /extension_to_parts; aw => ys1.
move /setP_P: (ys1) => ys2.
have ys: sub y (source (identity x)) by aw; apply/setP_P.
have fi: (function (identity x)) by fprops.
rewrite etp_V // identity_V //; set_extens t.
  by move /(Vf_image_P fi ys) => [u uy]; bw; [ move => -> | apply: ys2].
move => ty;apply /(Vf_image_P fi ys); ex_tac; bw; fprops.
Qed.

Lemma composable_for_function f g:
  g \coP f -> composableC g f.
Proof. by move=> [[ fg _ _] [ff _ _ ] eq]. Qed.

Theorem etp_fs f: surjection f -> surjection (extension_to_parts f).
Proof.
move=> sf; apply: surj_if_exists_right_inv.
have [r [cfr cfri]]:= (exists_right_inv_from_surj sf).
have cfr' := (composable_for_function cfr).
exists (extension_to_parts r); split; first by apply: etp_composable.
rewrite - etp_compose // cfri etp_identity /extension_to_parts; aw.
Qed.

Theorem etp_fi f: injection f -> injection (extension_to_parts f).
Proof.
move=> inf.
case: (emptyset_dichot (source f))=> eq.
  move: inf=> [[ cf _] _]; split; fprops.
  rewrite {1 2} /extension_to_parts=> x y.
  by rewrite lf_source eq setP_0; move /set1_P => -> /set1_P ->.
have [r [cfr cfri]] := (exists_left_inv_from_inj inf eq).
have cfr' := (composable_for_function cfr).
apply: inj_if_exists_left_inv.
exists (extension_to_parts r); split; first by apply: etp_composable.
rewrite - etp_compose // cfri etp_identity /extension_to_parts; aw.
Qed.

EII-5-2 Set of mappings of one set into another

The set of functional graphs is denoted by F^E, the set of functions by calF(E; F)

Definition functions x y :=
  Zo (correspondences x y)
  (fun z => fgraph (graph z) /\ x = domain (graph z)).
Definition gfunctions x y:=
  Zo (powerset (x \times y))(fun z => fgraph z /\ x = domain z).
Definition permutations E :=
  Zo (functions E E) bijection.

Definition sub_functions x y :=
  unionf(powerset x)(functions ^~ y).

Lemma fun_set_P x y f:
  inc f (functions x y) <-> (function_prop f x y).
Proof.
rewrite/function; split.
  move/Zo_P => [/correspondences_P [p1 p2 p3] [p4 p5]]; split => //.
  split => //; ue.
by move=> [[qa qb qc] <- pc]; apply: Zo_i; [apply/correspondences_P | split].
Qed.

Lemma sfun_set_P x y f:
  inc f (sub_functions x y) <->
  [/\ function f, sub (source f) x & target f = y].
Proof.
split.
  move/setUf_P => [z /setP_P zx /fun_set_P [pa pb pc]];split => //; ue.
by move => [pa /setP_P pb pc]; apply /setUf_P; ex_tac; apply/fun_set_P.
Qed.

Lemma gfun_set_i f:
  function f -> inc (graph f) (gfunctions (source f) (target f)).
Proof. by move=> [[pa pd] pb pc]; apply: Zo_i => //; apply/setP_P. Qed.

Lemma gfun_set_hi x y z:
  inc z (gfunctions x y) -> exists f,
    [/\ function f, source f = x, target f = y & graph f = z].
Proof.
move/Zo_P => [/setP_P /corr_propcc [_ _ pa] [pb pc]].
exists (triple x y z); aw; split => // ; apply: function_pr=>//.
Qed.

Lemma function_exten5 x y a b:
  inc a (functions x y) -> inc b (functions x y) ->
  graph a = graph b -> a = b.
Proof.
move /fun_set_P=> [fa sa ta] /fun_set_P [fb sb tb] sg.
apply: function_exten1=>//; ue.
Qed.

Lemma fun_set_small_source y: small_set (functions emptyset y).
Proof.
move=> u v uf vf; apply: (function_exten5 uf vf).
move /fun_set_P: uf => [fa sa _]; move/fun_set_P: vf => [fb sb _].
rewrite !empty_source_graph //.
Qed.

Lemma fun_set_small_target x: small_set (functions x emptyset).
Proof.
move=> u v uf vf; apply: (function_exten5 uf vf).
move /fun_set_P: uf => [fa _ ta]; move/fun_set_P: vf => [fb _ tb].
rewrite !empty_target_graph//.
Qed.

Lemma fun_set_ne x y: (x = emptyset \/ nonempty y) -> nonempty (functions x y).
Proof.
case=> p.
  rewrite p;move: (empty_function_tg_function y) => h.
  by exists (empty_function_tg y); apply/fun_set_P.
move: p => [p py]; exists (constant_function x py); apply/fun_set_P.
apply constant_prop.
Qed.

Canonical isomorphism between calF(E,F) and F^E

Lemma graph_lf_axiom x y:
  lf_axiom graph (functions x y) (gfunctions x y).
Proof. by move=> g /fun_set_P [fg <- <-]; apply: gfun_set_i. Qed.

Lemma graph_fb x y:
  bijection (Lf graph (functions x y) (gfunctions x y)).
Proof.
apply: lf_bijective.
- by apply: graph_lf_axiom.
- by move=> u v us vs g; apply: (function_exten5 us vs g).
- move=> z zg ; move: (gfun_set_hi zg) => [f [pa pb pc pd]].
  by exists f => //;apply/fun_set_P.
Qed.

Lemma fun_set_equipotent x y:
  (functions x y) \Eq (gfunctions x y).
Proof. apply: (equipotent_aux (f:= graph)); aw; apply: graph_fb. Qed.

Isomorphism between calF(E,F) and calF(E',F') for equipotent sets

Definition compose3function u v :=
  Lf (fun f => (v \co f) \co u)
  (functions (target u) (source v))
  (functions (source u) (target v)).

Lemma c3f_axiom u v:
  function u -> function v ->
  lf_axiom (fun f => (v \co f) \co u)
  (functions (target u) (source v))
  (functions (source u) (target v)).
Proof.
move=> fu fv x; move /fun_set_P=> [fx sx tx]; apply/fun_set_P; aw.
split=> //; aw; fct_tac ;[fct_tac | aw].
Qed.

Lemma c3f_f u v:
  function u -> function v -> function (compose3function u v).
Proof. by move =>fu fv; apply: lf_function; apply: c3f_axiom. Qed.

Lemma c3f_V u v f:
  function u -> function v ->
  function f -> source f = target u -> target f = source v ->
  Vf (compose3function u v) f = (v \co f) \co u.
Proof.
rewrite /compose3function=> fu fv ff sf tf.
by aw; [apply: c3f_axiom=>// | apply/fun_set_P].
Qed.

Theorem c3f_fi u v:
  surjection u -> injection v -> injection (compose3function u v).
Proof.
rewrite /compose3function=> su iv.
have fu: function u by fct_tac.
have fv: function v by fct_tac.
apply: lf_injective; first by apply: c3f_axiom.
move=> f g.
case: (emptyset_dichot (source v)) => sve.
  by move=> i1 i2 c; apply: (fun_set_small_target (x:= target u)); ue.
move: (exists_right_inv_from_surj su) => [s [cus cusi]].
move: (exists_left_inv_from_inj iv sve).
move=> [r [crv crvi]] /fun_set_P [ff sf tf] /fun_set_P [fg sg tg] ceq.
have cvf: v \coP f by hnf.
have cvg: v \coP g by hnf.
have fvf: function (v \co f) by fct_tac.
have fvg: function (v \co g) by fct_tac.
have cvfu: (v \co f) \coP u by hnf; aw.
have cvgu: (v \co g) \coP u by hnf; aw.
move:(f_equal (fun i => i \co s) ceq).
rewrite - compfA // cusi - sf - (compf_s f v) compf_id_r //.
rewrite - compfA // cusi - sg - (compf_s g v) compf_id_r // => eq.
move: (f_equal (fun i => r \co i) eq).
rewrite compfA // crvi - tf compf_id_l //.
rewrite compfA // crvi - tg compf_id_l //.
Qed.

Theorem c3f_fs u v:
  (nonempty (source u) \/ (nonempty (source v)) \/ (nonempty (target v))
    \/ target u = emptyset) ->
  injection u -> surjection v -> surjection (compose3function u v).
Proof.
move=> nehyp iu sv.
have fu: function u by fct_tac.
have fv: function v by fct_tac.
move: (c3f_f fu fv); set (c3f:= compose3function u v) => c3ff.
split => //; rewrite /c3f/compose3function; aw => y ys.
case: (emptyset_dichot (source u)) => nesu.
  have p:(target u = emptyset \/ nonempty (source v)).
    case: nehyp.
      by rewrite nesu=> [] [h] [x]; case: x.
    case; [by right | case; last by left].
    by move=> [w wt]; move: (surjective_pr sv wt)=> [x xs _];right; ex_tac.
  have: (nonempty (functions (target u) (source v))).
    by apply: (fun_set_ne p).
  move=> [f fsp]; ex_tac; move/fun_set_P:(fsp) => [ff sf tf].
  rewrite c3f_V //.
  apply: (fun_set_small_source (y:=target v)); rewrite - nesu //.
  by apply: c3f_axiom.
move: (exists_right_inv_from_surj sv)=> [s [cvs cvsi]].
move: (exists_left_inv_from_inj iu nesu) => [r [cru crui]].
have Hb: function s by fct_tac.
have Hc: function r by fct_tac.
move/fun_set_P:ys=> [fy sy ty].
set (f:= (s \co y) \co r).
have sf: source f = target u by move: cru=> [_ _]; rewrite /f; aw.
have tf: target f = source v by move: cvs=> [_ _]; rewrite /f; aw.
have sytr: source y = target r by rewrite sy; move: (f_equal target crui); aw.
have tytr: source s = target y by rewrite ty; move: (f_equal source cvsi); aw.
have csy: s \coP y by [].
have fcyr: function (y \co r) by fct_tac.
have csyr: s \coP (y \co r) by hnf; aw.
have tcyr : (target (y \co r) = target v) by aw.
have fcsy: function (s \co y) by fct_tac.
have ff: function f by rewrite/f; fct_tac=>//; aw.
exists f; first by apply/fun_set_P.
rewrite c3f_V //.
rewrite/f -(@compfA s y r) // (@compfA v s (y \co r)) //.
rewrite cvsi -tcyr compf_id_l // -compfA //.
rewrite crui - sy compf_id_r //.
Qed.

Lemma c3f_fb u v:
  bijection u -> bijection v -> bijection (compose3function u v).
Proof.
move=> [iu su][iv sv]; split; first by apply: c3f_fi=>//.
apply: c3f_fs=>//.
case: (emptyset_dichot (target u)); first by right; right; right.
move=> [y yt]; move: (surjective_pr su yt)=> [x xs _]; left; ex_tac.
Qed.

Isomorphism between calF(BxC,A) and calF(C, calF(B,A)) and calF(B, calF(C,A))

Definition partial_fun_axiom f :=
  function f /\ exists a b, source f = a \times b.

Lemma partial_fun_axiom_pr f:
  partial_fun_axiom f ->
  source f = (domain (source f)) \times (range (source f)).
Proof.
move=> [ff [a [b sf]]]; rewrite sf.
case: (emptyset_dichot a); first by move => ->; rewrite setX_0l; bw.
case: (emptyset_dichot b); first by move => ->; rewrite setX_0r; bw.
by move=> h1 h2; bw.
Qed.

Definition first_partial_fun f y:=
  Lf (fun x => Vf f (J x y)) (domain (source f)) (target f).

Definition second_partial_fun f x:=
  Lf (fun y => Vf f (J x y)) (range (source f)) (target f).

Definition first_partial_function f:=
  Lf (fun y => first_partial_fun f y) (range (source f))
  (functions (domain (source f)) (target f)).

Definition second_partial_function f:=
  Lf (fun x => second_partial_fun f x) (domain (source f))
  (functions (range (source f)) (target f)).

Definition first_partial_map b c a:=
  Lf (fun f=> first_partial_function f)
  (functions (b \times c) a)
  (functions c (functions b a)).

Definition second_partial_map b c a:=
  Lf (fun f=> second_partial_function f)
  (functions (b \times c) a)
  (functions b (functions c a)).

Lemma fpf_axiom f y:
  partial_fun_axiom f -> inc y (range (source f)) ->
  lf_axiom (fun x => Vf f (J x y)) (domain (source f)) (target f).
Proof.
move=> pfa; move: (partial_fun_axiom_pr pfa)=> pfb.
move=> yr x xs; move: pfa=>[ff _]; Wtac;ue.
Qed.

Lemma spf_axiom f x:
  partial_fun_axiom f -> inc x (domain (source f)) ->
  lf_axiom (fun y => Vf f (J x y)) (range (source f)) (target f).
Proof.
move=> pfa; move: (partial_fun_axiom_pr pfa)=> pfb.
move=> yr t xs; move: pfa=>[ff _]; Wtac; ue.
Qed.

Lemma fpf_f f y:
  partial_fun_axiom f -> inc y (range (source f)) ->
  function (first_partial_fun f y).
Proof.
rewrite/first_partial_fun=> pfa yr.
by apply: lf_function; apply: fpf_axiom.
Qed.

Lemma spf_f f x:
  partial_fun_axiom f -> inc x (domain (source f)) ->
  function (second_partial_fun f x).
Proof.
rewrite/second_partial_fun=> pfa yr.
by apply: lf_function; apply: spf_axiom.
Qed.

Lemma fpf_V f x y:
  partial_fun_axiom f -> inc x (domain (source f)) ->
  inc y (range (source f)) ->
  Vf (first_partial_fun f y) x = Vf f (J x y).
Proof.
rewrite/first_partial_fun=> pfa xd yr.
by rewrite lf_V //; apply: fpf_axiom.
Qed.

Lemma spf_V f x y:
  partial_fun_axiom f -> inc x (domain (source f)) ->
  inc y (range (source f)) ->
  Vf (second_partial_fun f x) y = Vf f (J x y).
Proof.
rewrite/first_partial_fun=> pfa xd yr.
by rewrite lf_V //; apply: spf_axiom.
Qed.

Lemma fpfa_axiom f:
  partial_fun_axiom f ->
  lf_axiom (fun y => (first_partial_fun f y))(range (source f))
  (functions (domain (source f)) (target f)).
Proof.
move=> pfa x xr; apply /fun_set_P; rewrite /first_partial_fun;red; aw.
by split => //;apply: fpf_f.
Qed.

Lemma spfa_axiom f:
  partial_fun_axiom f ->
  lf_axiom (fun x => second_partial_fun f x) (domain (source f))
  (functions (range (source f)) (target f)).
Proof.
move=> pfa x xr; apply /fun_set_P;rewrite /second_partial_fun; red;aw.
split => //; by apply: spf_f.
Qed.

Lemma fpfa_f f:
  partial_fun_axiom f -> function (first_partial_function f).
Proof.
rewrite /first_partial_function=> fpa.
by apply: lf_function; apply: fpfa_axiom.
Qed.

Lemma spfa_f f:
 partial_fun_axiom f -> function (second_partial_function f).
Proof.
rewrite /second_partial_function=> fpa.
by apply: lf_function; apply: spfa_axiom.
Qed.

Lemma fpfa_V f y:
  partial_fun_axiom f -> inc y (range (source f)) ->
  Vf (first_partial_function f) y = first_partial_fun f y.
Proof.
rewrite /first_partial_function=> pfa yr.
by rewrite lf_V //; apply: fpfa_axiom.
Qed.

Lemma spfa_V f x:
  partial_fun_axiom f -> inc x (domain (source f)) ->
  Vf (second_partial_function f) x = second_partial_fun f x.
Proof.
rewrite /second_partial_function=> pfa yr.
by rewrite lf_V //; apply: spfa_axiom.
Qed.

Lemma fpfb_axiom a b c:
  nonempty b -> nonempty c ->
  lf_axiom (fun f=> first_partial_function f)
  (functions (b \times c) a)
  (functions c (functions b a)).
Proof.
move=> neb nec x; move/fun_set_P=>[fx sx tx]; apply/fun_set_P.
red;rewrite {2 3} /first_partial_function;aw; rewrite sx tx; bw.
by split => //; apply: fpfa_f; split=>//; rewrite sx;exists b, c.
Qed.

Lemma spfb_axiom a b c:
  nonempty b -> nonempty c ->
  lf_axiom (fun f=> second_partial_function f)
  (functions (b \times c) a)
  (functions b (functions c a)).
Proof.
move=> neb nec x; move/fun_set_P=>[fx sx tx]; apply/fun_set_P.
red;rewrite {2 3} /second_partial_function; aw; rewrite sx tx; bw.
by split => //; apply: spfa_f; split=>//; rewrite sx;exists b, c.
Qed.

Lemma fpfb_f a b c:
  nonempty a -> nonempty b -> function (first_partial_map a b c).
Proof.
by rewrite /first_partial_map=> nea neb;apply: lf_function; apply: fpfb_axiom.
Qed.

Lemma spfb_f a b c:
  nonempty a -> nonempty b -> function (second_partial_map a b c).
Proof.
by rewrite /second_partial_map=> nea neb; apply: lf_function; apply: spfb_axiom.
Qed.

Lemma fpfb_V a b c f:
  nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
  Vf (first_partial_map a b c) f = first_partial_function f.
Proof.
by rewrite/first_partial_map=> nea neb fs; aw; apply: fpfb_axiom.
Qed.

Lemma spfb_V a b c f:
  nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
  Vf (second_partial_map a b c) f = second_partial_function f.
Proof.
by rewrite/second_partial_map=> nea neb fs; aw; apply: spfb_axiom.
Qed.

Lemma fpfb_VV a b c f x:
  nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
  inc x (a \times b) ->
  Vf (Vf (Vf (first_partial_map a b c) f) (Q x)) (P x) = Vf f x.
Proof.
move=> nea neb fs xp; rewrite fpfb_V=>//.
move /fun_set_P: fs => [fs sf tf].
have pfaf: (partial_fun_axiom f) by split=>//; exists a, b.
move /setX_P: xp =>[xp px qx].
have qxr: (inc (Q x) (range (source f))) by rewrite sf; bw.
have pxr: (inc (P x) (domain (source f))) by rewrite sf; bw.
by rewrite fpfa_V // fpf_V // xp.
Qed.

Lemma spfb_VV a b c f x:
  nonempty a -> nonempty b -> inc f (functions (a \times b) c) ->
  inc x (a \times b) ->
  Vf (Vf (Vf (second_partial_map a b c) f) (P x)) (Q x) = Vf f x.
Proof.
move=> nea neb fs xp; rewrite spfb_V=>//.
move /fun_set_P: fs => [fs sf tf].
have pfaf: (partial_fun_axiom f) by split=>//; exists a, b.
move /setX_P: xp =>[xp px qx].
have qxr: (inc (Q x) (range (source f))) by rewrite sf; bw.
have pxr: (inc (P x) (domain (source f))) by rewrite sf; bw.
by rewrite spfa_V // spf_V // xp.
Qed.

Theorem fpfa_fb a b c:
  nonempty a -> nonempty b -> bijection (first_partial_map a b c).
Proof.
move=> nea neb.
set f:= _ a b c.
have sf:source f = functions (a \times b) c.
   by rewrite /f /first_partial_map; aw.
have tf: target f = functions b (functions a c)
  by rewrite /f /first_partial_map; aw.
have ff: function f by apply: (fpfb_f _ nea neb).
split.
  split=>//.
  move=> x y; rewrite sf=> xs ys eq.
  have sx: source x = a \times b by move /fun_set_P: xs => [_ ].
  have sy: source y = a \times b by move /fun_set_P: ys => [_ ].
  have ha: forall z, inc z (source x) -> Vf x z = Vf y z.
    rewrite sx => z zp.
    by rewrite -(fpfb_VV nea neb xs zp) -(fpfb_VV nea neb ys zp) eq.
  move: xs ys => /fun_set_P [fx _ tx] /fun_set_P [fy _ ty].
  by apply: function_exten=>//; try ue.
split=>//; move=> y yt.
set (g:= Lf (fun x => Vf (Vf y (Q x)) (P x)) (a \times b) c).
have ta: lf_axiom (fun x => Vf (Vf y (Q x) ) (P x)) (a \times b) c.
  move=> x /setX_P [xp pa qb].
  move: yt; rewrite tf; move /fun_set_P => [fy sy ty].
  have: (inc (Vf y (Q x)) (target y)) by Wtac.
  by rewrite ty; move /fun_set_P=> [fW sW <-]; Wtac.
have gsf: (inc g (source f)).
 by rewrite /g sf; apply /fun_set_P; red;aw; split => //; apply: lf_function.
ex_tac.
have: inc (Vf f g) (target f) by Wtac.
move:yt; rewrite tf;move=> /fun_set_P [fy sy ty] /fun_set_P [fW sW tw].
apply: function_exten=>//; try ue; move => x; rewrite sW=> xs.
have: inc (Vf (Vf f g) x) (target (Vf f g)) by Wtac.
have: inc (Vf y x) (target y) by Wtac.
rewrite tw ty; move=> /fun_set_P [fy1 sy1 ty1] /fun_set_P [fW1 sW1 tw1].
apply: function_exten=>//; try ue; rewrite sW1=> z zs.
have psg: (inc (J z x) (source g)) by rewrite /g; aw; fprops.
rewrite/g lf_source in psg; rewrite sf in gsf.
move: (fpfb_VV nea neb gsf psg); aw; move=> ->.
by rewrite /g lf_V; first by aw.
Qed.

Theorem spfa_fb a b c:
  nonempty a -> nonempty b -> bijection (second_partial_map a b c).
Proof.
move=> nea neb.
set f:= _ a b c.
have sf:source f = functions (a \times b) c.
   by rewrite /f /second_partial_map; aw.
have tf: target f = functions a (functions b c).
  by rewrite /f /second_partial_map; aw.
have ff: function f by apply: (spfb_f _ nea neb).
split.
  split=>//.
  move=> x y; rewrite sf=> xs ys eq.
  have sx: source x = a \times b by move /fun_set_P: xs => [_ ].
  have sy: source y = a \times b by move /fun_set_P: ys => [_ ].
  have ha: forall z, inc z (source x) -> Vf x z = Vf y z.
    rewrite sx => z zp.
    by rewrite -(spfb_VV nea neb xs zp) -(spfb_VV nea neb ys zp) eq.
  move: xs ys => /fun_set_P [fx _ tx] /fun_set_P [fy _ ty].
  by apply: function_exten=>//; try ue.
split=>//; move=> y yt.
pose (g:= Lf (fun x => Vf (Vf y (P x)) (Q x)) (a \times b) c).
have ta: lf_axiom (fun x => Vf (Vf y (P x)) (Q x)) (a \times b) c.
  move=> x /setX_P [xp pa qb].
  move: yt; rewrite tf; move /fun_set_P => [fy sy ty].
  have : (inc (Vf y (P x)) (target y)) by Wtac.
  by rewrite ty; move /fun_set_P=> [fW sW <-]; Wtac.
have gsf: (inc g (source f)).
 by rewrite /g sf; apply /fun_set_P; red;aw; split => //; apply: lf_function.
ex_tac.
have: inc (Vf f g) (target f) by Wtac.
move:yt; rewrite tf;move=> /fun_set_P [fy sy ty] /fun_set_P [fW sW tw].
apply: function_exten=>//; try ue; move => x; rewrite sW=> xs.
have: inc (Vf (Vf f g) x) (target (Vf f g)) by Wtac.
have: inc (Vf y x) (target y) by Wtac.
rewrite tw ty; move=> /fun_set_P [fy1 sy1 ty1] /fun_set_P [fW1 sW1 tw1].
apply: function_exten=>//; try ue; rewrite sW1=> z zs.
have psg: (inc (J x z) (source g)) by rewrite /g; aw; fprops.
rewrite/g lf_source in psg; rewrite sf in gsf.
move: (spfb_VV nea neb gsf psg); aw; move=> ->.
by rewrite /g lf_V; first by aw.
Qed.

End Bunion.
Export Bunion.

Module Bproduct.

EII-5-3 Definition of the product of a family of sets

We have two variants of the definitions of the product; z is a functional graph, with the same domain as f, and z(i) is in f(i). Note that f is not required to be a functional graph

Definition productb f:=
  Zo (powerset ((domain f) \times (unionb f)))
  (fun z => [/\ fgraph z, domain z = domain f
    & forall i, inc i (domain f) -> inc (Vg z i) (Vg f i)]).

Definition productf sf f:= productb (Lg sf f).

Lemma setXb_P f x:
  inc x (productb f) <->
  [/\ fgraph x, domain x = domain f &
    forall i, inc i (domain f) -> inc (Vg x i) (Vg f i)].
Proof.
split; first by move/Zo_P => [] //.
move => [pa pb pc]; apply: Zo_i => //; apply/setP_P => t tx.
have gx: (sgraph x) by fprops.
have aux: inc (P t) (domain f) by rewrite - pb; apply: domain_i1.
rewrite - (gx _ tx); apply: setXp_i => //.
by apply /setUb_P; ex_tac; rewrite (pr2_V pa tx); apply: pc.
Qed.

Lemma setXf_P sf f x:
  inc x (productf sf f) <->
  [/\ fgraph x, domain x = sf & forall i, inc i sf -> inc (Vg x i) (f i)].
Proof.
split.
  move/setXb_P; bw; move => [pa pb pc];split => //.
  move => i isf; move: (pc _ isf); bw.
move => [pa pb pc]; apply/setXb_P;bw;split => //.
by move => i isf; bw; apply: pc.
Qed.

Lemma setXb_exten f x x':
  inc x (productb f) -> inc x' (productb f) -> {inc (domain f), x =1g x'} ->
  x = x'.
Proof.
move=> /setXb_P [fx dx px] /setXb_P [fx' dx' px'] sv.
apply: fgraph_exten=>//; ue.
Qed.

Lemma setXf_exten sf f x x':
  inc x (productf sf f) -> inc x' (productf sf f) -> {inc sf, x =1g x'} ->
  x = x'.
Proof.
move => pa pb pc; apply: (setXb_exten pa pb); bw.
Qed.

This lemma says that we may always assume that x is a functional graph
Lemma productb_gr x: productb (Lg (domain x) (Vg x)) = productb x.
Proof.
set_extens t; move /setXb_P => [p1]; bw => p2 p3;apply /setXb_P; bw;
   split => // i idg; move: (p3 _ idg); bw.
Qed.

Lemma unionb_gr X : unionb (Lg (domain X) (Vg X)) = unionb X.
Proof.
set_extens t => /setUb_P; bw; move => [y ya]; bw => yb;
    apply/setUb_P;bw; ex_tac; bw.
Qed.

Projection function to component i

Definition pr_i f i:= Lf (Vg ^~ i) (productb f) (Vg f i).

Lemma pri_axiom f i:
  inc i (domain f) ->
  lf_axiom (Vg ^~ i) (productb f) (Vg f i).
Proof. by move=> id x /setXb_P [fx dx]; apply. Qed.

Lemma pri_f f i: inc i (domain f) -> function (pr_i f i).
Proof. by move=> id; apply: lf_function; apply: pri_axiom. Qed.

Lemma pri_V f i x:
  inc i (domain f) -> inc x (productb f) ->
  Vf (pr_i f i) x = Vg x i.
Proof. by rewrite/pr_i=> id xp; aw; apply: pri_axiom. Qed.

Hint Resolve pri_f : fprops.

Special case where the domain is empty

Lemma setXb_0 : productb emptyset = singleton emptyset.
Proof.
move: fgraph_set0 => h.
apply: set1_pr.
  by apply/setXb_P;split => //; rewrite domain_set0 => i /in_set0.
by move => z /setXb_P [_]; rewrite domain_set0; move/domain_set0_P.
Qed.

Lemma setXb_0' f: productb (Lg emptyset f) = singleton emptyset.
Proof. rewrite /Lg funI_set0; apply: setXb_0. Qed.

a product is empty iff all factors are empty

Lemma setXb_ne f: nonempty_fam f -> nonempty (productb f).
Proof.
move=> hyp.
exists (Lg (domain f)(fun i=> rep (Vg f i))).
by apply/setXb_P; split; fprops; bw => i id; bw; apply: rep_i; apply: hyp.
Qed.

Lemma setXb_ne2 f: nonempty (productb f) -> nonempty_fam f.
Proof.
move=> [x] /setXb_P [fg _ h i id]; move:(h _ id) => w; ex_tac.
Qed.

The set of graphs is a product

Lemma graphset_P1 a b z:
  inc z (gfunctions a b) <->
  [/\ fgraph z, domain z = a & sub z (a \times b)].
Proof.
split; first by move/Zo_P => [/setP_P pa [pb pc]].
move => [pa pb pc]; apply: Zo_i; [by apply/setP_P | done].
Qed.

Lemma graphset_P2 a b z:
  inc z (gfunctions a b) <->
  [/\ fgraph z, domain z = a & sub (range z) b].
Proof.
split; first by move/graphset_P1 => [pa pb] /corr_propcc [_ _ pc].
move => [pa pb pc]; apply/graphset_P1;split => //.
apply/corr_propcc;rewrite pb;split; fprops.
Qed.

Lemma setXb_sub_graphset f x:
  sub (unionb f) x ->
  sub (productb f) (gfunctions (domain f) x).
Proof.
move=> su t /setXb_P [ft dt hyp]; apply/graphset_P2;split => //.
move=> a /(range_gP ft) [b bt]->; apply: su.
rewrite dt in bt;union_tac.
Qed.

Lemma setXb_eq_graphset f x:
  (forall i, inc i (domain f) -> Vg f i = x) ->
  productb f = gfunctions (domain f) x.
Proof.
move=> prop; apply: extensionality.
  apply: setXb_sub_graphset =>//.
  by move=> y /setUb_P [z zd zV]; rewrite - (prop _ zd).
move=> y /graphset_P2 [fy dy sr]; apply/setXb_P;split => //.
move=> i id; rewrite (prop _ id); apply: sr.
rewrite - dy in id; fprops.
Qed.

Product of a single set

Definition product1 x a := productb (cst_graph (singleton a) x).

Lemma cst_graph_pr x y: productb (cst_graph x y) = gfunctions x y.
Proof.
have xd: x = domain (cst_graph x y) by bw.
rewrite xd - setXb_eq_graphset - xd // => i ix; bw.
Qed.

Lemma setX1_pr x a:
  product1 x a = gfunctions (singleton a) x.
Proof. apply: cst_graph_pr. Qed.

Lemma setX1_P x a y:
  inc y (product1 x a) <->
    [/\ fgraph y, domain y = singleton a & inc (Vg y a) x].
Proof.
apply: (iff_trans (setXf_P _ _ _)); split; move=> [pa pb pc];split => //.
  apply: pc; fprops.
by move => i /set1_P ->.
Qed.

Lemma setX1_pr2 f x: domain f = singleton x ->
  product1 (Vg f x) x = productb f.
Proof.
move=> df.
rewrite setX1_pr -df (setXb_eq_graphset (x:= (Vg f x))) //.
by rewrite df => i /set1_P ->.
Qed.

Canonical bijection between x and product1 x a

Definition product1_canon x a :=
  Lf (fun i => cst_graph (singleton a) i) x (product1 x a).

Lemma setX1_canon_axiom x a:
  lf_axiom (fun i => cst_graph (singleton a) i) x (product1 x a).
Proof. move=> y yx; apply /setX1_P;split; bw;fprops. Qed.

Lemma setX1_canon_f x a: function (product1_canon x a).
Proof. apply: lf_function; apply: setX1_canon_axiom. Qed.

Lemma setX1_canon_V x a i:
  inc i x -> Vf (product1_canon x a) i = cst_graph (singleton a) i.
Proof.
by rewrite /product1_canon=> iw; aw; apply: setX1_canon_axiom.
Qed.

Lemma setX1_canon_fb x a: bijection (product1_canon x a).
Proof.
apply: lf_bijective.
+ by apply: setX1_canon_axiom.
+ move=> u v ux vx eq; move: (f_equal (Vg ^~a) eq); bw; fprops.
+ move=> y /setX1_P [fy dy Vx]; ex_tac.
  rewrite -dy; apply: fgraph_exten; fprops; bw.
  by rewrite dy ;move=> z zd /=; bw; move /set1_P: zd => ->.
Qed.

A product of n sets (with n=2) is isomorphic to the product of two sets

Definition product2 x y := productf C2 (variant C0 x y).

Definition product2_canon x y :=
  Lf (fun z => (variantLc (P z) (Q z))) (x \times y) (product2 x y).

Lemma setX2_P x y z:
  inc z (product2 x y) <->
  [/\ fgraph z, domain z = C2 , inc (Vg z C0) x & inc (Vg z C1) y].
Proof.
split.
  move /(setXf_P) => [fa fb fc]; split => //.
    move: (fc _ inc_C0_2); bw; fprops.
  move: (fc _ inc_C1_2); bw; fprops.
move => [pa pb pc pd]; apply/(setXf_P); split ; bw => i ind; try_lvariant ind.
Qed.

Lemma setX2_canon_axiom x y:
  lf_axiom (fun z => variantLc (P z) (Q z))
  (x \times y) (product2 x y).
Proof. move=> t /setX_P [pt px qy]; apply/setX2_P;bw; split;fprops. Qed.

Lemma setX2_canon_f x y: function (product2_canon x y).
Proof. apply: lf_function; apply: setX2_canon_axiom. Qed.

Lemma setX2_canon_V x y z:
  inc z (x \times y) -> Vf (product2_canon x y) z = variantLc (P z) (Q z).
Proof. rewrite /product2_canon => zp; aw; by apply: setX2_canon_axiom. Qed.

Lemma product2_canon_fb x y:
  bijection (product2_canon x y).
Proof.
rewrite /product2_canon.
move: (setX2_canon_axiom (x:=x) (y:=y)) => pa.
apply: lf_bijective=>//.
  move => u v /setX_P [up pux quy] /setX_P [vp pvx qvy] eq.
  move: (f_equal (Vg ^~ C0) eq)(f_equal (Vg ^~ C1) eq); bw.
  by apply: pair_exten=>//.
move=> z /setX2_P [fz dz Va Vb].
exists (J (Vg z C0) (Vg z C1)); aw; first fprops.
symmetry;apply: fgraph_exten;fprops; bw;try ue.
move=> t td; try_lvariant td.
Qed.

The product of singletons is a singleton

Lemma setX_set1 f: (allf f singletonp) -> singletonp (productb f).
Proof.
move=> als; apply/singletonP; split.
  by apply: setXb_ne => i idf; move /singletonP: (als _ idf) => [].
move=> a b ap bp; apply: (setXb_exten ap bp)=> i id.
move /singletonP: (als _ id) => [ne eq]; apply: eq.
  by move/setXb_P: ap => [_ _ ]; apply.
by move/setXb_P: bp => [_ _ ]; apply.
Qed.

Some properties of constant graphs

Definition diagonal_graphp e i :=
  Zo (gfunctions i e) constantgp.

Lemma diagonal_graph_P e i x:
  inc x (diagonal_graphp e i) <->
  [/\ constantgp x, domain x = i & sub (range x) e].
Proof.
split; first by move /Zo_P => [] /graphset_P2 [pa pb pc] pd.
move => [pa pb pc]; apply/Zo_i => //; apply/graphset_P2; split => //.
by move: pa => [].
Qed.

Definition constant_functor i e:=
  Lf (fun x => cst_graph i x) e (gfunctions i e).

Lemma cf_injective i e:
  nonempty i -> injection (constant_functor i e).
Proof.
rewrite /constant_functor;move=> [x xi].
apply: lf_injective.
  move=> t te; rewrite /cst_graph; apply/graphset_P2.
  split; fprops; bw.
  by move=> y /Lg_range_P [b be ->].
move=> u v ue ve eq;move: (f_equal (Vg ^~ x) eq); bw.
Qed.

Change of variables in a product

Definition product_compose f u :=
  Lf (fun x => x \cg (graph u))
  (productb f) (productf (source u) (fun k => Vg f (Vf u k))).

Section ProductCompose.
Variables (f u: Set).
Hypotheses (bu: bijection u) (tudf: target u = domain f).

Lemma pc_axiom0 c
  (g:= ((triple (domain c) (range c) c)) \co u):
  inc c (productb f) ->
  [/\ function g, c \cg (graph u) = graph g &
    (forall i, inc i (source u) ->
    Vg (graph g) i = Vg c (Vg (graph u) i))].
Proof.
move=> /setXb_P [fc dc eq].
have fu: function u by fct_tac.
have cg: (c \cg (graph u) = graph g) by rewrite/g /compose; aw.
have fg: function g.
  by rewrite/g; fct_tac; [ apply: function_pr; fprops| aw; ue].
split=>//.
move=> i iu; rewrite/g/compose; aw.
have id: inc i (domain (c \cg graph u)) by rewrite cg /g; fprops; aw.
have fgc: fgraph (c \cg graph u) by ue.
have fgv: fgraph (graph u) by fprops.
move/(compg_pP):(fdomain_pr1 fgc id) => [y Jv Ju].
move:(pr2_V fgv Jv); aw => <-.
move:(pr2_V fc Ju); aw.
Qed.

Lemma pc_axiom:
  lf_axiom (fun x => x \cg (graph u))
     (productb f) (productf (source u) (fun k => Vg f (Vf u k))).
Proof.
move=> x xp; move: (pc_axiom0 xp) => [fg cg VV].
have fu: function u by fct_tac.
apply/setXb_P; [ rewrite cg; split; bw; [ fprops | aw; bw | ]].
move => i isu;bw; rewrite (VV _ isu) -/(Vf u i).
move /setXb_P: xp => [_ _]; apply; Wtac.
Qed.

Lemma pc_f: function (product_compose f u).
Proof. by apply: lf_function; apply: pc_axiom. Qed.

Lemma pc_V x: inc x (productb f) ->
   Vf (product_compose f u) x = x \cg (graph u).
Proof. by rewrite /product_compose=> xp; aw; apply: pc_axiom. Qed.

Lemma pc_VV x i:
  inc x (productb f) -> inc i (source u) ->
   Vg (Vf (product_compose f u) x) i = Vg x (Vf u i).
Proof.
move=> xp iu; rewrite pc_V //; move:(pc_axiom0 xp) => [fg -> ->] //.
Qed.

Lemma pc_fb: bijection (product_compose f u).
Proof.
move: (pc_f)=> fpc.
have su: surjection u by move: bu=> [_].
have spc: (source (product_compose f u) = productb f).
  by rewrite /product_compose; aw.
split.
  split=>//.
  rewrite spc=> x y xs ys eq.
  apply: (setXb_exten xs ys).
  rewrite -tudf; move=> i iu; move: ((proj2 su) _ iu) => [z zs <-].
  by rewrite - (pc_VV xs zs) -(pc_VV ys zs) eq.
split => //.
set nf:= Lg (source u) (fun k => Vg f (Vf u k)).
have tpc:target (product_compose f u) = productb nf.
  rewrite /product_compose; aw.
rewrite tpc spc => y yp.
set x:= Lg (domain f) (fun i => Vg y (Vf (inverse_fun u) i)).
have xp: (inc x (productb f)).
  apply /setXb_P; rewrite /x; bw; split; fprops.
  move=> i id; bw.
  rewrite -tudf in id; move: ((proj2 su) _ id) => [z zsu wz].
  rewrite -wz (inverse_V2 bu zsu).
  move/setXb_P: yp => [fy dy iVV].
  by move: (iVV z); rewrite /nf; bw; apply.
ex_tac.
have Wt: inc (Vf (product_compose f u) x) (productb nf).
  by rewrite - spc in xp; move: (Vf_target fpc xp); rewrite tpc.
apply: (setXb_exten Wt yp) => i; rewrite /nf; bw=> id.
have Wd: inc (Vf u i)(domain f) by rewrite -tudf; Wtac; fct_tac.
rewrite pc_VV // (LVg_E _ Wd) (inverse_V2 bu id) //.
Qed.

End ProductCompose.

EII-5-4 Partial products

a partial product is the set of restrictions

Lemma restriction_graph2 f j:
  fgraph f -> sub j (domain f) ->
  Lg j (Vg f) = f \cg (diagonal j).
Proof.
move=> fgj sj.
rewrite diagonal_is_identity - compg_composef.
  by rewrite/composef identity_d; apply: Lg_exten => i idx; rewrite identity_ev.
red;rewrite identity_r;split => //; apply: identity_fgraph.
Qed.

Product of f, with indices restricted to j

Definition restriction_product f j := productb (Lg j (Vg f)).
Definition pr_j f j :=
  Lf (fun z => restr z j) (productb f)(restriction_product f j).

Section RestrictionProduct.
Variables (f j: Set).
Hypothesis (jdf: sub j (domain f)).

Lemma restriction_productE :
  restriction_product f j = productb (restr f j).
Proof. done. Qed.

Lemma prj_axiom:
  lf_axiom (fun z => restr z j)
  (productb f)(restriction_product f j).
Proof.
rewrite /restriction_product=> x /setXb_P [fx dx iVV].
have sx: sub j (domain x) by rewrite dx.
apply/setXb_P; bw; split; fprops.
by move=> i ij; bw; apply: iVV; apply: jdf.
Qed.

Lemma prj_f : function (pr_j f j).
Proof. apply: lf_function; apply: prj_axiom. Qed.

Lemma prj_V x: inc x (productb f) -> Vf (pr_j f j) x = (restr x j).
Proof. by rewrite /pr_j =>ix; aw; apply: prj_axiom. Qed.

Lemma prj_VV x i:
  inc x (productb f) -> inc i j
  -> Vg (Vf (pr_j f j) x) i = Vg x i.
Proof.
move=> xp ij; rewrite prj_V //.
by move /setXb_P: xp => [fw dd _]; bw; ue.
Qed.

End RestrictionProduct.

If f is a family of non-empty sets, any g defined on a subset of the domain of f with values in the partial product can be extended to the whole product; thus pr_i and pr_j are sujective

Theorem extension_psetX f j g:
  nonempty_fam f ->
  fgraph g -> domain g = j -> sub j (domain f) ->
  (forall i, inc i j -> inc (Vg g i) (Vg f i)) ->
  exists h, [/\ domain h = domain f, fgraph h,
    (forall i, inc i (domain f) -> inc (Vg h i) (Vg f i)) &
    {inc j, h =1g g} ].
Proof.
move=> alne fg dg sjdf iVV.
set (h:= g \cup (unionf ((domain f) -s j)
  (fun i => (singleton (J i (rep (Vg f i))))))).
have hg: sgraph h.
  move=>t;case /setU2_P; first by move: fg=> [gg _]; apply: gg.
  move/setUf_P=> [y _ /set1_P ->]; fprops.
have dh: domain h = domain f.
  set_extens t.
    move /(domainP hg) => [y /setU2_P []].
      move=> Jg; apply: sjdf; rewrite -dg; bw; fprops; ex_tac.
    move /setUf_P => [y' yc /set1_P Js].
    by rewrite (pr1_def Js); move /setC_P: yc => [].
  move => tdf; apply/(domainP hg);case: (inc_or_not t j).
    by rewrite -dg; move/(domainP (proj1 fg)) => [y jg];exists y; apply:setU2_1.
  move=> ntj; exists (rep (Vg f t)).
  apply:setU2_2; apply /setUf_P; exists t;fprops.
have fgh: fgraph h.
  split =>//.
  move => x y; case /setU2_P => x1; case /setU2_P => y1.
  - by move: fg=> [_ ]; apply.
  - move/setUf_P: y1 => [z /setC_P [_ nzj] /set1_P eq1] eq2.
    move: (domain_i1 x1); rewrite dg eq2 eq1; aw; contradiction.
  - move/setUf_P: x1 => [z/setC_P [_ nzj] /set1_P eq1] eq2.
    move: (domain_i1 y1); rewrite dg - eq2 eq1; aw; contradiction.
  - move/setUf_P: x1 => [x1 _ /set1_P ->]; aw.
    by move/setUf_P: y1 => [y1 _ /set1_P ->]; aw => ->.
have sV: forall i, inc i j -> Vg h i = Vg g i.
  have sgh: (sub g h) by move=> t; rewrite /h; aw; fprops.
  by move=> i; rewrite -dg=> ij; symmetry; apply: (sub_graph_ev fgh sgh ij).
exists h; split => // i id.
case: (inc_or_not i j)=> hyp; first by rewrite sV //; apply: iVV.
have ic: (inc i ((domain f) -s j)) by fprops.
have Jh: (inc (J i (rep (Vg f i))) h).
   by rewrite /h; apply: setU2_2; union_tac.
by move: (pr2_V fgh Jh); aw; move=> <-; apply: rep_i; apply: alne.
Qed.

Theorem prj_fs f j: nonempty_fam f -> sub j (domain f) ->
  surjection (pr_j f j).
Proof.
move=> alne sjd;split; first by apply: prj_f.
rewrite /pr_j=> y; aw; move/setXb_P.
bw;move => [fy dy iVVy].
have iVV: (forall i, inc i j -> inc (Vg y i) (Vg f i)).
 by move => i ij; move: (iVVy _ ij); bw.
move: (extension_psetX alne fy dy sjd iVV) => [h [dh fgh iVVh sv]].
have hp: (inc h (productb f)) by apply/setXb_P.
ex_tac; rewrite prj_V //; rewrite -dh in sjd; symmetry.
by apply: fgraph_exten; bw;fprops=> x; rewrite dy => xd /=; bw; rewrite sv.
Qed.

Lemma pri_fs f k: nonempty_fam f ->
  inc k (domain f) -> surjection (pr_i f k).
Proof.
move=> alne kd.
set (j:= singleton k).
have sjd: (sub j (domain f)) by move=> t; move/set1_P => ->.
have cpc: (product1_canon (Vg f k) k) \coP (pr_i f k).
  split; first by apply: setX1_canon_f.
     by apply: pri_f.
  by rewrite /product1_canon /pr_i; aw.
have fcpx:(function ((product1_canon (Vg f k) k) \co (pr_i f k))).
  by fct_tac.
have prjc: (pr_j f j = (product1_canon (Vg f k) k) \co (pr_i f k)).
  apply: function_exten => //.
  - by apply: prj_f=>//.
  - by rewrite /pr_j/pr_i; aw.
  - rewrite /pr_j/pr_i/product1_canon/product1; aw.
  - rewrite/restriction_product.
    have: (Lg j (Vg f)) = cst_graph (singleton k) (Vg f k).
      by apply: Lg_exten => t /set1_P ->.
    by rewrite/restriction_product; move->.
  - move=> x xs.
    have xp: inc x (productb f) by move: xs;rewrite /pr_j lf_source.
    have xsk: inc x (source (pr_i f k)) by rewrite /pr_i lf_source.
    have aux1: inc (Vf (pr_i f k) x) (Vg f k).
      have : (target (pr_i f k) = Vg f k) by rewrite/pr_i; aw.
      by move=> <-; Wtac; apply: pri_f=>//.
    aw=>//; rewrite setX1_canon_V //.
    rewrite prj_V //.
    have xp1: inc x (productb f) by [].
    move /setXb_P: xp1 => [fx dx iVVx].
    have ssk: sub (singleton k) (domain x).
       by move=> xw eq1; bw; rewrite (set1_eq eq1) dx.
    rewrite/j; apply: fgraph_exten; rewrite /cst_graph;fprops;bw.
    move=> z zk /=; bw;rewrite (set1_eq zk) pri_V //.
apply: (left_compose_fs2 cpc).
  by rewrite - prjc; apply: prj_fs.
move: (setX1_canon_fb (Vg f k) k)=> [ h _]; apply: h.
Qed.

if X and Y are functional graphs, with same domain, productb X is a subset of productb g if and only if the same holds for each component (for one implication, the small product must be non-empty)

Lemma setXb_monotone1 f g:
  domain f = domain g ->
  (forall i, inc i (domain f) -> sub (Vg f i) (Vg g i))
  -> sub (productb f) (productb g).
Proof.
move=> dfdg sVV x /setXb_P [fx dx iVV].
apply/setXb_P; rewrite -dfdg;split => //; move => i ifg; apply: sVV; fprops.
Qed.

Lemma setXb_monotone2 f g:
  domain f = domain g ->
  nonempty_fam f ->
  sub (productb f) (productb g) ->
  (forall i, inc i (domain f) -> sub (Vg f i) (Vg g i)).
Proof.
move=> dfdg alne sfg i id j jV.
have jt: (inc j (target (pr_i f i))) by rewrite/ pr_i; aw.
move:((proj2 (pri_fs alne id)) _ jt) => [x xs <-].
move: xs; rewrite /pr_i lf_source=>xs.
rewrite pri_V //.
by move /setXb_P: (sfg _ xs) => [fx dx]; apply; rewrite -dfdg.
Qed.

EII-5-5 associativity of products of sets

Given a product with domain I, and a partition J of I, we can consider the set of mappings that associate to each j in J the partial product. This is a product. Associativity says that this product of products is isomorphic to the initial product. Implies associativity of cardinal product

Definition prod_assoc_axioms f g :=
  partition_w_fam g (domain f).

Definition prod_assoc_map f g :=
  Lf(fun z => (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) z)))
  (productb f)
  (productf (domain g) (fun l => (restriction_product f (Vg g l)))).

Lemma pam_axiom f g:
  prod_assoc_axioms f g ->
  lf_axiom(fun z => (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) z)))
  (productb f)
  (productf (domain g) (fun l => (restriction_product f (Vg g l)))).
Proof.
move=> [fg md u] t td; apply/setXb_P; bw; split;fprops.
move=> i id; bw.
have: (restriction_product f (Vg g i) = target (pr_j f (Vg g i))).
  by rewrite /pr_j; aw.
move=>->; Wtac; last by rewrite/pr_j lf_source.
apply: prj_f=>//; move=> z; rewrite -u=> tu; union_tac.
Qed.

Lemma pam_f f g:
  prod_assoc_axioms f g ->
  function (prod_assoc_map f g).
Proof. by move => h; apply: lf_function; apply: pam_axiom. Qed.

Lemma pam_V f g x:
  prod_assoc_axioms f g -> inc x (productb f) ->
  Vf (prod_assoc_map f g) x = (Lg (domain g) (fun l => Vf (pr_j f (Vg g l)) x)).
Proof. by rewrite /prod_assoc_map=> a xp; aw; apply: pam_axiom. Qed.

Lemma pam_fi f g:
  prod_assoc_axioms f g ->
  injection (prod_assoc_map f g).
Proof.
move=> pa; split; first by apply: pam_f.
have sp:(source (prod_assoc_map f g) = productb f).
  by rewrite /prod_assoc_map; aw.
rewrite sp {sp} => x y xs ys.
rewrite (pam_V pa xs)(pam_V pa ys) => sv.
move: pa=> [fg md ugdf].
apply: (@setXb_exten _ x y xs ys) => i; rewrite - ugdf.
move/setUb_P => [z zd iV].
have svf: sub (Vg g z) (domain f) by move=> t tv; rewrite - ugdf; union_tac.
move: (f_equal (Vg ^~ z) sv); bw;rewrite prj_V // prj_V // => sv1.
move/setXb_P: xs => [fx dx _];move/setXb_P: ys => [fy dy _].
move:(f_equal (Vg ^~i) sv1); bw; ue.
Qed.

Theorem pam_fb f g:
  prod_assoc_axioms f g ->
  bijection (prod_assoc_map f g).
Proof.
move=> pa; split; first by apply: pam_fi.
split; first by apply: pam_f.
have sp: source (prod_assoc_map f g) = productb f
  by rewrite /prod_assoc_map; aw.
have tp: target (prod_assoc_map f g) =
  (productf (domain g) (fun l => restriction_product f (Vg g l))).
  by rewrite /prod_assoc_map; aw.
rewrite sp tp; move=> y yp; move /setXf_P: (yp); bw; move => [fy dy iVr].
move: (pa) => [fg md ugdf].
have sVd: forall i, inc i (domain g) -> sub (Vg g i) (domain f).
  by move=> i id v vV; rewrite -ugdf; union_tac.
pose h i := Lf (fun z => (Vg (Vg y i) z)) (Vg g i) (unionb f).
have ta:forall i, inc i (domain g) ->
    lf_axiom (fun z => Vg (Vg y i) z) (Vg g i) (unionb f).
  move=> i id x xV; move: (sVd _ id) =>sVdi.
  apply: (@setUb_i _ x); first by apply: sVdi=>//.
  move: (iVr _ id); bw; move/setXb_P => [fgV deq]; bw => rel.
  move: (rel _ xV); bw.
have afp: forall i, inc i (domain g) -> function_prop (h i) (Vg g i) (unionb f).
  move=> i id; rewrite /h.
  by split; first (by apply: lf_function; apply: ta); aw.
move: (extension_partition_thm pa afp) => [x [[[fx sx tx] ag] etc]].
have gxp: inc (graph x) (productb f).
  apply/setXb_P; rewrite (f_domain_graph fx) - sx;split; fprops.
  move=> i ix; rewrite -/(Vf x i).
  move: ix; rewrite sx -ugdf; move/(setUb_P) =>[z zdg iV].
  move: (ag _ zdg)=> [_ _ eq]; rewrite (eq _ iV) /h.
  aw; last by apply: (ta _ zdg).
  move: (iVr _ zdg); bw; move/setXb_P => [qa]; bw => eq1 res.
  move: (res _ iV); bw.
have Wt: inc (Vf (prod_assoc_map f g)(graph x))(target (prod_assoc_map f g)).
  by Wtac; apply: pam_f.
ex_tac; symmetry; apply: (setXf_exten (x:=y) (x':= Vf _ _ ) yp).
  by rewrite - tp.
move=> i id.
have aux2: sub (Vg g i) (domain f) by apply: sVd.
have aux3: sub (Vg g i) (domain (graph x)) by aw; ue.
rewrite pam_V=> //; bw; rewrite prj_V //.
move: (iVr _ id); bw; move/setXb_P=> [fgy]; bw => qa qb.
apply: fgraph_exten; bw; fprops.
move: (ag _ id)=> [ aa bb cc].
move => j; rewrite qa => jd; move: (cc _ jd); bw.
by rewrite -/(Vf x j) => ->; rewrite/h; aw; apply: ta.
Qed.

Case where the domain is partitioned in two sets

Lemma variantLc_prop x y:
  variantLc x y = Lg C2 (variant C0 x y).
Proof. by []. Qed.

Lemma prod_assoc_map2 f g:
  prod_assoc_axioms f g -> domain g = C2
  -> (productb f) \Eq
  ((restriction_product f(Vg g C0)) \times (restriction_product f (Vg g C1))).
Proof.
move=> pam dg.
eqtrans (productf (domain g) (fun l => (restriction_product f (Vg g l)))).
  exists (prod_assoc_map f g).
  split; first (by apply: pam_fb); rewrite /prod_assoc_map; aw.
eqsym.
exists (product2_canon (restriction_product f (Vg g C0))
    (restriction_product f (Vg g C1))).
rewrite /bijection_prop/product2_canon; aw; split => //.
   by apply: product2_canon_fb.
rewrite dg; congr (productb<