Stable homotopy type theory?

Question

This is a combined question, strictly speaking I am asking three questions concerning, respectively, homotopy type theory, stable homotopy theory and Yetter-Drinfeld modules. But I believe in the present context they can be viewed as a single question.

After a lecture on HoTT by Voevodsky (at TACL 2013 in Nashville) I asked him whether Homotopy Type Theory can be useful for stable homotopy theory. Without much hesitation he replied that HoTT is not really well suited to describe stable phenomena. We never talked after that, and now we will never talk at all, so I still do not know where the main difficulty lies.

Discussing this with several other people (sorry, don't exactly remember with whom) I gradually developed impression that the main difficulty relates to the fact that there seems to be no known good formalism combining constructive type theory and substructural logics, that would lead to some sort of linear type theory. Among possible models one should have triangulated monoidal categories, like stable homotopy category, and it seems not to be known what is the analog of dependent types there.

The first question then is whether what I said above makes any sense, and whether there is any work in this direction.

A situation where one has something like "linear dependent types" is in the context of Yetter-Drinfeld modules over Hopf algebras. Heuristically, the starting point is the fact that in any category $\mathscr C$ with (Cartesian) products every object $X$ has a unique comonoid structure, and the category of comodules over this comonoid is equivalent to the slice $\mathscr C/X$. One could then try to imitate this in (non-Cartesian) monoidal categories, considering comodules over comonoids as variable families over that comonoid. When this comonoid is equipped with a Hopf monoid structure, one can get a "linear" analog of Freyd-Yetter's crossed G-sets.

The second question is then, whether anybody studied features of categories of Yetter-Drinfeld modules over varying Hopf algebras which would resemble either what happens in HoTT or in stable homotopy category.

And the third question comes from the fact that while there are plenty of examples of monoids in stable homotopy categories (ring spectra) I cannot remember any considerations of comonoids or Hopf objects there. Does anybody know some works on this? Or even more simple question (actually fourth, sorry): in unstable homotopy theory one knows that for a, say, topological group $G$ there are certain homotopy categories of $G$-spaces and of spaces over $BG$ which are equivalent. Is there an analog of this fact in stable homotopy theory?

Or maybe Voevodsky had in mind that there seems to be no analog of univalence in the stable context? (Well that was fifth, I certainly must stop here.)

I found only one related question, Are there connections between Homotopy type theory and Grothendieck's theory of motives?, about possible connections between HoTT and motivic homotopy theory. I discovered my pessimistic comment there, remembering that answer by Voevodsky and arguing that motivic homotopy is in a sense even "more linear" than stable homotopy, so it might be even more difficult to relate these two. Anyway.

Answer 1

A suitable variety of type theory for stable homotopy theory has subsequently been proposed:

• Mitchell Riley, A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis (2022) [doi:10.14418/wes01.3.139, ir:3269, pdf]

• Mitchell Riley, Linear Homotopy Type Theory, talk at: HoTTEST Event for Junior Researchers 2022 (Jan 2022) [slides: pdf, video: YT]

  Abstract. Some ∞-toposes support constructions that are inherently 'linear', such as the external smash product of parameterised spectra. These cannot be added axiomatically to ordinary HoTT, because there is no way to enforce this linearity: there are no restrictions on variable uses. This talk describes an extension of HoTT with linear tensor and hom type formers, as a kind of 'binary modality' and its right adjoint. Trying to stay compatible with existing results in HoTT naturally leads us to a novel kind of bunched dependent type theory. Our type theory is intended to be as human-usable as possible, with an eye towards synthetic stable homotopy theory.

For its use as a quantum programming language, see

• Hisham Sati, Urs Schreiber, The Quantum Monadology, [arXiv:2310.15735]

Answer 2

With respect to the first question, expanding on my comment which pointed out the nLab page dependent linear type theory and the article by Urs Schreiber, 'Quantization via Linear homotopy types', I'd like to pass on some additional relevant commentary by Urs.

There is a way to express linearity for homotopy types, see stable homotopy type. As Simon pointed out in his comment, the category of parametrized spectra is an ∞-topos, indeed a tangent ∞-topos. One can then look to add an axiom to HoTT that makes it the internal language for tangent ∞-toposes. That axiom should be:

1. there is a pointed type $X_\ast$

2. the morphism $\Sigma \Omega X_\star \to X_\star$ is an equivalence

So far this makes the ambient category "linear" in the terminology of Schwede's old article on parameterized spectra. One could now continue to add the axioms

3. the morphism $\Sigma \Omega(X_\star^{S_\star}) \to X_\star^{S_\star}$ is an equivalence, for finite pointed powers.

If one could add the infinite set of these axioms, that would be Goodwillie's localization for the tangent $\infty$-topos.

There's work in preparation by Mathieu Anel, Eric Finster, and André Joyal along these lines.

Answer 3

There are multiple possible routes to study stable homotopy theory in a type-theoretic system, some of which are work in progress by various people, but none of which are fully developed.

As has been pointed out, one can make use of the fact that the category of parametrized spectra is an $(\infty,1)$-topos and therefore (conjecturally) admits an interpretation of HoTT, then use this model to motivate new structures and axioms for HoTT to produce a "homotopy type theory of parametrized spectra" analogous to what we have done for directed and cohesive homotopy type theories. There is work in progress on deciding what exactly these new features should be.

On the other hand, one can try to attack the category of spectra directly. As has been pointed out, since it has finite limits it conjecturally admits a model of dependent type theory but without $\Pi$-types and without a universe. This lack makes it almost impossible to do anything resembling current homotopy type theory purely inside spectra. What seems more useful is to have an ambient unstable homotopy type theory which can be related to the stable one in some way. So that, for instance, we have an unstable homotopy type of maps between two spectra, and can talk about homotopies and apply the theory of h-levels and equivalences (using unstable $\Pi$-types) in that way. There could also be an unstable universe of stable types that is "univalent" in an appropriate sense.

When one plays with this a bit, it starts to seem very natural, even necessary, to allow stable homotopy types to depend on unstable ones, so that we are heading back in the direction of parametrized spectra. But now instead of considering each parametrized spectrum as a basic object, we are stratifying them over their base spaces, with two context zones for unstable and stable types. In the non-homotopy context, it's not hard to write down such a type theory that has models in "indexed monoidal categories", and that categorical structure can be generalized to "indexed monoidal $(\infty,1)$-categories", which are mostly what the original nLab page "dependent linear type theory" is about (I've now moved that content to Indexed monoidal (∞,1)-category). But as far as I know, no one has yet proposed a good way to write down a homotopy type theory that has semantics in such indexed monoidal $(\infty,1)$-categories.

There is work by type theorists on "dependent linear logic". Some of it, such as "linear LF", I believe involves linear types dependent on nonlinear ones. But I'm not aware of any version of such a theory yet that would, for instance, allow linear types to have non-linear identity types, which seems to me to be what we would want to be able to do stable homotopy theory this way.