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.
That's a good point, @peterlefanulumsdaine .  What would you think about eliminating the notation `compose` entirely and just having `Notation "g 'o' f" := (fun x => g (f x))`?