mathlib3 documentation

category_theory.monoidal.types.symmetric

The category of types is a symmetric monoidal category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]

def category_theory.types_symmetric :

category_theory.symmetric_category (Type u)

Equations

category_theory.types_symmetric = category_theory.symmetric_of_chosen_finite_products category_theory.limits.types.terminal_limit_cone category_theory.limits.types.binary_product_limit_cone

@[simp]

theorem category_theory.braiding_hom_apply {X Y : Type u} {x : X} {y : Y} :

(β_ X Y).hom (x, y) = (y, x)

@[simp]

theorem category_theory.braiding_inv_apply {X Y : Type u} {x : X} {y : Y} :

(β_ X Y).inv (y, x) = (x, y)