chore(library/hott) move function extensionality into new axioms folder, adjust file(s) using it
feat(library/hott) add univalence axiom
chore(library/hott) adapted univalence axiom to suit notation in book and def in Coq.
Added substitution lemma for equivalence calculations
chore(library/hott) add note referring to missing substitution lemma
chore(library/hott) cleanup
fix(library/hott) make universe index in ua.lean variable
fix(emacs/lean-syntax): syntax highlight, issue #306

1- FIXED     structure foo := (bar : Type) -- the name of structures is not highlighted
2- NOT FIXED check foo-- this comment is not highlighted
3- FIXED     check Type.{5} -- Type is not highlighted
4- FIXED     definition bar{thisishighlighted : Type} := foo
5- FIXED     definition bar2 {thetypeofthisvariableisnothighlighted :Type} := foo

Have no idea what is going on with 2. I'm not sure if this is our bug,
or Emacs code we depend on.
fix(kernel/error_msgs): ignore binder information when comparing type mismatches, fixes #304
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
feat(frontends/lean): max precedence used by Lean is not max_uint anymore

The motivation is to allow users to define notation with higher
precedence than function application.
refactor(library/data/num): break into pieces to reduce dependencies
refactor(library/data/bool): break into pieces to reduce dependencies
refactor(data/num/string): break into pieces to reduce dependencies
refactor(library/logic/wf): add well_founded class, and cleanup file
fix(library/hott/fibrant): set arguments for type class resolution
feat(library/algebra/group): add multiplicative and additive structures
feat(library/data/nat/wf): add nat.lt is well founded theorem
feat(emacs/lean-mode): bind "C-c C-k" to quail-show-key

 - Use this to see how to type a unicode character
fix(emacs/lean-syntax): change comment symbols to be considered as punctuations

Please read the documentation of "modify-syntax-entry":

"The first character of NEWENTRY should be one of the following:
  _           symbol constituent
  .           punctuation
"

Close: #306