proposition: Lemma braid_bimap_braid {x y z w} (f : x ~> z) (g : y ~> w) : braid ∘ g ⨂ f ∘ braid ≈ f ⨂ g.
proof: Proof. rewrite <- comp_assoc. rewrite bimap_braid. rewrite comp_assoc. rewrite braid_invol. cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal.Braided