proposition: Theorem Yang_Baxter_equation {a b c : C} : braid ⨂ id[a] ∘ tensor_assoc⁻¹ ∘ id[b] ⨂ braid ∘ tensor_assoc ∘ braid ⨂ id[c] ∘ tensor_assoc⁻¹ ≈ tensor_assoc⁻¹ ∘ id[c] ⨂ braid ∘ tensor_assoc ∘ braid ⨂ id[b] ∘ tensor_assoc⁻¹ ∘ id[a] ⨂ braid.
proof: Proof. rewrite <- !comp_assoc. rewrite (@comp_assoc _ _ _ _ _ (id ⨂ braid)). rewrite (@comp_assoc _ _ _ _ _ _ (braid ⨂ id)). rewrite <- hexagon_identity. rewrite <- !comp_assoc. rewrite (@comp_assoc _ _ _ _ _ tensor_assoc⁻¹ tensor_assoc). rewrite iso_from_to, id_left. rewrite iso_to_from, id_right. rewrite (@comp_assoc _ _ _ _ _ (id ⨂ braid)). rewrite (@comp_assoc _ _ _ _ _ _ (braid ⨂ id)). rewrite <- hexagon_identity. rewrite <- !comp_assoc. rewrite (@comp_assoc _ _ _ _ _ tensor_assoc⁻¹ tensor_assoc). rewrite iso_from_to, id_left. rewrite (@comp_assoc _ _ _ _ _ _ tensor_assoc⁻¹). rewrite iso_to_from, id_left. spose (braid_natural a _ id _ _ (@braid _ b c)) as X. rewrite bimap_id_id in X. rewrite id_right in X. rewrite X. rewrite bimap_id_id. rewrite id_right. reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Isomorphism Category.Theory.Functor Category.Theory.Naturality Category.Functor.Bifunctor Category.Structure.Monoidal Category.Structure.Monoidal.Naturality