Nuprl Definition : cu_filler_2
cu_filler_2(J;K;L;f;g;x;i;box;X) ==
case l-first(y.¬bisname(f y);J)
of inl(y) =>
cu-cube-restriction(cube(get_face(y;f y;box));K;L;g;((x:=i) o f);X)
| inr(_) =>
case l-first(y.¬bisname((f o g) y);J) of inl(y) => 44 | inr(_) => 55
Definitions occuring in Statement :
cu-cube-restriction: cu-cube-restriction(alpha;L;J;f;a;T),
get_face: get_face(y;c;box),
face-cube: cube(f),
name-comp: (f o g),
face-map: (x:=i),
isname: isname(z),
l-first: l-first(x.f[x];L),
bnot: ¬bb,
apply: f a,
decide: case b of inl(x) => s[x] | inr(y) => t[y],
natural_number: $n
Definitions occuring in definition :
cu-cube-restriction: cu-cube-restriction(alpha;L;J;f;a;T),
face-cube: cube(f),
get_face: get_face(y;c;box),
face-map: (x:=i),
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),
apply: f a,
name-comp: (f o g),
natural_number: $n
FDL editor aliases :
cu_filler_2
cu_filler_2
Latex:
cu\_filler\_2(J;K;L;f;g;x;i;box;X) ==
case l-first(y.\mneg{}\msubb{}isname(f y);J)
of inl(y) =>
cu-cube-restriction(cube(get\_face(y;f y;box));K;L;g;((x:=i) o f);X)
| inr($_{}$) =>
case l-first(y.\mneg{}\msubb{}isname((f o g) y);J) of inl(y) => 44 | inr($_{}$) => 55
Date html generated:
2016_06_16-PM-08_09_42
Last ObjectModification:
2015_09_23-AM-09_35_21
Theory : cubical!sets
Home
Index