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.
Does `IsEquiv (fun x => ?f (?g x))` work?  I suspect the problem is that the goal is actually the beta-reduced form of `(f o g) o h`, which is hard, if not impossible, to write a single pattern for.