(𝟙_ C ⟶ -)
is a lax monoidal functor to Type
#
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
def
category_theory.coyoneda_tensor_unit
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
(𝟙_ 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' := _}