Nuprl Definition : ctt-term-meaning
cttTerm(X) == lvl:ℕ4 × T:{X ⊢lvl _} × {X ⊢ _:T}
Definitions occuring in Statement :
ctt-level-type: {X ⊢lvl _},
cubical-term: {X ⊢ _:A},
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 _},
cubical-term: {X ⊢ _:A}
FDL editor aliases :
ctt-term-meaning
ctt-term-meaning
Latex:
cttTerm(X) == lvl:\mBbbN{}4 \mtimes{} T:\{X \mvdash{}lvl \_\} \mtimes{} \{X \mvdash{} \_:T\}
Date html generated:
2020_05_20-PM-07_49_48
Last ObjectModification:
2020_05_04-AM-09_37_59
Theory : cubical!type!theory
Home
Index