The category of types is a symmetric monoidal category #
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
def
category_theory.coyoneda_tensor_unit
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
category_theory.lax_monoidal_functor C (Type v)
(𝟙_ C ⟶ -)
is a lax monoidal functor to Type
.
Equations
- category_theory.coyoneda_tensor_unit C = {to_functor := {obj := (category_theory.coyoneda.obj (opposite.op (𝟙_ C))).obj, map := (category_theory.coyoneda.obj (opposite.op (𝟙_ C))).map, map_id' := _, map_comp' := _}, ε := λ (p : 𝟙_ (Type v)), 𝟙 (opposite.unop (opposite.op (𝟙_ C))), μ := λ (X Y : C) (p : {obj := (category_theory.coyoneda.obj (opposite.op (𝟙_ C))).obj, map := (category_theory.coyoneda.obj (opposite.op (𝟙_ C))).map, map_id' := _, map_comp' := _}.obj X ⊗ {obj := (category_theory.coyoneda.obj (opposite.op (𝟙_ C))).obj, map := (category_theory.coyoneda.obj (opposite.op (𝟙_ C))).map, map_id' := _, map_comp' := _}.obj Y), (λ_ (𝟙_ C)).inv ≫ (p.fst ⊗ p.snd), μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}
noncomputable
def
category_theory.monoidal_functor.map_pi
{C : Type u_1}
[category_theory.category C]
[category_theory.monoidal_category C]
(F : category_theory.monoidal_functor (Type u_3) C)
(n : ℕ)
(β : Type u_3) :
F.to_lax_monoidal_functor.to_functor.obj (fin (n + 1) → β) ≅ F.to_lax_monoidal_functor.to_functor.obj β ⊗ F.to_lax_monoidal_functor.to_functor.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.map_pi n β = F.to_lax_monoidal_functor.to_functor.map_iso (equiv.pi_fin_succ n β).to_iso ≪≫ (category_theory.as_iso (F.to_lax_monoidal_functor.μ β (fin n → β))).symm