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) = g o f)
Definitions occuring in Statement :
mk-cat: mk-cat,
compose: f o g,
lambda: λx.A[x],
monoid_hom: MonHom(M1,M2),
grp: Group{i}
Definitions occuring in definition :
mk-cat: mk-cat,
grp: Group{i},
monoid_hom: MonHom(M1,M2),
lambda: λx.A[x],
compose: f o g
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:
2020_05_20-AM-07_56_55
Last ObjectModification:
2017_01_15-PM-11_47_44
Theory : small!categories
Home
Index