HoTT/HoTT — pull request #229 by JasonGross (2013-10-22 05:27:10+00:00)
Title: 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.