5 commits

Author	SHA1	Message	Date
Floris van Doorn	ddef24223b	make pointed suspensions, wedges and spheres the default (in contrast to the unpointed ones), remove sphere_index ... All HITs which automatically have a point are pointed without a 'p' in front. HITs which do not automatically have a point do still have a p (e.g. pushout/ppushout). There were a lot of annoyances with spheres being indexed by N_{-1} with almost no extra generality. We now index the spheres by nat, making sphere 0 = pbool.	2017-07-20 15:02:09 +01:00
Floris van Doorn	9342fe2716	feat(hott) move many lemmas to library, and cleanup various parts	2016-12-02 16:55:23 -08:00
Floris van Doorn	341a53b880	feat(pointed): make the naming in the pointed library more consistent. ... Also start on a naming conventions file	2016-09-22 16:00:27 -04:00
Floris van Doorn	52dd6cf90b	feat(hott): Port files from other repositories to the HoTT library. ... This commit adds truncated 2-quotients, groupoid quotients, Eilenberg MacLane spaces, chain complexes, the long exact sequence of homotopy groups, the Freudenthal Suspension Theorem, Whitehead's principle, and the computation of homotopy groups of almost all spheres which are known in HoTT.	2016-05-06 14:27:27 -07:00
Ulrik Buchholtz	89296ec52a	feat(hott): the complex hopf fibration S3 to S2	2016-03-23 09:22:55 -07:00