If C is braided, so is Cᵒᵖ. #
Todo: we should also do Cᵐᵒᵖ.
instance
instBraidedCategoryOppositeOppositeMonoidalCategoryOp
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.BraidedCategory C]
:
Equations
- One or more equations did not get rendered due to their size.