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, pseudofunctors to cat, the category of sections, and the dependent product.

This is on top of #269, #274, #275, and #278.