proposition: Lemma braid2_natural : natural (@braid2 _).
proof: Proof. unfold braid2; simpl; intros; normal. rewrite from_tensor_assoc_natural. rewrite <- !comp_assoc. rewrite <- to_tensor_assoc_natural. normal. comp_right. comp_left. normal. bimap_left. rewrite to_tensor_assoc_natural. rewrite <- !comp_assoc. rewrite <- from_tensor_assoc_natural. comp_left. comp_right. normal. bimap_right. spose (braid_natural _ _ h _ _ i) as X. normal; assumption. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Naturality Category.Functor.Bifunctor Category.Structure.Monoidal.Symmetric