Port products of functors and natural transformations

This is required for the hom functor.  I had some fancy notations that let you write things like `Hom C ⟨ F ⟨ 1 ⟩ , 1 ⟩`, but they were black magic, so I stripped them before porting.  I'll probably put them back in to `Functor/Prod/Notations` or something, but only in `contrib`.  This should be compatible with all other pull requests currently open or about to be opened.