Fix #44: the full Grothendieck construction for (contravariant) pseudofunctors

[sstucki]

Now (hopefully) with the correct notion of equality on arrows.

Differences w.r.t. the old version:

• The fixed version turned out a lot more complicated.
• This version uses pseudofunctors (rather than plain functors). The associativity and unit laws require coherence conditions which plain functors don't provide. I believe it should be possible to instead give a construction using plain functors into StrictCats (instead of Cats), but the version using pseudofunctors is more general.
• Interestingly, because of the way the coherence conditions are defined in Pseudofuctor, it was easier to prove the contravariant version of the construction.

[JacquesCarette]

Superb! Thanks a lot.