Nuprl Definition : named-path
named-path(X;A;a;b;I;alpha;z) == {omega:A(iota(z)(alpha))| name-path-endpoints(X;A;a;b;I;alpha;z;omega)}
Definitions occuring in Statement :
name-path-endpoints: name-path-endpoints(X;A;a;b;I;alpha;z;omega),
cubical-type-at: A(a),
cube-set-restriction: f(s),
iota: iota(x),
cons: [a / b],
set: {x:A| B[x]}
Definitions occuring in definition :
set: {x:A| B[x]} ,
cubical-type-at: A(a),
cube-set-restriction: f(s),
cons: [a / b],
iota: iota(x),
name-path-endpoints: name-path-endpoints(X;A;a;b;I;alpha;z;omega)
FDL editor aliases :
named-path
named-path
Latex:
named-path(X;A;a;b;I;alpha;z) ==
\{omega:A(iota(z)(alpha))| name-path-endpoints(X;A;a;b;I;alpha;z;omega)\}
Date html generated:
2016_06_16-PM-07_27_38
Last ObjectModification:
2015_09_23-AM-09_34_02
Theory : cubical!sets
Home
Index