Nuprl Definition : cu-box-in-box
cu-box-in-box(I;box) ==
{u:i:ℕ||box|| ⟶ cu-cube-family(cube(box[i]);I-[dimension(box[i])];1)|
∀i,j:ℕ||box||.
((¬(dimension(box[i]) = dimension(box[j]) ∈ Cname))
⇒ (cu-cube-restriction(cube(box[i]);I-[dimension(box[i])];I-[dimension(box[i]); dimension(box[j])];
(dimension(box[j]):=direction(box[j]));1;u i)
= cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]); dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)
∈ cu-cube-family(cube(box[i]);I-[dimension(box[i]);
dimension(box[j])];(1 o (dimension(box[j]):=direction(box[j]))))))}
Definitions occuring in Statement :
cu-cube-restriction: cu-cube-restriction(alpha;L;J;f;a;T),
cu-cube-family: cu-cube-family(alpha;L;f),
face-cube: cube(f),
face-direction: direction(f),
face-dimension: dimension(f),
name-comp: (f o g),
face-map: (x:=i),
id-morph: 1,
cname_deq: CnameDeq,
coordinate_name: Cname,
list-diff: as-bs,
select: L[n],
length: ||as||,
cons: [a / b],
nil: [],
int_seg: {i..j-},
all: ∀x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
natural_number: $n,
equal: s = t ∈ T
Definitions occuring in definition :
face-dimension: dimension(f),
cons: [a / b],
cname_deq: CnameDeq,
list-diff: as-bs,
select: L[n],
face-cube: cube(f),
cu-cube-restriction: cu-cube-restriction(alpha;L;J;f;a;T),
apply: f a,
nil: [],
id-morph: 1,
face-direction: direction(f),
face-map: (x:=i),
name-comp: (f o g),
cu-cube-family: cu-cube-family(alpha;L;f),
equal: s = t ∈ T,
coordinate_name: Cname,
not: ¬A,
implies: P ⇒ Q,
length: ||as||,
natural_number: $n,
int_seg: {i..j-},
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
set: {x:A| B[x]}
FDL editor aliases :
cu-box-in-box
cu-box-in-box
Latex:
cu-box-in-box(I;box) ==
\{u:i:\mBbbN{}||box|| {}\mrightarrow{} cu-cube-family(cube(box[i]);I-[dimension(box[i])];1)|
\mforall{}i,j:\mBbbN{}||box||.
((\mneg{}(dimension(box[i]) = dimension(box[j])))
{}\mRightarrow{} (cu-cube-restriction(cube(box[i]);I-[dimension(box[i])];I-[dimension(box[i]);
dimension(box[j])];
(dimension(box[j]):=direction(box[j]));1;u i)
= cu-cube-restriction(cube(box[j]);I-[dimension(box[j])];I-[dimension(box[j]);
dimension(box[i])];
(dimension(box[i]):=direction(box[i]));1;u j)))\}
Date html generated:
2016_06_16-PM-08_08_24
Last ObjectModification:
2015_09_23-AM-09_35_13
Theory : cubical!sets
Home
Index