The category of types is a monoidal category #
@[simp]
theorem
CategoryTheory.tensor_apply
{W : Type u}
{X : Type u}
{Y : Type u}
{Z : Type u}
(f : W ⟶ X)
(g : Y ⟶ Z)
(p : CategoryTheory.MonoidalCategory.tensorObj W Y)
:
CategoryTheory.MonoidalCategory.tensorHom f g p = (f p.fst, g p.snd)
@[simp]
theorem
CategoryTheory.leftUnitor_hom_apply
{X : Type u}
{x : X}
{p : PUnit.{u + 1} }
:
Type u.hom CategoryTheory.types
(CategoryTheory.MonoidalCategory.tensorObj CategoryTheory.MonoidalCategory.tensorUnit' X) X
(CategoryTheory.MonoidalCategory.leftUnitor X) (p, x) = x
@[simp]
theorem
CategoryTheory.leftUnitor_inv_apply
{X : Type u}
{x : X}
:
(CategoryTheory.MonoidalCategory.leftUnitor X).inv x = (PUnit.unit, x)
@[simp]
theorem
CategoryTheory.rightUnitor_hom_apply
{X : Type u}
{x : X}
{p : PUnit.{u + 1} }
:
Type u.hom CategoryTheory.types
(CategoryTheory.MonoidalCategory.tensorObj X CategoryTheory.MonoidalCategory.tensorUnit') X
(CategoryTheory.MonoidalCategory.rightUnitor X) (x, p) = x
@[simp]
theorem
CategoryTheory.rightUnitor_inv_apply
{X : Type u}
{x : X}
:
(CategoryTheory.MonoidalCategory.rightUnitor X).inv x = (x, PUnit.unit)
@[simp]
theorem
CategoryTheory.associator_hom_apply
{X : Type u}
{Y : Type u}
{Z : Type u}
{x : X}
{y : Y}
{z : Z}
:
(CategoryTheory.MonoidalCategory.associator X Y 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}
:
(CategoryTheory.MonoidalCategory.associator X Y Z).inv (x, y, z) = ((x, y), z)
noncomputable def
CategoryTheory.MonoidalFunctor.mapPi
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.MonoidalCategory C]
(F : CategoryTheory.MonoidalFunctor (Type u_2) C)
(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.