Nuprl Definition : univ-comp
univ-comp{i:l}() == cfun-to-cop(();c𝕌;compU())
Definitions occuring in Statement :
compU: compU(),
cubical-universe: c𝕌,
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp),
trivial-cube-set: ()
Definitions occuring in definition :
compU: compU(),
cubical-universe: c𝕌,
trivial-cube-set: (),
comp-fun-to-comp-op: cfun-to-cop(Gamma;A;comp)
FDL editor aliases :
univ-comp
Latex:
univ-comp\{i:l\}() == cfun-to-cop(();c\mBbbU{};compU())
Date html generated:
2017_01_10-PM-00_15_24
Last ObjectModification:
2016_12_26-PM-10_35_56
Theory : cubical!type!theory
Home
Index