Nuprl Definition : cu_filler_1
cu_filler_1{i:l}(I;J;K;f;x;i;box) ==
case l-first(y.¬bisname(f y);J)
of inl(y) =>
cu-cube-family(cube(get_face(y;f y;box));K;((x:=i) o f))
| inr(_) =>
cu-box-in-box([fresh-cname(K) / K];open_box_image(c𝕌;I;[fresh-cname(K) / K];f[x:=fresh-cname(K)];box))
Definitions occuring in Statement :
cu-box-in-box: cu-box-in-box(I;box),
cu-cube-family: cu-cube-family(alpha;L;f),
cubical-universe: c𝕌,
open_box_image: open_box_image(X;I;K;f;bx),
get_face: get_face(y;c;box),
face-cube: cube(f),
name-comp: (f o g),
face-map: (x:=i),
extend-name-morph: f[z1:=z2],
isname: isname(z),
fresh-cname: fresh-cname(I),
l-first: l-first(x.f[x];L),
cons: [a / b],
bnot: ¬bb,
apply: f a,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :
decide: case b of inl(x) => s[x] | inr(y) => t[y],
l-first: l-first(x.f[x];L),
bnot: ¬bb,
isname: isname(z),
cu-cube-family: cu-cube-family(alpha;L;f),
face-cube: cube(f),
get_face: get_face(y;c;box),
apply: f a,
name-comp: (f o g),
face-map: (x:=i),
cu-box-in-box: cu-box-in-box(I;box),
open_box_image: open_box_image(X;I;K;f;bx),
cubical-universe: c𝕌,
cons: [a / b],
extend-name-morph: f[z1:=z2],
fresh-cname: fresh-cname(I)
FDL editor aliases :
cu_filler_1
cu_filler_1
Latex:
cu\_filler\_1\{i:l\}(I;J;K;f;x;i;box) ==
case l-first(y.\mneg{}\msubb{}isname(f y);J)
of inl(y) =>
cu-cube-family(cube(get\_face(y;f y;box));K;((x:=i) o f))
| inr($_{}$) =>
cu-box-in-box([fresh-cname(K) / K];open\_box\_image(c\mBbbU{};I;[fresh-cname(K) /
K];f[x:=fresh-cname(K)];box))
Date html generated:
2016_06_16-PM-08_09_26
Last ObjectModification:
2015_09_23-AM-09_35_17
Theory : cubical!sets
Home
Index