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
feat(frontends/lean): namespaces also define scope for variables
refactor(library): remove some unnecessary sections
fix(doc/lean/test_single): "race condition" when running tests in parallel
fix(frontends/lean/elaborator): bug when reporting error position
feat(frontends/lean/parser): reject ambiguous parameter declaration, closes #242
we can do without parameters