6 commits

Author	SHA1	Message	Date
Floris van Doorn	4a29f4bdd4	feat(types): incorporate pathovers in the files of the types folder ... Conflicts: hott/cubical/pathover.hlean	2015-05-26 21:37:01 -07:00
Jeremy Avigad	33214f0895	refactor(hott/*): remove 'Module:' lines	2015-05-23 20:52:58 +10:00
Floris van Doorn	de6294a4ce	feat(hott.core): add more files to core.hlean	2015-05-18 15:59:55 -07:00
Floris van Doorn	43fb334914	feat(circle): prove loop != base	2015-05-07 16:39:03 -07:00
Floris van Doorn	297d50378d	feat(hott): add definitions using truncations and theorems about them ... define embedding, (split) surjection, retraction, existential quantifier, 'or' connective also add a whole bunch of theorems about these definitions still has two sorry's which can be solved after #564 is closed	2015-04-29 10:04:07 -07:00
Floris van Doorn	60ae9f627c	feat(hott): add core.hlean and types/default.hlean	2015-04-10 06:35:24 -07:00