proposition: Lemma Fun_prod_comp_law : Fcomp_law Fun_prod_map.
proof: Proof. unfold Fcomp_law in |- *; simpl in |- *. intros c1 c2 c3 f g. unfold Fun_prod_mor, Mor_prod in |- *. apply Trans with (H_together C1 (H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj1_prod C1 c2 a o g) (H_proj2_prod C1 c1 a o Id a)). apply (Map2_r (Op_together (C1 c3 a) _) (a1:=H_proj1_prod C1 c1 a o f o g) (a2:=H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj1_prod C1 c2 a o g) (H_proj2_prod C1 c1 a o Id a)). apply Trans with ((H_proj1_prod C1 c1 a o f) o g). apply Ass. apply Trans with ((H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj1_prod C1 c2 a) o g). apply Comp_r; apply Sym. apply (Prf_eq1_prod (C1 c2 a) (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a)). apply Ass1. apply Trans with (H_together C1 (H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj1_prod C1 c2 a o g) (H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj2_prod C1 c2 a o Id a)). apply (Prf_map2_congl (Op_together (C1 c3 a) _) (b1:=H_proj2_prod C1 c1 a o Id a) (b2:=H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj2_prod C1 c2 a o Id a) (H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj1_prod C1 c2 a o g)). apply Trans with ((H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a) o H_proj2_prod C1 c2 a) o Id a). apply Comp_r. apply Trans with (H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a) o H_proj2_prod C1 c2 a). apply Sym. apply (Prf_eq2_prod (C1 c2 a) (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a)). apply Comp_r. apply (Prf_map2_congl (Op_together (C1 c2 a) _) (b1:=H_proj2_prod C1 c1 a) (b2:=H_proj2_prod C1 c1 a o Id a) (H_proj1_prod C1 c1 a o f)). apply Idr. apply Ass1. apply Sym. apply (Eq3_prod (C1 c3 a) (H_proj1_prod C1 c2 a o g) (H_proj2_prod C1 c2 a o Id a) (H_together C1 (H_proj1_prod C1 c1 a o f) (H_proj2_prod C1 c1 a o Id a))). Qed.
imports: Binary_Products Functor