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 :
fdl-hom: fdl-hom(L;f),
free-dl-generator: free-dl-generator(x),
free-dl: free-dl(X),
mk-functor: mk-functor,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
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:
2020_05_20-AM-09_00_15
Last ObjectModification:
2020_01_16-PM-05_08_05
Theory : lattices
Home
Index