Adjoint functorial parts

Given a functor `G : D → C`, if we have an initial object of `(Y / G)` for all `Y : C`, we get a left adjoint to `G`.  This construction should be functorial in `G`, as well as in `C` and `D`.  This pull request constructs the action on morphisms, as well as the identity law.

I cannot figure out how to state the composition law (see [here for work in progress](https://github.com/JasonGross/HoTT/compare/adjoint-functorial-parts-more)), and if I restrict functoriality to `G`, then I can state the composition law, but I cannot seem to prove it (see [here for work in progress](https://github.com/JasonGross/HoTT/compare/adjoint-functorial-parts-more-2)).  I suspect this means I am doing something wrong, or that I need some kind of functoriality on the "we have an initial object of `(Y / G)` for all `Y : C`" hypothesis (but apparently it's not needed except to prove the composition law?).  Any suggestions/help would be appreciated, but that should be independent of this pull request.
Last I checked, `Variables C D : PreCategory.` gives `C` and `D` the same universes, while separating the declarations gives them different universes.  I haven't checked if this has been fixed yet.