proposition: Corollary proj_right_left_diagonal {x y} : proj_right ⨂ proj_left ∘ ∆(x ⨂ y) ≈ braid.
proof: Proof. rewrite <- bimap_id_left_right. rewrite <- comp_assoc. rewrite proj_right_id_diagonal. unfold proj_left, proj_right. normal. rewrite bimap_comp_id_left. rewrite <- !comp_assoc. rewrite (comp_assoc _ tensor_assoc). rewrite to_tensor_assoc_natural. normal. rewrite <- comp_assoc. rewrite triangle_identity_right. rewrite <- !comp_assoc. rewrite (comp_assoc (tensor_assoc⁻¹)). rewrite iso_from_to. normal. rewrite <- bimap_id_right_left. rewrite !comp_assoc. rewrite <- to_unit_right_natural. symmetry. rewrite <- id_right at 1. rewrite <- !comp_assoc. comp_left. symmetry. normal. spose (@from_tensor_assoc_natural _ _ x _ y _ y _ id id eliminate) as X0. rewrite bimap_id_id in X0. rewrite <- !comp_assoc. rewrite (comp_assoc (bimap _ _)). rewrites. normal. rewrite eliminate_right_diagonal. rewrite <- triangle_identity_right. normal. rewrite iso_to_from. normal; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal.Proofs Category.Structure.Monoidal.Cartesian