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	9f13527c25	chore(hott): update default files and some markdown files	2016-07-09 10:20:21 -07:00
Floris van Doorn	43cf2ad23d	style(hott): replace all other occurrences of hprop/hset ... They are replaced by either Prop/Set or prop/set	2016-02-22 11:15:38 -08:00
Leonardo de Moura	4a6ff8058d	fix(hott): import commands (some files have been moved to different directories)	2015-09-25 09:39:45 -07:00
Ulrik Buchholtz	384a366e0f	refactor(hott): move homotopy hits to new homotopy folder	2015-09-24 22:52:33 -04:00