Floris van Doorn
|
da033c0f4c
|
work on dependent smash and cup product on EM-spaces
also many small fixes
|
2018-09-20 02:08:45 +02:00 |
|
Floris van Doorn
|
3367c20f9d
|
make pointed suspension and spheres the default
There is one proof in realprojective which I couldn't quite fix, so for now I left a sorry
|
2017-07-20 18:03:13 +01:00 |
|
Floris van Doorn
|
91931ca338
|
generalize is_exact
|
2017-03-30 17:05:32 -04:00 |
|
Floris van Doorn
|
b08457c77f
|
move things to the Lean library, and update after changes in the Lean library
|
2016-11-24 00:11:55 -05:00 |
|
Floris van Doorn
|
d8c694e113
|
update after changes in the HoTT library. Mostly some naming and notation changes
|
2016-09-23 17:16:25 -04:00 |
|
Floris van Doorn
|
e7c3144dbd
|
fill in sorry in spherical_fibrations
|
2016-09-15 18:05:58 -04:00 |
|
Ulrik Buchholtz
|
288e0d71b2
|
make everything compile on lean post 6f74f6522...
|
2016-03-24 16:14:44 -04:00 |
|
Ulrik Buchholtz
|
5a23744094
|
update README to reflect recent discussion
|
2016-03-24 13:27:21 -04:00 |
|
Ulrik Buchholtz
|
9ca4a3fbb1
|
start spherical fibrations (NB post #1021 lean)
|
2016-03-24 13:27:21 -04:00 |
|