Add _ $== _ :> _ notation exposing the underlying type of homs

[Alizter]

In many situations we will have a goal like f $== g however it can be difficult to remember what the base category was supposed to be in this situation. We should add a _ $== _ :> _ notation perhaps that breaks nicely in long_path_scope so that such goals become easier to udnerstand.

f $== g :> A means that f, g : A.