Nuprl Definition : Kan-A-filler
Kan-A-filler(X;A;filler) ==
∀I:Cname List. ∀alpha:X(I). ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:A-open-box(X;A;I;alpha;J;x;i).
fills-A-open-box(X;A;I;alpha;bx;filler I alpha J x i bx)
Definitions occuring in Statement :
fills-A-open-box: fills-A-open-box(X;A;I;alpha;bx;cube),
A-open-box: A-open-box(X;A;I;alpha;J;x;i),
I-cube: X(I),
nameset: nameset(L),
coordinate_name: Cname,
list: T List,
int_seg: {i..j-},
all: ∀x:A. B[x],
apply: f a,
natural_number: $n
Definitions occuring in definition :
coordinate_name: Cname,
I-cube: X(I),
list: T List,
nameset: nameset(L),
int_seg: {i..j-},
natural_number: $n,
all: ∀x:A. B[x],
A-open-box: A-open-box(X;A;I;alpha;J;x;i),
fills-A-open-box: fills-A-open-box(X;A;I;alpha;bx;cube),
apply: f a
FDL editor aliases :
Kan-A-filler
Latex:
Kan-A-filler(X;A;filler) ==
\mforall{}I:Cname List. \mforall{}alpha:X(I). \mforall{}J:nameset(I) List. \mforall{}x:nameset(I). \mforall{}i:\mBbbN{}2.
\mforall{}bx:A-open-box(X;A;I;alpha;J;x;i).
fills-A-open-box(X;A;I;alpha;bx;filler I alpha J x i bx)
Date html generated:
2016_06_16-PM-06_43_17
Last ObjectModification:
2015_09_23-AM-09_32_05
Theory : cubical!sets
Home
Index