Nuprl Definition : decode-meaning
decode-meaning{i:l}(n; A) ==
let Xa,a,ma = A in
provision(allowed(ma) ∧ type(allow(ma))=if (n =z 0) then c𝕌 if (n =z 1) then c𝕌' else c𝕌'' fi ;
let t = term(allow(ma)) in
cttType(levl= n
type= decode(t)
comp= CompFun(t)))
Definitions occuring in Statement :
context-set: context-set(ctxt),
mk_ctt-type-mng: mk_ctt-type-mng,
ctt-term-term: term(t),
ctt-term-type-is: type(t)=T,
universe-comp-fun: CompFun(A),
universe-decode: decode(t),
cubical-universe: c𝕌,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
let: let,
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,
ctt-term-type-is: type(t)=T,
context-set: context-set(ctxt),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
cubical-universe: c𝕌,
let: let,
ctt-term-term: term(t),
allow: Error :allow,
mk_ctt-type-mng: mk_ctt-type-mng,
universe-decode: decode(t),
universe-comp-fun: CompFun(A)
Latex:
decode-meaning\{i:l\}(n; A) ==
let Xa,a,ma = A in
provision(allowed(ma) \mwedge{} type(allow(ma))=if (n =\msubz{} 0) then c\mBbbU{} if (n =\msubz{} 1) then c\mBbbU{}' else c\mBbbU{}'' fi ;
let t = term(allow(ma)) in
cttType(levl= n
type= decode(t)
comp= CompFun(t)))
Date html generated:
2020_05_21-AM-10_45_05
Last ObjectModification:
2020_05_07-PM-04_58_20
Theory : cubical!type!theory
Home
Index