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