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.
@[protected, instance]
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