If C is braided, so is Cᵒᵖ.

Todo: we should also do Cᵐᵒᵖ.

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

Equations

• instBraidedCategoryOpposite = { braiding := fun (X Y : Cᵒᵖ) => (β_ Y.unop X.unop).op, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }