Nuprl Definition : univ-meaning
univ-meaning{i:l}(n) ==
OK(if (n =z 0) then cttType(levl= 1type= c𝕌comp= compU())
if (n =z 1) then cttType(levl= 2type= c𝕌'comp= compU())
else cttType(levl= 3
type= c𝕌''
comp= compU())
fi )
Definitions occuring in Statement :
mk_ctt-type-mng: mk_ctt-type-mng,
compU: compU(),
cubical-universe: c𝕌,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
true: True,
natural_number: $n,
provision: provision(ok; v)
Definitions occuring in definition :
provision: Error :provision,
true: True,
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
mk_ctt-type-mng: mk_ctt-type-mng,
natural_number: $n,
cubical-universe: c𝕌,
compU: compU()
Latex:
univ-meaning\{i:l\}(n) ==
OK(if (n =\msubz{} 0) then cttType(levl= 1type= c\mBbbU{}comp= compU())
if (n =\msubz{} 1) then cttType(levl= 2type= c\mBbbU{}'comp= compU())
else cttType(levl= 3
type= c\mBbbU{}''
comp= compU())
fi )
Date html generated:
2020_05_21-AM-10_45_38
Last ObjectModification:
2020_05_05-PM-00_18_13
Theory : cubical!type!theory
Home
Index