The category of types is a symmetric monoidal category

instance CategoryTheory.typesSymmetric : CategoryTheory.SymmetricCategory (Type u)

Equations

• CategoryTheory.typesSymmetric = CategoryTheory.symmetricOfChosenFiniteProducts CategoryTheory.Limits.Types.terminalLimitCone CategoryTheory.Limits.Types.binaryProductLimitCone

@[simp]

theorem CategoryTheory.braiding_hom_apply {X : Type u} {Y : Type u} {x : X} {y : Y} : (β_ X Y).hom (x, y) = (y, x)

@[simp]

theorem CategoryTheory.braiding_inv_apply {X : Type u} {Y : Type u} {x : X} {y : Y} : (β_ X Y).inv (y, x) = (x, y)