Nuprl Definition : groupoid-square1
groupoid-square1(G;x00;x10;x01;x11;a;b;c) ==
cat-comp(cat(G)) x01 x10 x11 (cat-comp(cat(G)) x01 x00 x10 groupoid-inv(G;x00;x01;c) a) b
Definitions occuring in Statement :
groupoid-inv: groupoid-inv(G;x;y;x_y),
groupoid-cat: cat(G),
cat-comp: cat-comp(C),
apply: f a
Definitions occuring in definition :
apply: f a,
cat-comp: cat-comp(C),
groupoid-cat: cat(G),
groupoid-inv: groupoid-inv(G;x;y;x_y)
FDL editor aliases :
groupoid-square1
Latex:
groupoid-square1(G;x00;x10;x01;x11;a;b;c) ==
cat-comp(cat(G)) x01 x10 x11 (cat-comp(cat(G)) x01 x00 x10 groupoid-inv(G;x00;x01;c) a) b
Date html generated:
2020_05_20-AM-07_56_14
Last ObjectModification:
2015_09_23-AM-09_29_21
Theory : small!categories
Home
Index