Port some more things from HoTT-categories

including the fact that dualizing is functorial, and the grothendieck construction of functors to set, functors to cat, and pseudofunctors to cat.

This is on top of #269, #274, #275, and #278.