fix(hott): fix binding power of 2 notations

hott/algebra/precategory/basic.hlean

@@ -132,7 +132,8 @@ namespace category
   attribute Precategory.struct [instance] [priority 10000] [coercion]
   -- definition precategory.carrier [coercion] [reducible] := Precategory.carrier
   -- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct
-  notation g `∘⁅` C `⁆` f := @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
+  notation g `∘⁅`:60 C:0 `⁆`:0 f:60 :=
+  @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
   -- TODO: make this left associative
   -- TODO: change this notation?
 

hott/init/path.hlean

@@ -40,8 +40,8 @@ namespace eq
   definition inverse (p : x = y) : y = x :=
   eq.rec (refl x) p
 
-  notation p₁ ⬝ p₂ := concat p₁ p₂
-  notation p ⁻¹ := inverse p
+  infix   ⬝  := concat
+  postfix ⁻¹ := inverse
   --a second notation for the inverse, which is not overloaded
   postfix [parsing-only] `⁻¹ᵖ`:std.prec.max_plus := inverse