proposition: Proposition exl'_fork {C : Category} {w x y z: C} {H : IsCartesianProduct x y z} (f : w ~> x) (g : w ~> y) : exl' ∘ fork' f g ≈ f.
proof: Proof. intros. now apply (ump_product f g ). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal