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 I K (f o g)) = ((F J K g) o (F I J f)) ∈ ((X I) ⟶ (X K))))
∧ (∀I:Cname List. ((F I I 1) = (λx.x) ∈ ((X I) ⟶ (X I))))}
Definitions occuring in Statement :
name-comp: (f o g),
id-morph: 1,
name-morph: name-morph(I;J),
coordinate_name: Cname,
list: T List,
compose: f o g,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: λx.A[x],
function: x:A ⟶ B[x],
spread: spread def,
product: x:A × B[x],
universe: Type,
equal: s = 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 o g),
compose: f o g,
all: ∀x:A. B[x],
list: T List,
coordinate_name: Cname,
equal: s = t ∈ T,
function: x:A ⟶ B[x],
apply: f 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