Polygraphs in HoTT

[spitters]

By @MaximeLucasSky https://hal.archives-ouvertes.fr/hal-02385110 https://github.com/MaximeLucasSky/polygraphs

[Alizter]

Unless I am mistaken, aren't these just CW-complexes?

[MaximeLucasSky]

Yes, they are very similar to CW complexes. Alternatively, they can be seen as some sort of presentations of HITs. The main issue is that when building the Space associated by a CW complex you want to use 1-pushouts, which you can't do in the context of HoTT.

Strangely enough many things still work when replacing 1-pushouts by homotopy pushouts, but it is not really clear (at least to me) what those "homotopy CW-complexes" really are...

[Alizter]

I don't think there is any issue with "homotopy CW-complexes". In fact Favonia and Buchholtz also define CW-complexes in HoTT here:

https://favonia.org/files/cohomology-lics2018.pdf

They manage to compute the cellular cohomology of such a complex. The only practical issue with the "homotopy" version of CW complexes is that CW complexes we construct classically use easier to define attaching maps. For example, it is a lot clearer how to attach cells together when constructing the Grassmannians, Hatcher has a very nice description of it in his K-theory notes. But when doing this with "homotopy" CW-complexes, its not entirely clear (at lest to me) which map we have to use, this essentially amounts to choosing an element of Pi n (X) where X is the complex constructed so far, and we want to find a map S^n -> X.

I imagine we could compute the fundamental group of your polygraphs using van Kampen. I am not sure if we are able to say much about the higher homotopy groups however.

One thing I would be interested in is comparing the CW complexes we do know with your polygraph construction. Take the real projective spaces which Rijke and Buchholtz constructed (essentially as a CW complex).

https://arxiv.org/abs/1704.05770

Are you able to derive the induction principle for these?

About the HITs part: Can you construct some more complicated recursive HITs? I think you would be able to construct truncations using your construction and Rijke's join construction which essentially amounts to having coequalizers.

I am not sure you would be able to construct something really recursive like the James construction however.

I am only speculating however, perhaps @mikeshulman has something more informative to say than I do.

[mikeshulman]

When building a CW complex in the 1-category of topological spaces, one uses 1-pushouts since that's all that are available therein. But those 1-pushouts are homotopy pushouts for the model structure on topological spaces. And when working in an oo-category, one would build CW complexes directly using homotopy pushouts. So that's not really anything new or different.

The main difference I see between what you're doing and the classical notion of CW complex is that classically one would have only a set of n-cells for all n, rather than a whole type. So your CW complexes are sort of "space-enriched CW complexes".

BTW, I don't think "polygraph" is a very good name for these; it doesn't convey that they're really just generalized CW complexes, and conflicts with other usages of that word.

[MaximeLucasSky]

Thank you very much for your insight. This all started as a self-imposed exercise to get used to Coq and HoTT and I haven't really taken the time to take a step back and look at what I had done.

The general picture I had in mind in the 1-categorical case is that, given a nice-enough category C and a family of arrows f_n in that category there should an associated notion of CW-complex / polygraph. In the case where C = Top and f_n are the inclusion of the n-sphere in the n-ball this is the usual CW-complexes. If C is a category of algebras over a monad T on globular sets and the f_n are the image under T of the inclusion of the n-sphere in the n-ball then one gets T-polygraphs in the sense of Batanin/Garner. This should also encompass the computads on inverse diagrams of the nlab (which I believe you wrote @mikeshulman ?). What I was at first trying to formalize is the construction of the adjunction between C and those (f_n)-CW complexes/polygraphs.

Now of course this is not what I ended up implementing, which as you say looks a lot more like generalized CW-complexes. @Alizter I was not able to state a general nice induction principle for those although in principle it should follow from the one for the pushout. I'm not really familiar with neither Rijke and Buchholtz real projective spaces nor the James construction but I'll try to see what I can say on these examples.

[mikeshulman]

Thanks for the context! I still think that even in the general case, "cell complex" is a more general and widely-understood name, applicable to arbitrary categories with arbitrary collections of "cell" morphisms, than "polygraph'.