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 :
fg-lift: fg-lift(G;f),
free-letter: free-letter(x),
free-group: free-group(X),
mk-functor: mk-functor,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
fg-lift: fg-lift(G;f),
free-group: free-group(X),
lambda: λx.A[x],
free-letter: free-letter(x),
apply: f a
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:
2020_05_20-AM-08_23_14
Last ObjectModification:
2020_01_16-PM-05_09_36
Theory : free!groups
Home
Index