Nuprl Definition : meet-meaning
meet-meaning{i:l}(A; B) ==
let Xa,a,ma = A in
let Xb,b,mb = B 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