Commit graph

3 commits

Author SHA1 Message Date
Jakob von Raumer
4d6c516c01 feat(hott): add lemma: equivalent fin sets come from equal numbers, sums with fin sets are cancellable 2016-02-09 09:58:52 -08:00
Jakob von Raumer
0ad8131985 feat(hott): start cancellation proof for sums 2016-02-09 09:58:24 -08:00
Jakob von Raumer
1042f6c29d feat(hott): port finite ordinal sets from the std library, with all things related to nat.mod and to fintype still missing.
create a logic.hlean file for further extension of the logic theory in the prelude. add distributivity lemmas for products and sums.
2016-02-09 09:58:10 -08:00