Nuprl Definition : representable-psc
representable-psc(C) == {G:ps_context{1:l}(C)| ∃I:cat-ob(C). (G = Yoneda(I) ∈ ps_context{1:l}(C))}
Definitions occuring in Statement :
Yoneda: Yoneda(I),
ps_context: __⊢,
cat-ob: cat-ob(C),
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
exists: ∃x:A. B[x],
cat-ob: cat-ob(C),
equal: s = t ∈ T,
ps_context: __⊢,
Yoneda: Yoneda(I)
Latex:
representable-psc(C) == \{G:ps\_context\{1:l\}(C)| \mexists{}I:cat-ob(C). (G = Yoneda(I))\}
Date html generated:
2018_05_22-PM-09_59_32
Last ObjectModification:
2018_02_19-PM-06_28_57
Theory : presheaf!models!of!type!theory
Home
Index