proposition: Proposition fork'_natural (C: Category) (v w x y z: C) (H: IsCartesianProduct x y z) (f : v ~> w) (a : w ~> x) (b : w ~> y) : fork' a b ∘ f ≈ fork' (a ∘ f) (b ∘ f).
proof: Proof. apply ump_product; split; rewrite comp_assoc. - now rewrite exl'_fork. - now rewrite exr'_fork. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Structure.Terminal