Prove functoriality of comma category construction

At least in its category arguments.

This is the first step in showing that two formulations of (co)limits
are equivalent.

Unfortunately, it's somewhat slow, at 16s.  Ideas for speeding it up are welcome.