### Nuprl Definition : cubical-set

CubicalSet ==
{XF:X:L:(Cname List) ⟶ Type × (I:(Cname List) ⟶ J:(Cname List) ⟶ name-morph(I;J) ⟶ (X I) ⟶ (X J))|
let X,F XF
in (∀I,J,K:Cname List. ∀f:name-morph(I;J). ∀g:name-morph(J;K).
((F (f g)) ((F g) (F f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((F 1) x.x) ∈ ((X I) ⟶ (X I))))}

Definitions occuring in Statement :  name-comp: (f g) id-morph: 1 name-morph: name-morph(I;J) coordinate_name: Cname list: List compose: g all: x:A. B[x] and: P ∧ Q set: {x:A| B[x]}  apply: a lambda: λx.A[x] function: x:A ⟶ B[x] spread: spread def product: x:A × B[x] universe: Type equal: t ∈ T
Definitions occuring in definition :  set: {x:A| B[x]}  product: x:A × B[x] universe: Type spread: spread def and: P ∧ Q name-morph: name-morph(I;J) name-comp: (f g) compose: g all: x:A. B[x] list: List coordinate_name: Cname equal: t ∈ T function: x:A ⟶ B[x] apply: a id-morph: 1 lambda: λx.A[x]
FDL editor aliases :  c-set

Latex:
CubicalSet  ==
\{XF:X:L:(Cname  List)  {}\mrightarrow{}  Type  \mtimes{}  (I:(Cname  List)
{}\mrightarrow{}  J:(Cname  List)
{}\mrightarrow{}  name-morph(I;J)
{}\mrightarrow{}  (X  I)
{}\mrightarrow{}  (X  J))|
let  X,F  =  XF
in  (\mforall{}I,J,K:Cname  List.  \mforall{}f:name-morph(I;J).  \mforall{}g:name-morph(J;K).
((F  I  K  (f  o  g))  =  ((F  J  K  g)  o  (F  I  J  f))))
\mwedge{}  (\mforall{}I:Cname  List.  ((F  I  I  1)  =  (\mlambda{}x.x)))\}

Date html generated: 2016_06_16-PM-05_35_38
Last ObjectModification: 2015_09_23-AM-09_29_50

Theory : cubical!sets

Home Index