proposition: Proposition ump_product_auto1 (C : Category) `{@Cartesian C} (x y z: C) (h : z ~> x × y) (f : z ~> x) (g : z ~> y) : (exl ∘ h) ≈ f -> (exr ∘ h) ≈ g -> h ≈ fork f g.
proof: Proof. intros. apply (snd (ump_products _ _ _)); split; trivial. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Functor Category.Theory.Natural.Transformation Category.Instance.Sets Category.Instance.Fun Category.Structure.Cartesian Category.Lib.Tactics2