Nuprl Definition : ctt-type-meaning
cttType(X) == lvl:ℕ4 × T:{X ⊢lvl _} × Comp(X;lvl;T)
Definitions occuring in Statement :
ctt-level-comp: Comp(X;lvl;T),
ctt-level-type: {X ⊢lvl _},
int_seg: {i..j-},
product: x:A × B[x],
natural_number: $n
Definitions occuring in definition :
int_seg: {i..j-},
natural_number: $n,
product: x:A × B[x],
ctt-level-type: {X ⊢lvl _},
ctt-level-comp: Comp(X;lvl;T)
FDL editor aliases :
ctt-type-meaning
ctt-type-meaning
Latex:
cttType(X) == lvl:\mBbbN{}4 \mtimes{} T:\{X \mvdash{}lvl \_\} \mtimes{} Comp(X;lvl;T)
Date html generated:
2020_05_20-PM-07_56_04
Last ObjectModification:
2020_05_06-PM-01_17_48
Theory : cubical!type!theory
Home
Index