Library
▹
Category theory
▹
Yoneda lemma
Hom
v
(
A
, −)
yoneda
yoneda(
F
,
A
) is bijective and (yoneda(
F
,
A
))
-1
= (
(
F
(
A
))
→
Nat(Hom
v
(
A
, −),
F
)
x
↦
(
Hom(
A
,
X
)
→
(
F
(
X
))
f
↦
F
(
f
)(
x
)
)
X
∈
C
)
if
u
,
v
∈ ℕ,
C
is a/an
u
-small category,
F
:
C
→
Set
v
is a functor,
A
∈
C