feat(frontends/lean): local notation override global one

hott/algebra/precategory/basic.hlean

@@ -66,7 +66,7 @@ namespace category
     !is_trunc_eq
 
   end basic_lemmas
-  context squares
+  section squares
     parameters {ob : Type} [C : precategory ob]
     local infixl `⟶`:25 := @precategory.hom ob C
     local infixr `∘`    := @precategory.comp ob C _ _ _

src/frontends/lean/notation_cmd.cpp

@@ -711,7 +711,7 @@ static environment dispatch_notation_cmd(parser & p, bool overload, bool reserve
 }
 
 environment local_notation_cmd(parser & p) {
-    bool overload   = !in_context(p.env());
+    bool overload   = false; // REMARK: local notation override global one
     bool reserve    = false;
     bool persistent = false;
     return dispatch_notation_cmd(p, overload, reserve, persistent);