So Joel suggests that a group is just a special type of groupoid, and a groupoid is clearly just a special type of category. This means that every group is the subgroup of the automorphism group of something. Which seems to make sense to me. I don’t think that I’ve ever met a group that wasn’t the automorphisms of something. In Galois theory, the groups are field automorphisms (that fix some subfield). Matrix groups are automorphisms of vector spaces.

But I’d like to say that a ring is some universe U with operations and such that (U, ) is an abelian group, and (U,) is a monoid, and distributes over . But if (U, ) is an abeliean group, then the universe should consist of automorphisms of something. But I’ve met lots of rings whose objects that don’t seem like functions at all (like the integers). I’d like to reconcile these two views.

Perhaps the integers are really functions. In some forms of type theory, one identifies the natural numbers with the type ΠA:Type.(AA)⇒AA. So the number n is identified with the function λA:Typef:AA.fn. A similar identification can be made with the integers and maps from bijections on A to bijections on A.



Russell O’Connor: contact me