mathlib documentation

category_theory.monoidal.types

The category of types is a symmetric monoidal category

@[simp]
theorem category_theory.monoidal.tensor_apply {W X Y Z : Type u} (f : W X) (g : Y Z) (p : W Y) :
(f g) p = (f p.fst, g p.snd)

@[simp]
theorem category_theory.monoidal.left_unitor_hom_apply {X : Type u} {x : X} {p : punit} :
(λ_ X).hom (p, x) = x

@[simp]
theorem category_theory.monoidal.left_unitor_inv_apply {X : Type u} {x : X} :
(λ_ X).inv x = (punit.star, x)

@[simp]
theorem category_theory.monoidal.right_unitor_hom_apply {X : Type u} {x : X} {p : punit} :
(ρ_ X).hom (x, p) = x

@[simp]
theorem category_theory.monoidal.right_unitor_inv_apply {X : Type u} {x : X} :
(ρ_ X).inv x = (x, punit.star)

@[simp]
theorem category_theory.monoidal.associator_hom_apply {X Y Z : Type u} {x : X} {y : Y} {z : Z} :
(α_ X Y Z).hom ((x, y), z) = (x, y, z)

@[simp]
theorem category_theory.monoidal.associator_inv_apply {X Y Z : Type u} {x : X} {y : Y} {z : Z} :
(α_ X Y Z).inv (x, y, z) = ((x, y), z)

@[simp]
theorem category_theory.monoidal.braiding_hom_apply {X Y : Type u} {x : X} {y : Y} :
(β_ X Y).hom (x, y) = (y, x)

@[simp]
theorem category_theory.monoidal.braiding_inv_apply {X Y : Type u} {x : X} {y : Y} :
(β_ X Y).inv (y, x) = (x, y)