Floris van Doorn
|
a99a99f047
|
feat(hit/quotient): prove the flattening lemma
|
2015-11-08 14:04:59 -08:00 |
|
Leonardo de Moura
|
744d1cba3d
|
feat(library,hott,frontends/lean): avoid keywords with hyphen
|
2015-11-08 14:04:54 -08:00 |
|
Floris van Doorn
|
3c4c722afd
|
feat(hott): port more from chapters 4 and 6 of the book
|
2015-09-28 09:09:21 -07:00 |
|
Floris van Doorn
|
fb364f8bc7
|
feat(types): add more equivalences between combinations of type constructors
|
2015-09-11 23:35:21 -07:00 |
|
Floris van Doorn
|
e84b22864f
|
feat(hott): various changes in the HoTT library
|
2015-09-11 23:35:21 -07:00 |
|
Floris van Doorn
|
7e52c49dce
|
feat(hott): many changes is the HoTT library
Prove that 'is_left_adjoint F' is a mere proposition, although this proof is commented out because it takes ~10 seconds
|
2015-09-01 15:17:46 -07:00 |
|
Floris van Doorn
|
124c9d3d8a
|
feat(hott): various cleanup and fixes, rename \~ to ~, expand types.pointed
|
2015-06-25 22:31:40 -04:00 |
|
Floris van Doorn
|
43bcdd7994
|
feat(hott): remove sorry's in circle.hlean, characterize pathovers in degenerate pi's
|
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
|
9893de6194
|
feat(hit/circle): prove partly that the fundamental group of the circle is int
Also add markdown files for nat and int
|
2015-05-07 16:39:04 -07:00 |
|
Floris van Doorn
|
3d7656078d
|
feat(hott/types): prove that 'is_equiv f' is an hprop
|
2015-03-04 00:22:51 -05:00 |
|