Add `_ $== _ :> _` notation exposing the underlying type of homs
Opened this issue · 0 comments
Alizter commented
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
.