Nuprl Definition : ss-cat
ss-cat{i:l}() == Cat(ob = SeparationSpace;arrow(X,Y) = {f:Point(X) ⟶ Point(Y)| ss-map(X;Y;f)} ;id(X) = λp.p;comp(X,Y,Z\000C,f,g) = g o f)
Definitions occuring in Statement :
ss-map: ss-map(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-map: ss-map(X;Y;f),
lambda: λx.A[x],
compose: f o g
FDL editor aliases :
ss-cat
Latex:
ss-cat\{i:l\}() == Cat(ob = SeparationSpace;arrow(X,Y) = \{f:Point(X) {}\mrightarrow{} Point(Y)| ss-map(X;Y;f)\} ;id(\000CX) = \mlambda{}p.p;comp(X,Y,Z,f,g) = g o f)
Date html generated:
2019_10_31-AM-07_27_38
Last ObjectModification:
2019_03_19-PM-03_43_01
Theory : constructive!algebra
Home
Index