Floris van Doorn
6fca83a2ed
finish the construction of the LES for spectrum maps
2016-09-15 19:19:03 -04:00
Floris van Doorn
683a515178
progress on LES of spectrum maps
2016-09-15 17:57:33 -04:00
Floris van Doorn
6cec5dcdaa
fix definition of homotopy group of spectrum, continue of LES of spectra
2016-09-14 18:46:53 -04:00
Floris van Doorn
9d00ea2f6f
feat(spectrum): start on the LES of homotopy groups for spectra
2016-09-09 16:45:44 -04:00
Floris van Doorn
21c6e8f7e5
small changes after changes in HoTT library
2016-06-26 09:26:13 +01:00
Floris van Doorn
ba7b25d00f
move files to the HoTT library and update after changes in the HoTT library
2016-04-25 19:51:17 -04:00
Floris van Doorn
37fbe56b8c
Finish construction of the LES of homotopy groups without signs
...
The maps on every level are just the functorial action of the homotopy groups (possibly composed by a cast), but there are no compositions with path inversion.
There are also some updates in various files after changes in the HoTT library.
2016-04-07 17:28:19 -04:00
Mike Shulman
a6bf82618f
feat(homotopy/spectrum): sections of parametrized spectra
2016-03-25 09:33:36 -07:00
Mike Shulman
f8f7f69bcd
Finish proof of pfiber_equiv_of_square
2016-03-24 16:30:10 -07:00
Mike Shulman
22e75da53e
chain complexes of spectra
2016-03-23 11:32:25 -07:00
Mike Shulman
559777e45c
index spectra by a general succ_str, +Z, or +N, as appropriate
2016-03-23 11:31:38 -07:00
Mike Shulman
5379c2e253
feat(homotopy/spectrum): fibers of spectra
2016-03-23 11:31:06 -07:00
Mike Shulman
104378f2c3
feat(homotopy/spectrum): use namespaces and better typeclasses
2016-03-21 15:53:25 -07:00
Mike Shulman
2bb5176b97
feat(homotopy/spectrum): basic definitions and cotensors by types
2016-03-20 20:16:36 -07:00
