mathlib documentation


The category of types is a monoidal category #

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

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

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.