proposition: Corollary prod_in_out (x y : C) : prod_in ∘ prod_out ≈ @id _ (F (x × y)).
proof: Proof. intros. exact (iso_from_to fobj_prod_iso). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Opposite Category.Structure.Cartesian