# The category of types is a monoidal category #

Equations
@[simp]
theorem CategoryTheory.tensor_apply {W : Type u} {X : Type u} {Y : Type u} {Z : Type u} (f : W X) (g : Y Z) :
= (f p.1, g p.2)
@[simp]
theorem CategoryTheory.whiskerLeft_apply (X : Type u) {Y : Type u} {Z : Type u} (f : Y Z) :
= (p.1, f p.2)
@[simp]
theorem CategoryTheory.whiskerRight_apply {Y : Type u} {Z : Type u} (f : Y Z) (X : Type u) :
= (f p.1, p.2)
@[simp]
theorem CategoryTheory.leftUnitor_hom_apply {X : Type u} {x : X} {p : PUnit.{u + 1} } :
(p, x) = x
@[simp]
theorem CategoryTheory.leftUnitor_inv_apply {X : Type u} {x : X} :
@[simp]
theorem CategoryTheory.rightUnitor_hom_apply {X : Type u} {x : X} {p : PUnit.{u + 1} } :
(x, p) = x
@[simp]
theorem CategoryTheory.rightUnitor_inv_apply {X : Type u} {x : X} :
@[simp]
theorem CategoryTheory.associator_hom_apply {X : Type u} {Y : Type u} {Z : Type u} {x : X} {y : Y} {z : Z} :
.hom ((x, y), z) = (x, y, z)
@[simp]
theorem CategoryTheory.associator_inv_apply {X : Type u} {Y : Type u} {Z : Type u} {x : X} {y : Y} {z : Z} :
.inv (x, y, z) = ((x, y), z)
@[simp]
theorem CategoryTheory.associator_hom_apply_1 {X : Type u} {Y : Type u} {Z : Type u} :
(.hom x).1 = x.1.1
@[simp]
theorem CategoryTheory.associator_hom_apply_2_1 {X : Type u} {Y : Type u} {Z : Type u} :
(.hom x).2.1 = x.1.2
@[simp]
theorem CategoryTheory.associator_hom_apply_2_2 {X : Type u} {Y : Type u} {Z : Type u} :
(.hom x).2.2 = x.2
@[simp]
theorem CategoryTheory.associator_inv_apply_1_1 {X : Type u} {Y : Type u} {Z : Type u} :
(.inv x).1.1 = x.1
@[simp]
theorem CategoryTheory.associator_inv_apply_1_2 {X : Type u} {Y : Type u} {Z : Type u} :
(.inv x).1.2 = x.2.1
@[simp]
theorem CategoryTheory.associator_inv_apply_2 {X : Type u} {Y : Type u} {Z : Type u} :
(.inv x).2 = x.2.2
noncomputable def CategoryTheory.MonoidalFunctor.mapPi {C : Type u_1} [] (F : ) (n : ) (β : Type u_2) :
F.obj (Fin (n + 1)β) CategoryTheory.MonoidalCategory.tensorObj (F.obj β) (F.obj (Fin nβ))

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
Instances For