proposition: Corollary merge_inv {x y z : C} (f h : y ~> x) (g i : z ~> x) : f ▽ g ≈ h ▽ i ↔ (f ≈ h) * (g ≈ i).
proof: Proof. apply (@fork_inv _ O). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Cartesian Category.Structure.Initial Category.Construction.Opposite