Nuprl Definition : full-ss-cat
full-ss-cat{i:l}() == Cat(ob = SeparationSpace;arrow(X,Y) = {f:Point(X) ⟶ Point(Y)| ss-function(X;Y;f)} ;id(X) = λp.p;\000Ccomp(X,Y,Z,f,g) = g o f)
Definitions occuring in Statement :
ss-function: ss-function(X;Y;f),
ss-point: Point(ss),
separation-space: SeparationSpace,
mk-cat: mk-cat,
compose: f o g,
set: {x:A| B[x]} ,
lambda: λx.A[x],
function: x:A ⟶ B[x]
Definitions occuring in definition :
mk-cat: mk-cat,
separation-space: SeparationSpace,
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
ss-point: Point(ss),
ss-function: ss-function(X;Y;f),
lambda: λx.A[x],
compose: f o g
FDL editor aliases :
full-ss-cat
Latex:
full-ss-cat\{i:l\}() ==
Cat(ob = SeparationSpace;
arrow(X,Y) = \{f:Point(X) {}\mrightarrow{} Point(Y)| ss-function(X;Y;f)\} ;
id(X) = \mlambda{}p.p;
comp(X,Y,Z,f,g) = g o f)
Date html generated:
2019_10_31-AM-07_27_41
Last ObjectModification:
2019_03_19-PM-03_43_04
Theory : constructive!algebra
Home
Index