Nuprl Definition : encode-meaning
encode-meaning{i:l}(n; A) ==
let Xa,a,ma = A in
provision(allowed(ma) ∧ level(allow(ma)) < n; mk-ctt-term-mng(n; if (n =z 1) then c𝕌
if (n =z 2) then c𝕌'
else c𝕌''
fi ; encode(type(allow(ma));
cfun-to-cop(context-set(Xa);type(allow(ma))
;comp(allow(ma))))))
Definitions occuring in Statement :
context-set: context-set(ctxt),
ctt-type-comp: comp(T),
ctt-type-type: type(T),
ctt-type-level: level(T),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
universe-encode: encode(T;cT),
cubical-universe: c𝕌,
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
less_than: a < b,
spreadn: spread3,
and: P ∧ Q,
natural_number: $n,
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,
less_than: a < b,
ctt-type-level: level(T),
mk-ctt-term-mng: mk-ctt-term-mng(lvl; T; t),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
cubical-universe: c𝕌,
universe-encode: encode(T;cT),
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
context-set: context-set(ctxt),
ctt-type-type: type(T),
ctt-type-comp: comp(T),
allow: Error :allow
Latex:
encode-meaning\{i:l\}(n; A) ==
let Xa,a,ma = A in
provision(allowed(ma) \mwedge{} level(allow(ma)) < n;
mk-ctt-term-mng(n; if (n =\msubz{} 1) then c\mBbbU{}
if (n =\msubz{} 2) then c\mBbbU{}'
else c\mBbbU{}''
fi ; encode(type(allow(ma));cfun-to-cop(context-set(Xa);type(allow(ma))
;comp(allow(ma))))))
Date html generated:
2020_05_21-AM-10_45_22
Last ObjectModification:
2020_05_07-PM-05_23_18
Theory : cubical!type!theory
Home
Index