Nuprl Definition : max-meaning
max-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),
interval-join: r ∨ s,
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,
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),
interval-type: 𝕀,
interval-join: r ∨ s,
ctt-term-term: term(t),
allow: Error :allow
Latex:
max-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))=\mBbbI{} \mwedge{} type(allow(mb))=\mBbbI{};
mk-ctt-term-mng(levelsup(level(allow(ma));level(allow(mb))); \mBbbI{};
term(allow(ma)) \mvee{} term(allow(mb))))
Date html generated:
2020_05_21-AM-10_40_04
Last ObjectModification:
2020_05_05-PM-04_53_13
Theory : cubical!type!theory
Home
Index