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