proposition: Lemma bimap_braid {x y z w} (f : x ~> z) (g : y ~> w) : g ⨂ f ∘ braid ≈ braid ∘ f ⨂ g.
proof: Proof. spose (braid_natural _ _ f _ _ g) as X. normal. apply X. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal.Braided