HoTT/HoTT — pull request #287 by JasonGross (2013-12-15 01:15:50+00:00)
Title: 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.