feat(frontends/lean): display type of binders, closes #238
feat(quantifiers.lean): change exists_unique to a constructively stronger formulation

the previous formulation was constructively probably to weak to be useful
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
feat(binary.lean): add helper theorem for associative functions
feat(algebra/category/): minor additions, start on adjunction
fix(library/algebra/category): minor fixes to reflect recent changes, and fix tests
chore(library/algebra/category): add workaround
chore(*): minimize the use of parameters
fix(frontends/lean/elaborator): better specific universe detection
feat(library/universe): improve support for universe level constraints in the unifier
feat(frontends/lean): add 'universes' command
feat(kernel/inductive): track when K-like reduction can be used
feat(kernel/inductive): K-like reduction in the kernel

Given (H_1 : a = a), we have that
      eq.rec H_2 H_1
reduces to H_2

This is not exclusive to equality.
It applies to any inductive datatype in Prop, containing only one
constructor with zero "arguments" (we say they are nullary).

BTW, the restriction to only one constructor is not needed, but it is
does not buy much to support multiple nullary constructors since Prop is
proof irrelevant.
refactor(library/logic): use new K-like reduction to simplify some proofs
refactor(frontends/lean/util): add auxiliary function
fix(frontends/lean/elaborator): incorrect type information being reports in lean-mode, fixes #241
feat(shell): add options --cpp and --discard
feat(frontends/lean): allow variables anywhere