refactor(frontends/lean): adjust function names to reflect how parameters/variables behave
feat(library/algebra/category): use variables instead of parameters
refactor(library/algebra/category): remove unnecessary sections
refactor(frontends/lean): do not expose unnecessary functions
feat(frontends/lean/notation_cmd): remove the cleanup notation hack
feat(frontends/lean): allow parameters only in contexts
refactor(library/scoped_ext): sections are just "nameless" namespaces
feat(frontends/lean): do not allow coercion definition in sections
checkpoint