Exponential laws

Add the construction of the functors which witness the exponential laws, and product laws.  Also add associated machinery such as the functorialness of functor categories, the subprecategory of precategories satisfying any (given) mere proposition which makes Functors an hSet.

Next up is (probably) the yoneda lemma, the structure identity principle, univalence of Set.