Nuprl Definition : yoneda-embedding
yoneda-embedding(C) == functor(ob(X) = rep-pre-sheaf(C;X);arrow(X,Y,f) = A |→ λg.(cat-comp(C) A X Y g f))
Definitions occuring in Statement :
rep-pre-sheaf: rep-pre-sheaf(C;X),
mk-nat-trans: x |→ T[x],
mk-functor: mk-functor,
cat-comp: cat-comp(C),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mk-functor: mk-functor,
rep-pre-sheaf: rep-pre-sheaf(C;X),
mk-nat-trans: x |→ T[x],
lambda: λx.A[x],
apply: f a,
cat-comp: cat-comp(C)
FDL editor aliases :
yoneda-embedding
Latex:
yoneda-embedding(C) ==
functor(ob(X) = rep-pre-sheaf(C;X);
arrow(X,Y,f) = A |\mrightarrow{} \mlambda{}g.(cat-comp(C) A X Y g f))
Date html generated:
2020_05_20-AM-07_53_09
Last ObjectModification:
2017_01_13-PM-01_29_08
Theory : small!categories
Home
Index