Prove that the comma category construction is functorial

At least in its category arguments.

This is the first step in showing that two formulations of (co)limits
are equivalent.