Nuprl Definition : Kan-filler

Kan-filler(X;filler) ==
  ∀I:Cname List. ∀J:nameset(I) List. ∀x:nameset(I). ∀i:ℕ2. ∀bx:open_box(X;I;J;x;i).
    fills-open_box(X;I;bx;filler I J x i bx)


Definitions occuring in Statement :  fills-open_box: fills-open_box(X;I;bx;cube),  open_box: open_box(X;I;J;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,  list: T List,  nameset: nameset(L),  int_seg: {i..j-},  natural_number: $n,  all: ∀x:A. B[x],  open_box: open_box(X;I;J;x;i),  fills-open_box: fills-open_box(X;I;bx;cube),  apply: f a
FDL editor aliases :  Kan-filler
Latex:
Kan-filler(X;filler)  ==
    \mforall{}I:Cname  List.  \mforall{}J:nameset(I)  List.  \mforall{}x:nameset(I).  \mforall{}i:\mBbbN{}2.  \mforall{}bx:open\_box(X;I;J;x;i).
        fills-open\_box(X;I;bx;filler  I  J  x  i  bx)


Date html generated: 2016_06_16-PM-06_49_11
Last ObjectModification: 2015_09_23-AM-09_32_35

Theory : cubical!sets


Home Index