mathlibdocumentation

category_theory.monoidal.types

The category of types is a symmetric monoidal category #

@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem category_theory.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.left_unitor_hom_apply {X : Type u} {x : X} {p : punit} :
(λ_ X).hom (p, x) = x
@[simp]
theorem category_theory.left_unitor_inv_apply {X : Type u} {x : X} :
(λ_ X).inv x = (punit.star, x)
@[simp]
theorem category_theory.right_unitor_hom_apply {X : Type u} {x : X} {p : punit} :
(ρ_ X).hom (x, p) = x
@[simp]
theorem category_theory.right_unitor_inv_apply {X : Type u} {x : X} :
(ρ_ X).inv x = (x, punit.star)
@[simp]
theorem category_theory.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.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.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)

(𝟙_ C ⟶ -) is a lax monoidal functor to Type.

Equations
noncomputable def category_theory.monoidal_functor.map_pi {C : Type u_1} (F : C) (n : ) (β : Type u_3) :

If F is a monoidal functor out of Type, it takes the (n+1)st cartesian power of a type to the image of that type, tensored with the image of the nth cartesian power.

Equations