proposition: Lemma fun_set_to_prod7 f g: (forall i, inc i (domain F) -> inc (f i) (gfunctions src (Vg F i))) -> g = ext_map_prod (domain F) (fun i=> src)(Vg F) f -> (forall i, inc i (domain F) -> f i = graph ((pr_i F i) \co (g \co (constant_functor (domain F) src) ))).
proof: Proof. move=> allf geq i idf. set f1:= (constant_functor (domain F) src). have fct: function f1. apply: lf_function. move=> x xd; apply/ gfunctions_P2; rewrite /cst_graph. by split; aww; move => w /Lg_range_P [b _ ->]. have fg: (function g). rewrite geq; apply: ext_map_prod_f. move=> x xd; move:(gfunctions_hi (allf _ xd))=> [h [fh sh <- <-]]. by rewrite domain_fg //; split; fprops;apply: f_range_graph. have cpa: g \coP f1. split=>//;rewrite geq/f1/ext_map_prod/constant_functor; aw. rewrite /productf. set k:= cst_graph (domain F) src. have dkdf: (domain k = domain F) by rewrite /k;aw. have aux: (forall i, inc i(domain k) -> Vg k i = src). by move=> j jd; rewrite /k LgV //;ue. by rewrite (setXb_eq_gfunctions aux) dkdf. have fcf: function (g \co f1) by fct_tac. have cpb: (pr_i F i) \coP (g \co f1). split => //; first by apply: pri_f. rewrite geq /pr_i/ext_map_prod; aw; rewrite/productf Lg_recovers //. have fctr: function ((pr_i F i) \co (g \co f1)) by fct_tac. have [h [fh sh th gh]] := (gfunctions_hi (allf _ idf)). have sf1: source f1 = source h by rewrite /f1/pr_i/constant_functor; aw. have ta1: lf_axiom (cst_graph (domain F)) src (gfunctions (domain F) src). move=> y yd; rewrite /cst_graph/gfunctions. apply: Zo_i; last by aw; split; fprops. apply /setP_P => t /funI_P [z zd ->]; fprops. suff: (h = (pr_i F i) \co (g \co f1)) by move=> <-; ue. apply: function_exten =>//. by rewrite /pr_i/constant_functor; aw. by rewrite /pr_i/constant_functor; aw. rewrite /f1; move => x xh. have xs: inc x src by rewrite - sh. have xs2: inc x (source (constant_functor (domain F) src)). by rewrite /constant_functor; aw. have aax: ext_map_prod_axioms (domain F) (fun _ : Set => src)(Vg F) f. move=> z zs; move: (gfunctions_hi (allf _ zs))=> [k [fk <- <- <-]]. by rewrite domain_fg //;split; fprops; apply: f_range_graph. set q:= cst_graph (domain F) x. have qp: inc q (productf (domain F) (fun _ : Set => src)). by apply/setXf_P; rewrite/q; aw; split; fprops => k kd; rewrite LgV. have si: Vf (constant_functor (domain F) src) x = q. rewrite /Vf/constant_functor /Lf; aw; rewrite LgV//. have seq: (x = Vg q i) by rewrite LgV. rewrite ! compfV // ?compf_s // si geq ext_map_prod_V //. set s:= (Lg (domain F) (ext_map_prod_aux q f)). have isp: inc s (productb F). rewrite /s /ext_map_prod_aux; apply/setXb_P; split;aww. move=> j jd; rewrite LgV // LgV //. have [k [fk sk <- <-]] := (gfunctions_hi (allf _ jd)). rewrite -/(Vf _ _ ); Wtac. by rewrite /s pri_V // LgV // /ext_map_prod_aux /Vf gh - seq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)