proposition: Corollary exr_fork {x z w : C} (f : x ~> z) (g : x ~> w) : exr ∘ f △ g ≈ g.
proof: Proof. intros. now apply (ump_products f g (f △ g)). Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal