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