proposition: Corollary fork_merge {x y z w : C} (f : x ~> y) (g : x ~> z) (h : w ~> y) (i : w ~> z) : (f △ g) ▽ (h △ i) ≈ (f ▽ h) △ (g ▽ i).
proof: Proof. rewrite <- id_left. rewrite <- fork_exl_exr. rewrite <- fork_comp. apply fork_respects; rewrite <- merge_comp; cat; apply (@fork_respects (C^op)); cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Structure.Cartesian Category.Structure.Cocartesian Category.Construction.Opposite