Nuprl Definition : nerve_box_edge1

nerve_box_edge1(G;box;x;i;j;c;y) ==
  if (c x =z i) ∨b(¬beq-cname(y;j)) then nerve_box_edge(box;c;y)
  if (i =z 0)
    then groupoid-square1(G;nerve_box_label(box;flip(c;x));nerve_box_label(box;flip(flip(c;x);y));
         nerve_box_label(box;c);nerve_box_label(box;flip(c;y));nerve_box_edge(box;flip(c;x);y);
         nerve_box_edge(box;flip(flip(c;x);y);x);nerve_box_edge(box;flip(c;x);x))
  else groupoid-square2(G;nerve_box_label(box;c);nerve_box_label(box;flip(c;y));
       nerve_box_label(box;flip(c;x));nerve_box_label(box;flip(flip(c;y);x));nerve_box_edge(box;flip(c;y);x);
       nerve_box_edge(box;c;x);nerve_box_edge(box;flip(c;x);y))
  fi 


Definitions occuring in Statement :  nerve_box_edge: nerve_box_edge(box;c;y),  nerve_box_label: nerve_box_label(box;L),  name-morph-flip: flip(f;y),  eq-cname: eq-cname(x;y),  groupoid-square2: groupoid-square2(G;x00;x10;x01;x11;b;c;d),  groupoid-square1: groupoid-square1(G;x00;x10;x01;x11;a;b;c),  bor: p ∨bq,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  natural_number: $n
Definitions occuring in definition :  bor: p ∨bq,  apply: f a,  bnot: ¬bb,  eq-cname: eq-cname(x;y),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  natural_number: $n,  groupoid-square1: groupoid-square1(G;x00;x10;x01;x11;a;b;c),  groupoid-square2: groupoid-square2(G;x00;x10;x01;x11;b;c;d),  nerve_box_label: nerve_box_label(box;L),  nerve_box_edge: nerve_box_edge(box;c;y),  name-morph-flip: flip(f;y)
FDL editor aliases :  nerve_box_edge1
Latex:
nerve\_box\_edge1(G;box;x;i;j;c;y)  ==
    if  (c  x  =\msubz{}  i)  \mvee{}\msubb{}(\mneg{}\msubb{}eq-cname(y;j))  then  nerve\_box\_edge(box;c;y)
    if  (i  =\msubz{}  0)
        then  groupoid-square1(G;nerve\_box\_label(box;flip(c;x));nerve\_box\_label(box;flip(flip(c;x);y));
                  nerve\_box\_label(box;c);nerve\_box\_label(box;flip(c;y));nerve\_box\_edge(box;flip(c;x);y);
                  nerve\_box\_edge(box;flip(flip(c;x);y);x);nerve\_box\_edge(box;flip(c;x);x))
    else  groupoid-square2(G;nerve\_box\_label(box;c);nerve\_box\_label(box;flip(c;y));
              nerve\_box\_label(box;flip(c;x));nerve\_box\_label(box;flip(flip(c;y);x));
              nerve\_box\_edge(box;flip(c;y);x);nerve\_box\_edge(box;c;x);nerve\_box\_edge(box;flip(c;x);y))
    fi 


Date html generated: 2016_06_16-PM-07_09_49
Last ObjectModification: 2015_09_23-AM-09_33_36

Theory : cubical!sets


Home Index