proposition: Lemma hexagon_rotated {x y z} : tensor_assoc ∘ braid ⨂ id ∘ tensor_assoc ⁻¹ << x ⨂ (y ⨂ z) ~~> y ⨂ (x ⨂ z) >> id ⨂ braid ∘ tensor_assoc ∘ braid.
proof: Proof. rewrite <- (id_right (id ⨂ braid ∘ tensor_assoc ∘ braid)). rewrite <- (iso_to_from tensor_assoc). rewrite comp_assoc; rewrite <- (comp_assoc _ tensor_assoc braid); rewrite <- (comp_assoc _ (tensor_assoc ∘ braid) _). rewrite hexagon_identity. rewrite !comp_assoc. rewrite <- bimap_comp; rewrite id_left. rewrite braid_invol. cat. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Functor.Bifunctor Category.Structure.Monoidal.Braided