proposition: Lemma fun_set_to_prod6 f: function f -> target f = productb F -> (function (fun_set_to_prod5 F f) /\ (fun_set_to_prod5 F f) \coP (constant_functor (domain F)(source f) )/\ (fun_set_to_prod5 F f) \co (constant_functor (domain F)(source f)) =f).
proof: Proof. move=> ff tfpF. set (tf := fun_set_to_prod5 F f). have ftf: function tf. rewrite /tf/fun_set_to_prod5; apply: ext_map_prod_f=> x xs. have [[fc sc tc] vc] := (fun_set_to_prod1 fF xs ff tfpF). split. + fprops. + by rewrite domain_fg. + by rewrite -tc; apply: f_range_graph. have ttf:(productb F = target tf). rewrite /tf/fun_set_to_prod5/ext_map_prod. aw; rewrite /productf; apply: f_equal; apply: fgraph_exten; aww. by move=> x xd; rewrite LgV. have ctf: tf \coP (constant_functor (domain F)(source f)). split; fprops. rewrite /constant_functor; apply: lf_function. move => x xs /=; apply/gfunctions_P2. rewrite/cst_graph; aw;split; fprops. have aux: fgraph (Lg (domain F) (fun _ : Set => x)) by fprops. move=> y /(range_gP aux) [b ]; rewrite Lgd => h ->; rewrite LgV //. set (k:= cst_graph (domain F) (source f)); aw. have: (domain F = domain k) by rewrite/k; aw. move=> ->; rewrite /constant_functor; aw. rewrite - setXb_eq_gfunctions. by rewrite /tf/fun_set_to_prod5/ext_map_prod; aw. by rewrite /k; aw => i id; rewrite LgV. split=> //; split=>//. have ta1: lf_axiom [eta cst_graph (domain F)] (source f) (gfunctions (domain F) (source f)). move=> y yd; rewrite /gfunctions. apply: Zo_i; last by aw; split; fprops. apply /setP_P => t /funI_P [z zd ->]; fprops. symmetry; apply: function_exten =>//; try fct_tac. by rewrite /constant_functor; aw. rewrite /tf/fun_set_to_prod5/ext_map_prod; aw. by rewrite /productf tfpF Lg_recovers //. move=> x xsf; rewrite /constant_functor. rewrite compfV // ?lf_source // LfV //. have cgd: inc (cst_graph (domain F) x) (productf (domain F) (fun _ : Set => source f)). rewrite/cst_graph; apply/setXf_P. by split; aww => j jd; rewrite LgV. have:inc (Vf f x) (productb F) by rewrite - tfpF; fprops. have: (inc (Vf tf (cst_graph (domain F) x)) (productb F)). by rewrite ttf; Wtac; rewrite /tf/fun_set_to_prod5/ext_map_prod; aw. move=> p1 p2; apply: (setXb_exten p2 p1). move=> i idf /=; rewrite /tf/fun_set_to_prod5 ext_map_prod_V //. rewrite LgV // /ext_map_prod_aux /cst_graph LgV //. set cp:= (pr_i F i) \co f. rewrite -/(Vf cp x) /cp compfV //; first by rewrite pri_V. split => //; [ by apply: pri_f | by rewrite /pr_i; aw]. move => j jd. move: (fun_set_to_prod1 fF jd ff tfpF) => [[fcf sc tc] vc]. split; fprops; first by rewrite - sc; fprops; rewrite domain_fg//. by rewrite -tc;apply: f_range_graph=>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)