If C is braided, so is Cᵒᵖ.

Todo: we should also do Cᵐᵒᵖ.

@[instance_reducible]

instance instBraidedCategoryOpposite {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory Cᵒᵖ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.BraidedCategory.unop_tensorμ {C : Type u_2} [Category.{v_2, u_2} C] [MonoidalCategory C] [BraidedCategory C] (X Y W Z : Cᵒᵖ) : (MonoidalCategory.tensorμ X W Y Z).unop = MonoidalCategory.tensorμ (Opposite.unop X) (Opposite.unop Y) (Opposite.unop W) (Opposite.unop Z)

@[simp]

theorem CategoryTheory.BraidedCategory.op_tensorμ {C : Type u_2} [Category.{v_2, u_2} C] [MonoidalCategory C] [BraidedCategory C] (X Y W Z : C) : (MonoidalCategory.tensorμ X W Y Z).op = MonoidalCategory.tensorμ (Opposite.op X) (Opposite.op Y) (Opposite.op W) (Opposite.op Z)