Nuprl Definition : free-group-functor
FreeGp == functor(ob(X) = free-group(X);arrow(X,Y,f) = fg-lift(free-group(Y);λx.free-letter(f x)))
Definitions occuring in Statement :
mk-functor: mk-functor,
fg-lift: fg-lift(G;f),
free-letter: free-letter(x),
free-group: free-group(X),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
apply: f a,
free-letter: free-letter(x),
lambda: λx.A[x],
free-group: free-group(X),
mk-functor: mk-functor
FDL editor aliases :
free-group-functor
Latex:
FreeGp == functor(ob(X) = free-group(X);arrow(X,Y,f) = fg-lift(free-group(Y);\mlambda{}x.free-letter(f x)))
Date html generated:
2017_01_19-PM-02_57_03
Last ObjectModification:
2017_01_16-AM-00_27_41
Theory : small!categories
Home
Index