feat(lean-input.el): add some new notation
feat(library): add definition of subsingleton and some other minor changes
feat(category): split category.lean in different files; add more constructions and theorems about isos