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.  (Much better than the 1m43s it was on HoTT/coq, though.)  Ideas for speeding it up are welcome.