Nuprl Definition : inv-meaning
inv-meaning{i:l}(A) ==
let Xa,a,ma = A in
provision(allowed(ma) ∧ type(allow(ma))=𝕀; mk-ctt-term-mng(level(allow(ma)); 𝕀; 1-(term(allow(ma)))))
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),
interval-rev: 1-(r),
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),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ctt-term-level: level(t),
interval-type: 𝕀,
interval-rev: 1-(r),
ctt-term-term: term(t),
allow: Error :allow
Latex:
inv-meaning\{i:l\}(A) ==
let Xa,a,ma = A in
provision(allowed(ma) \mwedge{} type(allow(ma))=\mBbbI{};
mk-ctt-term-mng(level(allow(ma)); \mBbbI{}; 1-(term(allow(ma)))))
Date html generated:
2020_05_21-AM-10_40_37
Last ObjectModification:
2020_05_05-PM-04_35_10
Theory : cubical!type!theory
Home
Index