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.1, g p.2)
@[simp]
theorem
CategoryTheory.whiskerLeft_apply
(X : Type u)
{Y : Type u}
{Z : Type u}
(f : Y ⟶ Z)
(p : CategoryTheory.MonoidalCategory.tensorObj X Y)
:
CategoryTheory.MonoidalCategory.whiskerLeft X f p = (p.1, f p.2)
@[simp]
theorem
CategoryTheory.whiskerRight_apply
{Y : Type u}
{Z : Type u}
(f : Y ⟶ Z)
(X : Type u)
(p : CategoryTheory.MonoidalCategory.tensorObj Y X)
:
CategoryTheory.MonoidalCategory.whiskerRight f X p = (f p.1, p.2)
@[simp]
theorem
CategoryTheory.leftUnitor_hom_apply
{X : Type u}
{x : X}
{p : PUnit.{u + 1} }
:
(CategoryTheory.MonoidalCategory.leftUnitor X).hom (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} }
:
(CategoryTheory.MonoidalCategory.rightUnitor X).hom (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.
Equations
- F.mapPi n β = (F.mapIso (Equiv.piFinSucc n β).toIso).trans (CategoryTheory.asIso (F.μ β (Fin n → β))).symm