search

HoTT / Coq-HoTT

A Coq library for Homotopy Type Theory
http://homotopytypetheory.org/
Other
1.25k stars 193 forks source link

Pointed shouldn't depend on Homotopy #1144

Open mikeshulman opened 4 years ago

mikeshulman commented 4 years ago

Let's try to keep the dependencies of directories as simple as possible. In particular, I'd like to remove the dependency on Freudenthal from pSusp and simply put that lemma into the Freudenthal file. I think it's better if the directory Pointed is just about basic properties of pointed types, not depending on fancy homotopy theory.

mikeshulman commented 4 years ago

And I guess that means I think Suspension shouldn't be in Homotopy either. Maybe in Colimits?

mikeshulman commented 4 years ago

Hmm, another possibility would be to move pSusp into Homotopy, putting most of it in Suspension (or maybe in a LoopSusp) and the bit using Freudenthal into Freudenthal.

Alizter commented 4 years ago

I agree with a lot of this restructuring especially since we now have the (co)limits folders. Here is a question: Would you consider smash products to be part of the "core" pointed library?

From my work with the smash coherences, it seems to me that the "core" pointed library ought to be something stating properties of the ((oo,1)-)category of pointed types. Smash products are a bit more general in that we have similar constructions in every(?) category with zero object.

With this viewpoint, smash products just become the "uncurrying" construction for pointed maps. And then loop-susp adjunction is just a special case of this.

If we just want the core pointed library to restrict to "limits" in the category of pointed types. I would be OK with that too.

My smash coherences can be found here. Check out the folders PointedCategory and Homotopy/SmashCoherence for the work.

Anyway about organization:

I would merge pSusp and Suspension and move the loop-susp stuff elsewhere. In general the rule should be that pointed versions of a given type get defined in that types file. Which means we should consider moving pforall, psigma etc. into appropriate places.

We could move Loops into the limits folder.

The stuff about pointed truncations needs to be moved the the Truncations folder and included with the index file. It doesn't do any harm to have pointed truncations with the regular ones but I can't ever see someone wanting pointed truncation but not truncations.

mikeshulman commented 4 years ago

I think right now my inclination is to put the basic definitions regarding suspension and smash products into Colimits, and the categorical properties as you mention like loop-susp and smash coherence into Pointed. But I would keep pforall and psigma in Pointed; since Types comes "before" Pointed I wouldn't want to clutter it up with them. I would probably keep Loops and pTrunc in Pointed also; for the latter, the reason is to keep the dependencies between directories clean, so that Truncations can come "before" Pointed.

Alizter commented 4 years ago

@mikeshulman When you say types come "before" pointed. This isn't strictly true. We define pointed types in Basics. This means that Pointed forall etc. should not depend on Pointed. The pointed truncations would also not depend on pointed.

I should note that the smash coherence stuff is quite bulky. It takes a lot longer to build than the rest of pointed. It might be worth keeping it separated.

mikeshulman commented 4 years ago

I mean the directory Types comes before the directory Pointed. And I think as much as possible, definitions relating to pointed types should go in the directory Pointed.