Nuprl Definition : ctt-type-meaning1
ctt-type-meaning1{i:l}(X) == lvl:ℕ4 × {X ⊢lvl _} × Top
Definitions occuring in Statement :
ctt-level-type: {X ⊢lvl _},
int_seg: {i..j-},
top: Top,
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 _},
top: Top
FDL editor aliases :
ctt-type-meaning1
Latex:
ctt-type-meaning1\{i:l\}(X) == lvl:\mBbbN{}4 \mtimes{} \{X \mvdash{}lvl \_\} \mtimes{} Top
Date html generated:
2020_05_20-PM-07_55_24
Last ObjectModification:
2020_05_05-AM-09_37_01
Theory : cubical!type!theory
Home
Index