Yoneda embedding

The Yoneda embedding $よ$ is an embedding of a locally small category into the Category of presheaves, that

maps an object to the presheaf $よ$
maps a morphism to the natural transformation $よ$ , whose components are the pushforwards of

Proof of embedding

Let . By the Yoneda lemma we have

よ よ よ よ

where using the notation of the proof of the Yoneda lemma given $よ$ and

よ よ

so $よ$ , implying

よ よ

so in particular, $よ$ is fully faithful. $よ$ is also clearly injective on objects, since if $よよ$ then

よ よ

so .

#state/tidy | #lang/en | #SemBr