Nuprl Definition : ctt-level-type

{X ⊢lvl _} ==  if (lvl =z 0) then {X ⊢ _} if (lvl =z 1) then {X ⊢' _} if (lvl =z 2) then {X ⊢'' _} else {X ⊢''' _} fi 


Definitions occuring in Statement :  cubical-type: {X ⊢ _},  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  natural_number: $n
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  natural_number: $n,  cubical-type: {X ⊢ _}
FDL editor aliases :  ctt-level-type ctt-level-type ctt-level-type
Latex:
\{X  \mvdash{}lvl  \_\}  ==
    if  (lvl  =\msubz{}  0)  then  \{X  \mvdash{}  \_\}
    if  (lvl  =\msubz{}  1)  then  \{X  \mvdash{}'  \_\}
    if  (lvl  =\msubz{}  2)  then  \{X  \mvdash{}''  \_\}
    else  \{X  \mvdash{}'''  \_\}
    fi 


Date html generated: 2020_05_20-PM-07_45_09
Last ObjectModification: 2020_05_04-AM-09_22_47

Theory : cubical!type!theory


Home Index