Nuprl Definition : eq1-meaning
eq1-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))=1)))
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-one: (i=1),
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-one: (i=1),
ctt-term-term: term(t),
allow: Error :allow
Latex:
eq1-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))=1)))
Date html generated:
2020_05_21-AM-10_39_13
Last ObjectModification:
2020_05_05-PM-04_23_05
Theory : cubical!type!theory
Home
Index