proposition: Corollary prod_in_inj {x y z : C} (f g : F x ~> F y × F z) : prod_in ∘ f ≈ prod_in ∘ g ↔ f ≈ g.
proof: Proof. split; intros Hprod. - rewrite <- id_left. rewrite <- prod_out_in. rewrite <- comp_assoc. rewrite Hprod. rewrite comp_assoc. autorewrite with functors; cat. - subst. rewrite Hprod. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Opposite Category.Structure.Cartesian