Nuprl Definition : cubical-universe
c𝕌 == <λI.{unit-cube(I) ⊢ _(Kan)}, λI,J,f,AK. (AK)unit-cube-map(f)>
Wellformedness Lemmas :
cubical-universe_wf
Definitions occuring in Statement :
csm-Kan-cubical-type: (AK)s,
Kan-cubical-type: {X ⊢ _(Kan)},
unit-cube-map: unit-cube-map(f),
unit-cube: unit-cube(I),
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
pair: <a, b>,
Kan-cubical-type: {X ⊢ _(Kan)},
lambda: λx.A[x],
csm-Kan-cubical-type: (AK)s,
unit-cube: unit-cube(I),
unit-cube-map: unit-cube-map(f)
FDL editor aliases :
c-univ
c-univ
Latex:
c\mBbbU{} == <\mlambda{}I.\{unit-cube(I) \mvdash{} \_(Kan)\}, \mlambda{}I,J,f,AK. (AK)unit-cube-map(f)>
Date html generated:
2016_06_16-PM-08_06_39
Last ObjectModification:
2015_09_23-AM-09_34_58
Theory : cubical!sets
Home
Index