Nuprl Definition : representable-cube-set
representable-cube-set() == {G:cubical_set{1:l}| ∃I:fset(ℕ). (G = formal-cube(I) ∈ cubical_set{1:l})}
Definitions occuring in Statement :
formal-cube: formal-cube(I),
cubical_set: CubicalSet,
fset: fset(T),
nat: ℕ,
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions occuring in definition :
set: {x:A| B[x]} ,
exists: ∃x:A. B[x],
fset: fset(T),
nat: ℕ,
equal: s = t ∈ T,
cubical_set: CubicalSet,
formal-cube: formal-cube(I)
FDL editor aliases :
representable-cube-set
Latex:
representable-cube-set() == \{G:cubical\_set\{1:l\}| \mexists{}I:fset(\mBbbN{}). (G = formal-cube(I))\}
Date html generated:
2018_05_23-AM-08_34_16
Last ObjectModification:
2017_11_09-AM-11_41_57
Theory : cubical!type!theory
Home
Index