fix(library/logic/wf_k): missing file
fix(frontends/lean): tactic + section variables, fixes #332
feat(library/hott) add universe polymorphism to paths, truncation, etc... get stuck at ua to funext proof anyway
feat(library/hott) completed the funext_from_ua proof with a somewhat restricted generality on universe levels
refactor(library/logic/decidable): rename decidable_rel -> decidable_pred, and decidable_rel2 -> decidable_rel
feat(hott/types/sigma): port large part of the sigma library from the hott library

most importantly, prove the characterization of paths in sigma types
feat(hott/path): add notation for higher and dependent transports
fix(library/type): move Prop back
fix(hott/trunc): comment out sorry
refactor(data.prod): move theorems about products from data.quotient.util to data.prod.thms
refactor(data/sigma): move notation from sigma.thms to sigma.decl
feat(hott/types): port more of the sigma library from Coq

prove theorems about interaction of sigma types and n-types, including the fact that sigmas preserve n-types
fix(hott/path): make recursion-like definitions reducible