1-category of successor structures

[Alizter]

One of the nice things about pType is the potential to define the wildcat structure "all the way up". We don't actually do this, but because pHomotopy is defined as pForall we get all the higher morphisms "for free".

I was interested in working out what exactly makes a "forall" in a category tick. From what I could find, its not really a commonly studied phenomenon. Typically in category theory, such "forall" looking sets of dependent functions carry an extra structure of being internal. This is a strong requirement that makes it impossible to replicate in various categories (keep Spectra in mind). However the lesson to learn from pType is that we almost never care about ppForall but only pForall which has nothing to do with the internal (dependent) hom.

Therefore I was interested in seeing if we can push this idea in other categories, notably the category of spectra. That would allow us to have a very nice category to work with.

I believe this is possible but it will require a bit more work on understanding the exact definitions of family of spectra over a spectrum and how a hypothetical "sForall" might be constructed. The route of paramaterized spectra appears to somewhat be a red-herring and doesn't really gain us much.

Anyway, to give an initial proof-of-concept of the wider application of the pType-pforall technique, I decided to choose a structure which is not entirely trivial but still simple to work with. The toy example I chose in the end is the category of successor strucutres.

I don't believe that this work will lead to a deeper understanding of the theory of successor structures, however it does demonstrate that the forall-technique can be generalised.

The basic recipe is as follows:

• Start with a category C.
• Define a "displayed" version of the objects of C. Notably this should be a family over C.
• Define the homotopy family.
• Define foralls and higher homotopies between them using the family.

Interesting things to note:

• My pelim tactic from before has an analogue here.
• The structure of SuccStr has a non-trivial endomap which can be "displayed" appropriately.
• We get a full 1-cat structure and 2-cat with some more work.

I would like to eventually try this technique on spectra once we work out what the correct way to have displayed spectra is. These are not parameterized spectra as the base space must also be a spectrum. It should probably consist of pFam for each pType in spextra and some how a displayed pointed map which I have yet to formulate.

I think that this work so far is harmless so I would advocate including it. It might be worth considering a way to axiomatize what a "forall" is in a category, but I think even just defining how to "display" things will be quite non-trivial.

cc @jdchristensen and @mikeshulman (who might be interested in the displayed part).

[jdchristensen]

I think it's fine to include this as another example of creating a wild category. I made some minor suggestions, and maybe it's worth waiting a day to see if @mikeshulman has any comments?

[mikeshulman]

I don't have time to look at this in detail, but it does look interesting! I'll be interested to see how far it can be generalized.

Regarding the question of how to define displayed spectra and other things, I wonder whether https://arxiv.org/abs/2311.18781 could be relevant? In that paper we formulated a type theory with a generic "display" operation that acts on (among other things) any type defined in the empty context to compute a notion of "displayed elements" of that type.

[Alizter]

@jdchristensen Thanks for taking a look. I've addressed all your comments.

[Alizter]

Regarding the question of how to define displayed spectra and other things, I wonder whether arxiv.org/abs/2311.18781 could be relevant? In that paper we formulated a type theory with a generic "display" operation that acts on (among other things) any type defined in the empty context to compute a notion of "displayed elements" of that type.

Yes! I definitely think this is relevant. I hope to sit down at some point and see if I can turn the crank on displayifying some things using the work you and Astra did. It definitely did inspire me to think more in a displayed way.

[jdchristensen]

LGTM! I'll let you merge when you are ready. BTW, it's better to push an additional commit rather than squashing your changes into one commit, as otherwise the reviewer has no way to see how you addressed the comments. In this case, it was all minor stuff, so it doesn't matter too much, but I'm just mentioning it for the future.

[Alizter]

@jdchristensen sure that makes sense. By the way, you can see the diffenece by clicking on "force push" in the commit history.

[jdchristensen]

By the way, you can see the diffenece by clicking on "force push" in the commit history.

@Alizter Oh, thanks for pointing that out! Then what I said isn't as important, although I do still think it helps a bit in other ways.