mathlib documentation

category_theory.monoidal.types.coyoneda

`(𝟙_ C ⟶ -)` is a lax monoidal functor to `Type` #

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' := _}