Nuprl Definition : full-faithful-functor
ff-functor(C;D;F) ==
∀x,y:cat-ob(C). Bij(cat-arrow(C) x y;cat-arrow(D) (functor-ob(F) x) (functor-ob(F) y);functor-arrow(F) x y)
Definitions occuring in Statement :
functor-arrow: functor-arrow(F),
functor-ob: functor-ob(F),
cat-arrow: cat-arrow(C),
cat-ob: cat-ob(C),
biject: Bij(A;B;f),
all: ∀x:A. B[x],
apply: f a
Definitions occuring in definition :
all: ∀x:A. B[x],
cat-ob: cat-ob(C),
biject: Bij(A;B;f),
cat-arrow: cat-arrow(C),
functor-ob: functor-ob(F),
apply: f a,
functor-arrow: functor-arrow(F)
FDL editor aliases :
ff-functor
Latex:
ff-functor(C;D;F) ==
\mforall{}x,y:cat-ob(C).
Bij(cat-arrow(C) x y;cat-arrow(D) (functor-ob(F) x) (functor-ob(F) y);functor-arrow(F) x y)
Date html generated:
2016_05_18-AM-11_52_25
Last ObjectModification:
2015_09_23-AM-09_29_09
Theory : small!categories
Home
Index