Nuprl Definition : ctt-level-comp
Comp(X;lvl;T) ==
if (lvl =z 0) then composition-structure{i''':l, i:l}(X; T)
if (lvl =z 1) then composition-structure{i''':l, i':l}(X; T)
if (lvl =z 2) then composition-structure{i''':l, i'':l}(X; T)
else composition-structure{i''':l, i''':l}(X; T)
fi
Definitions occuring in Statement :
composition-structure: Gamma ⊢ Compositon(A),
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,
composition-structure: Gamma ⊢ Compositon(A)
FDL editor aliases :
ctt-level-comp
ctt-level-comp
Latex:
Comp(X;lvl;T) ==
if (lvl =\msubz{} 0) then composition-structure\{i''':l, i:l\}(X; T)
if (lvl =\msubz{} 1) then composition-structure\{i''':l, i':l\}(X; T)
if (lvl =\msubz{} 2) then composition-structure\{i''':l, i'':l\}(X; T)
else composition-structure\{i''':l, i''':l\}(X; T)
fi
Date html generated:
2020_05_20-PM-07_46_43
Last ObjectModification:
2020_05_06-PM-00_43_34
Theory : cubical!type!theory
Home
Index