Combine a few pull requests needed for my category theory library

This combines the pull requests required for https://github.com/JasonGross/HoTT-categories to compile; in order for my git submodule setup to know about this commit, I think I need to have HoTT/HoTT know about these commits, and making this pull request is the only way I could think of to do so.

Feel free to merge this request, or leave it open until the underlying requests are merged, or close it (I think my setup should still work fine even if this is closed).