Nuprl Definition : group-cat

Group ==  Cat(ob Group{i};arrow(G,H) MonHom(G,H);id(G) = λx.x;comp(G,H,K,f,g) f)



Definitions occuring in Statement :  mk-cat: mk-cat compose: g lambda: λx.A[x] monoid_hom: MonHom(M1,M2) grp: Group{i}
Definitions occuring in definition :  compose: g lambda: λx.A[x] monoid_hom: MonHom(M1,M2) grp: Group{i} mk-cat: mk-cat
FDL editor aliases :  group-cat

Latex:
Group  ==    Cat(ob  =  Group\{i\};arrow(G,H)  =  MonHom(G,H);id(G)  =  \mlambda{}x.x;comp(G,H,K,f,g)  =  g  o  f)



Date html generated: 2017_01_19-PM-02_56_56
Last ObjectModification: 2017_01_15-PM-11_47_44

Theory : small!categories


Home Index