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