Nuprl Definition : universe-term
t𝕌 == encode(c𝕌;univ-comp{i:l}())
Definitions occuring in Statement :
univ-comp: univ-comp{i:l}(),
universe-encode: encode(T;cT),
cubical-universe: c𝕌,
trivial-cube-set: ()
Definitions occuring in definition :
univ-comp: univ-comp{i:l}(),
cubical-universe: c𝕌,
trivial-cube-set: (),
universe-encode: encode(T;cT)
FDL editor aliases :
t-uni
Latex:
t\mBbbU{} == encode(c\mBbbU{};univ-comp\{i:l\}())
Date html generated:
2017_01_10-PM-00_16_20
Last ObjectModification:
2016_12_26-PM-10_41_24
Theory : cubical!type!theory
Home
Index