Nuprl Definition : groupoid-nerve-filler2
groupoid-nerve-filler2(C;I;J;box) ==
<λc.nerve_box_label(box;c)
, λc1,c2,p. poset_functor_extend(C;I;λc.nerve_box_label(box;c);λy,c. nerve_box_edge(box;c;y);c1;c2)
>
Definitions occuring in Statement :
nerve_box_edge: nerve_box_edge(box;c;y),
nerve_box_label: nerve_box_label(box;L),
poset_functor_extend: poset_functor_extend(C;I;L;E;c1;c2),
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),
nerve_box_label: nerve_box_label(box;L),
lambda: λx.A[x],
nerve_box_edge: nerve_box_edge(box;c;y)
FDL editor aliases :
groupoid-nerve-filler2
Latex:
groupoid-nerve-filler2(C;I;J;box) ==
<\mlambda{}c.nerve\_box\_label(box;c)
, \mlambda{}c1,c2,p. poset\_functor\_extend(C;I;\mlambda{}c.nerve\_box\_label(box;c);\mlambda{}y,c. nerve\_box\_edge(box;c;y);c1;c2\000C)
>
Date html generated:
2016_06_16-PM-07_13_41
Last ObjectModification:
2015_09_23-AM-09_33_49
Theory : cubical!sets
Home
Index