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