Define the functor (C -> D)^op -> (C^op -> D^op)

Unfortunately, it's a bit slow.  I'm not sure what to do to speed it up; over 50% of the time is spent figuring out that `idpath` has the right type.

Also, fine tune some other definitions so that we can get more proofs by convertibility.