Nuprl Definition : eq1-meaning

eq1-meaning{i:l}(Z) ==
  let X,t,m 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