Lean4
/-- The Hom bifunctor sending a type `X` and a commutative monoid `M` to the commutative monoid
`X → M` with pointwise operations.
This is also the coyoneda embedding of `Type` into `CommMonCat`-valued presheaves of commutative
monoids. -/
@[to_additive (attr := simps) /--
The Hom bifunctor sending a type `X` and a commutative monoid `M` to the commutative monoid
`X → M` with pointwise operations.
This is also the coyoneda embedding of `Type` into `AddCommMonCat`-valued presheaves of commutative
monoids. -/
]
def coyonedaType : (Type u)ᵒᵖ ⥤ CommMonCat.{u} ⥤ CommMonCat.{u}
where
obj
X :=
{ obj M := of <| X.unop → M
map f := ofHom <| Pi.monoidHom fun i ↦ f.hom.comp <| Pi.evalMonoidHom _ i }
map f := { app N := ofHom <| Pi.monoidHom fun i ↦ Pi.evalMonoidHom _ <| f.unop i }
