Nuprl Definition : meet-meaning

meet-meaning{i:l}(A; B) ==
  let Xa,a,ma in 
  let Xb,b,mb in 
  provision(allowed(ma) ∧ allowed(mb) ∧ type(allow(ma))=𝔽 ∧ type(allow(mb))=𝔽;
            mk-ctt-term-mng(levelsup(level(allow(ma));level(allow(mb))); 𝔽(term(allow(ma)) ∧ term(allow(mb)))))



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) levelsup: levelsup(x;y) face-and: (a ∧ b) face-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,  allowed: Error :allowed,  and: P ∧ Q ctt-term-type-is: type(t)=T context-set: context-set(ctxt) mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t) levelsup: levelsup(x;y) ctt-term-level: level(t) face-type: 𝔽 face-and: (a ∧ b) ctt-term-term: term(t) allow: Error :allow

Latex:
meet-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(ma))=\mBbbF{}  \mwedge{}  type(allow(mb))=\mBbbF{};
                        mk-ctt-term-mng(levelsup(level(allow(ma));level(allow(mb)));  \mBbbF{};
                                                        (term(allow(ma))  \mwedge{}  term(allow(mb)))))



Date html generated: 2020_05_21-AM-10_39_31
Last ObjectModification: 2020_05_05-PM-04_43_52

Theory : cubical!type!theory


Home Index