proposition: Proposition ump_product' (C : Category) `{@Cartesian C} (x y z: C) (h h': z ~> x × y) : (exl ∘ h) ≈ (exl ∘ h') -> (exr ∘ h) ≈ (exr ∘ h') -> h ≈ h'.
proof: Proof. intros. assert (RW: h ≈ fork (exl ∘ h) (exr ∘ h)). { apply (snd (ump_products _ _ _)); split; reflexivity. } rewrite RW; symmetry. apply (snd (ump_products _ _ _)); split; symmetry; assumption. 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