Nuprl Definition : eq0-meaning
eq0-meaning{i:l}(Z) ==
let X,t,m = Z in
provision(allowed(m) ∧ type(allow(m))=𝕀; mk-ctt-term-mng(level(allow(m)); 𝔽; (term(allow(m))=0)))
Definitions occuring in Statement :
context-set: context-set(ctxt),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
ctt-term-level: level(t),
face-zero: (i=0),
face-type: 𝔽,
interval-type: 𝕀,
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,
context-set: context-set(ctxt),
interval-type: 𝕀,
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-term-level: level(t),
face-type: 𝔽,
face-zero: (i=0),
ctt-term-term: term(t),
allow: Error :allow
Latex:
eq0-meaning\{i:l\}(Z) ==
let X,t,m = Z in
provision(allowed(m) \mwedge{} type(allow(m))=\mBbbI{}; mk-ctt-term-mng(level(allow(m)); \mBbbF{}; (term(allow(m))=0)))
Date html generated:
2020_05_21-AM-10_38_57
Last ObjectModification:
2020_05_05-PM-04_28_55
Theory : cubical!type!theory
Home
Index