Nuprl Definition : groupoid-nerve-filler

groupoid-nerve-filler(G;I;J;x;i;box) ==
  if null(J) then groupoid-nerve-filler0(I;x;box)
  if 3 <||box|| then groupoid-nerve-filler2(cat(G);I;J;box)
  else groupoid-nerve-filler1(G;I;J;x;i;box)
  fi 



Definitions occuring in Statement :  groupoid-nerve-filler2: groupoid-nerve-filler2(C;I;J;box) groupoid-nerve-filler1: groupoid-nerve-filler1(G;I;J;x;i;box) groupoid-nerve-filler0: groupoid-nerve-filler0(I;x;box) groupoid-cat: cat(G) length: ||as|| null: null(as) ifthenelse: if then else fi  lt_int: i <j natural_number: $n
Definitions occuring in definition :  null: null(as) groupoid-nerve-filler0: groupoid-nerve-filler0(I;x;box) ifthenelse: if then else fi  lt_int: i <j natural_number: $n length: ||as|| groupoid-nerve-filler2: groupoid-nerve-filler2(C;I;J;box) groupoid-cat: cat(G) groupoid-nerve-filler1: groupoid-nerve-filler1(G;I;J;x;i;box)
FDL editor aliases :  groupoid-nerve-filler

Latex:
groupoid-nerve-filler(G;I;J;x;i;box)  ==
    if  null(J)  then  groupoid-nerve-filler0(I;x;box)
    if  3  <z  ||box||  then  groupoid-nerve-filler2(cat(G);I;J;box)
    else  groupoid-nerve-filler1(G;I;J;x;i;box)
    fi 



Date html generated: 2016_06_16-PM-07_13_54
Last ObjectModification: 2015_09_23-AM-09_33_52

Theory : cubical!sets


Home Index