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