HoTT/HoTT — pull request #627 by JasonGross (2014-11-28 23:25:06+00:00)
Title: 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.