feat(library/algebra): modify categories to use definitions, prove basic theorems about discrete categories
fix(hott/trunc): add explicit coercion so that the notation works if nat is not opened
style(hott/path): indent within namespace, add variables
style(hott/types): some style fixes in prod and sigma
feat(hott/types): start characterization of pi-types and W-types
fix(tests/lean/struct_class): adjust test result to reflect recent changes
refactor(library/data/vector): cleanup
fix(tests/lean/whnf): make sure the test does not produce 'sorry'
fix(library/tactic/inversion_tactic): warning on clang++