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 :
cat-comp: cat-comp(C),
apply: f a,
lambda: λx.A[x],
mk-nat-trans: x |→ T[x],
rep-pre-sheaf: rep-pre-sheaf(C;X),
mk-functor: mk-functor
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:
2017_01_19-PM-02_53_06
Last ObjectModification:
2017_01_13-PM-01_29_08
Theory : small!categories
Home
Index