Comma

Port comma categories, universal morphisms, Kan extensions, and (co)limits.

I'm not terribly happy with the ASCII infix notation `T |v| S`, but I couldn't
figure out how to make `T , S` work, and I don't think I'm supposed to use
unicode.

I haven't figured out how to get the intro and elim rules for (co)limits to behave (I
don't want extra compositions with identity morphisms).  I also haven't
ported the morphisms between limits of the same functor, which was in
the catdb file.  (That should be straightforward, though, if we want
it.)  I might tackle those soon.

The next big port after this one will probably be adjoints, including the proof that (co)limits assemble into a functor adjoint to the constant diagram functor (and similarly for Kan extensions).