proposition: Lemma Fun_prod_id_law : Fid_law Fun_prod_map.
proof: Proof. unfold Fid_law in |- *; simpl in |- *. unfold Fun_prod_mor, Mor_prod in |- *. intro c; unfold Fun_prod_ob in |- *. apply Trans with (H_together C1 (Id (H_obj_prod C1 c a) o H_proj1_prod C1 c a) (H_proj2_prod C1 c a o Id a)). apply (Prf_map2_congr (Op_together (C1 c a) _) (a1:=H_proj1_prod C1 c a o Id c) (a2:=Id (H_obj_prod C1 c a) o H_proj1_prod C1 c a) (H_proj2_prod C1 c a o Id a)). apply Trans with (H_proj1_prod C1 c a). apply Idr1. apply Idl1. apply Trans with (H_together C1 (Id (H_obj_prod C1 c a) o H_proj1_prod C1 c a) (Id (H_obj_prod C1 c a) o H_proj2_prod C1 c a)). apply (Prf_map2_congl (Op_together (C1 c a) _) (b1:=H_proj2_prod C1 c a o Id a) (b2:=Id (H_obj_prod C1 c a) o H_proj2_prod C1 c a) (Id (H_obj_prod C1 c a) o H_proj1_prod C1 c a)). apply Trans with (H_proj2_prod C1 c a). apply Idr1. apply Idl1. apply (Prf_unique_together (Id (H_obj_prod C1 c a))). Qed.
imports: Binary_Products Functor