Nuprl Definition : pathabs-meaning
pathabs-meaning{i:l}(A; B) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
provision(allowed(ma) ∧ allowed(mb) ∧ type(allow(mb))=(type(allow(ma)))p; let b = term(allow(mb)) in
mk-ctt-term-mng(level(allow(ma));
(Path_type(allow(ma))
(b)[0(𝕀)]
(b)[1(𝕀)]); <>(b))\000C)
Definitions occuring in Statement :
context-set: context-set(ctxt),
ctt-type-type: type(T),
ctt-type-level: level(T),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
term-to-path: <>(a),
path-type: (Path_A a b),
interval-1: 1(𝕀),
interval-0: 0(𝕀),
interval-type: 𝕀,
csm-id-adjoin: [u],
cc-fst: p,
cube-context-adjoin: X.A,
csm-ap-term: (t)s,
csm-ap-type: (AF)s,
let: let,
spreadn: spread3,
and: P ∧ Q,
allow: allow(x),
allowed: allowed(x),
provision: provision(ok; v)
Definitions occuring in definition :
spreadn: spread3,
provision: Error :provision,
and: P ∧ Q,
allowed: Error :allowed,
ctt-term-type-is: type(t)=T,
cube-context-adjoin: X.A,
interval-type: 𝕀,
csm-ap-type: (AF)s,
cc-fst: p,
let: let,
ctt-term-term: term(t),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-type-level: level(T),
path-type: (Path_A a b),
ctt-type-type: type(T),
allow: Error :allow,
interval-0: 0(𝕀),
csm-ap-term: (t)s,
csm-id-adjoin: [u],
interval-1: 1(𝕀),
term-to-path: <>(a),
context-set: context-set(ctxt)
Latex:
pathabs-meaning\{i:l\}(A; B) ==
let Xa,a,ma = A in
let Xb,b,mb = B in
provision(allowed(ma) \mwedge{} allowed(mb) \mwedge{} type(allow(mb))=(type(allow(ma)))p;
let b = term(allow(mb)) in
mk-ctt-term-mng(level(allow(ma)); (Path\_type(allow(ma)) (b)[0(\mBbbI{})] (b)[1(\mBbbI{})]); <>(b))\000C)
Date html generated:
2020_05_21-AM-10_42_00
Last ObjectModification:
2020_05_08-AM-10_06_58
Theory : cubical!type!theory
Home
Index