fact: Definition fork {x y z} (f : x ~> y) (g : x ~> z) : x ~> y ⨂ z := f ⨂ g ∘ ∆x.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Naturality Category.Functor.Bifunctor Category.Structure.Monoidal.Symmetric