HoTT/HoTT — pull request #643 by mikeshulman (2014-12-16 09:26:01+00:00)
Title: Make `compose` a notation rather than a definition

This makes life a lot easier; we don't have to be constantly unfolding it, and we can avoid `Local Arguments compose /.` and `simpl rewrite` in lots of places.