Theoremsbraiding_inv_naturality, braiding_inv_naturality_assoc, braiding_inv_naturality_left, braiding_inv_naturality_left_assoc, braiding_inv_naturality_right, braiding_inv_naturality_right_assoc, braiding_naturality, braiding_naturality_assoc, braiding_naturality_left, braiding_naturality_left_assoc, braiding_naturality_right, braiding_naturality_right_assoc, braiding_tensor_left_hom, braiding_tensor_left_hom_assoc, braiding_tensor_left_inv, braiding_tensor_left_inv_assoc, braiding_tensor_right_hom, braiding_tensor_right_hom_assoc, braiding_tensor_right_inv, braiding_tensor_right_inv_assoc, curriedBraidingNatIso_hom_app_app, curriedBraidingNatIso_inv_app_app, hexagon_forward, hexagon_forward_assoc, hexagon_forward_inv, hexagon_forward_inv_assoc, hexagon_forward_iso, hexagon_reverse, hexagon_reverse_assoc, hexagon_reverse_inv, hexagon_reverse_inv_assoc, hexagon_reverse_iso, tensorLeftIsoTensorRight_hom_app, tensorLeftIsoTensorRight_inv_app, yang_baxter, yang_baxter', yang_baxter_assoc, yang_baxter_iso, braided, ext, ext_iff, toMonoidal_injective, braided, braided_assoc, map_braiding, map_braiding_assoc, comp_hom, comp_hom_assoc, forget_map, forget_obj, homMk_hom_hom, hom_ext, hom_ext_iff, id_hom, isoMk_hom, isoMk_inv, isoOfComponents_hom_hom_app, isoOfComponents_hom_hom_hom_app, isoOfComponents_inv_hom_app, isoOfComponents_inv_hom_hom_app, of_toFunctor, toLaxMonoidalFunctor_toFunctor, associator_monoidal, associator_monoidal_assoc, leftUnitor_monoidal, leftUnitor_monoidal_assoc, rightUnitor_monoidal, rightUnitor_monoidal_assoc, tensor_associativity, tensor_associativity_assoc, tensor_left_unitality, tensor_left_unitality_assoc, tensor_right_unitality, tensor_right_unitality_assoc, tensor_Ī“, tensor_Īµ, tensor_Ī·, tensor_Ī¼, tensorĪ“_tensorĪ¼, tensorĪ“_tensorĪ¼_assoc, tensorĪ¼_comp_Ī¼_tensorHom_Ī¼_comp_Ī¼, tensorĪ¼_comp_Ī¼_tensorHom_Ī¼_comp_Ī¼_assoc, tensorĪ¼_natural, tensorĪ¼_natural_assoc, tensorĪ¼_natural_left, tensorĪ¼_natural_left_assoc, tensorĪ¼_natural_right, tensorĪ¼_natural_right_assoc, tensorĪ¼_tensorĪ“, tensorĪ¼_tensorĪ“_assoc, mopFunctor_Ī“, mopFunctor_Īµ, mopFunctor_Ī·, mopFunctor_Ī¼, mop_braiding, mop_hom_braiding, mop_inv_braiding, unmopFunctor_Ī“, unmopFunctor_Īµ, unmopFunctor_Ī·, unmopFunctor_Ī¼, unmop_braiding, unmop_hom_braiding, unmop_inv_braiding, braiding_swap_eq_inv_braiding, reverseBraiding_eq, symmetry, symmetry_assoc, braiding_inv_tensorUnit_left, braiding_inv_tensorUnit_left_assoc, braiding_inv_tensorUnit_right, braiding_inv_tensorUnit_right_assoc, braiding_leftUnitor, braiding_leftUnitor_assoc, braiding_leftUnitor_auxā, braiding_leftUnitor_auxā, braiding_rightUnitor, braiding_rightUnitor_assoc, braiding_rightUnitor_auxā, braiding_rightUnitor_auxā, braiding_tensorUnit_left, braiding_tensorUnit_left_assoc, braiding_tensorUnit_right, braiding_tensorUnit_right_assoc, leftUnitor_inv_braiding, leftUnitor_inv_braiding_assoc, op_braiding, op_hom_braiding, op_inv_braiding, rightUnitor_inv_braiding, rightUnitor_inv_braiding_assoc, unop_braiding, unop_hom_braiding, unop_inv_braiding | 134 |