Nuprl Definition : full-faithful-functor
ff-functor(C;D;F) == ∀x,y:cat-ob(C). Bij(cat-arrow(C) x y;cat-arrow(D) (F x) (F y);F x y)
Definitions occuring in Statement :
functor-arrow: arrow(F),
functor-ob: 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: ob(F),
apply: f a,
functor-arrow: 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) (F x) (F y);F x y)
Date html generated:
2020_05_20-AM-07_51_10
Last ObjectModification:
2015_09_23-AM-09_29_09
Theory : small!categories
Home
Index