Nuprl Definition : free-dl-functor
FreeDistLattice == functor(ob(X) = free-dl(X);arrow(X,Y,f) = fdl-hom(free-dl(Y);λx.free-dl-generator(f x)))
Definitions occuring in Statement :
mk-functor: mk-functor,
fdl-hom: fdl-hom(L;f),
free-dl-generator: free-dl-generator(x),
free-dl: free-dl(X),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mk-functor: mk-functor,
fdl-hom: fdl-hom(L;f),
free-dl: free-dl(X),
lambda: λx.A[x],
free-dl-generator: free-dl-generator(x),
apply: f a
FDL editor aliases :
free-dl-functor
Latex:
FreeDistLattice ==
functor(ob(X) = free-dl(X);
arrow(X,Y,f) = fdl-hom(free-dl(Y);\mlambda{}x.free-dl-generator(f x)))
Date html generated:
2017_02_21-AM-09_58_36
Last ObjectModification:
2017_01_23-PM-01_42_08
Theory : small!categories
Home
Index