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:
2016_05_18-AM-11_56_03
Last ObjectModification:
2015_09_23-AM-09_29_21
Theory : small!categories
Home
Index