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(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