Nuprl Definition : groupoid-nerve-filler1

groupoid-nerve-filler1(G;I;J;x;i;box) ==
  <λc.nerve_box_label(box;c)
  , λc1,c2,p. poset_functor_extend(cat(G);I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge1(G;box;x;i;hd(J);c;y);c1;c2)
  >


Definitions occuring in Statement :  nerve_box_edge1: nerve_box_edge1(G;box;x;i;j;c;y),  nerve_box_label: nerve_box_label(box;L),  poset_functor_extend: poset_functor_extend(C;I;L;E;c1;c2),  groupoid-cat: cat(G),  hd: hd(l),  lambda: λx.A[x],  pair: <a, b>
Definitions occuring in definition :  pair: <a, b>,  poset_functor_extend: poset_functor_extend(C;I;L;E;c1;c2),  groupoid-cat: cat(G),  nerve_box_label: nerve_box_label(box;L),  lambda: λx.A[x],  nerve_box_edge1: nerve_box_edge1(G;box;x;i;j;c;y),  hd: hd(l)
FDL editor aliases :  groupoid-nerve-filler1
Latex:
groupoid-nerve-filler1(G;I;J;x;i;box)  ==
    <\mlambda{}c.nerve\_box\_label(box;c)
    ,  \mlambda{}c1,c2,p.  poset\_functor\_extend(cat(G);I;\mlambda{}c.nerve\_box\_label(box;c);
                                                                      \mlambda{}y,c.  nerve\_box\_edge1(G;box;x;i;hd(J);c;y);c1;c2)
    >


Date html generated: 2016_06_16-PM-07_13_29
Last ObjectModification: 2015_09_23-AM-09_33_46

Theory : cubical!sets


Home Index