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