Constructive homological algebra in HoTT

Question

I'm curious how much of homological algebra carries over to a constructive setting, like say HoTT (or some other variety of intensional type theory) without AC or excluded middle. There doesn't seem to be a lot of literature on this topic (or at least it's difficult for an outsider like me to find).

The category of abelian groups is fortunately still abelian in HoTT since we have set-quotients, so epis and monos are all normal. So I assume that a good amount of the general theory of homological algebra in abelian categories still applies (such as the snake lemma, 5 lemma, etc.)

But unfortunately it seems like the classical approach to derived functors suffers a setback because we cannot guarantee that we have enough projectives. I'm not sure if the existence of enough injectives is in jeopardy though, since abelian sheaves have enough injectives, but the comments in this related question suggest that indeed the existence of enough injectives is questionable.

I would guess that the derived category and Kan extension definition of derived functors (as given in Emily Riehl's homotopy theory textbook, for example) is better behaved in constructive mathematics, and it looks like Mike Shulman advocated this approach here. But from my naive point of view there's still the issue of showing existence of the Kan extension via functorial deformations of homotopical categories, and I'm also not sure if the usual localization procedure for constructing the derived category is complicated by the lack of AC.

Or perhaps something like $\infty$-topos theory in the style of Lurie, Riehl, Verity etc. (of which I know almost nothing) is the best approach to constructive homological algebra in HoTT, since the logic natively supports higher groupoids. Has any work been done on this since the advent of HoTT?

I'm pretty new to constructive mathematics (still making my way piece-wise through the HoTT volume), and I just have a "working mathematician's" knowledge of homological algebra, but I'm excited about the future of the univalent foundations project.

Answer 1

As regards HoTT, my own current opinion is that the best way to do "homological algebra" therein is by working directly with spectra.

With only a working mathematician's knowledge of homological algebra you may not know what a spectrum is. If you know the Dold-Kan theorem that a nonnegatively-graded chain complex is equivalent to a simplicial abelian group, hence in particular yields a simplicial set, i.e. a "space", then you can think of a spectrum as a space-like thing that corresponds similarly to a chain complex graded on the integers.

The definition of spectrum in HoTT is easy: it's a sequence of pointed types $E:\mathbb{N}\to Type_\ast$ together with equivalences $E_n \simeq \Omega E_{n+1}$. (If you're not familiar with spectra, the idea is that $E_n$ is like the part of a $\mathbb{Z}$-graded chain complex in degrees $\ge -n$, regraded to start from 0, with $\Omega$ corresponding to dropping the 0-chains and shift down by one.) See for instance this blog post and this paper. Similarly, you can define maps of spectra, homotopies between them, homotopy classes of maps between them, smash products of spectra, and so on. You can also define spectrification of a prespectrum, suspension prespectra which spectrify to suspension spectra, and the Eilenberg-MacLane spectrum $H M$ associated to an abelian group $M$.

Now you can define various homological notions by working with Eilenberg-MacLane spectra and then taking homotopy groups. For instance, $\mathrm{Ext}_S^n(M,N) = \pi_n(\mathrm{Hom}_{S}(H M, H N))$ (or maybe $\pi_{-n}$? I forget) and $\mathrm{Tor}^S_n(M,N) = \pi_n(H M \wedge_S H N)$.

These are not (even classically) the usual notions of Ext and Tor (over the integers), but rather "Ext and Tor over the sphere spectrum". This is roughly because the functor from simplicial abelian groups to simplicial sets forgets stuff. (It doesn't forget as much as you might think, though, because the higher homotopy groups are abelian.) To remember that stuff, we can work with modules over the ring spectrum $H\mathbb{Z}$, which classically coincide (as $(\infty,1)$-categories) with $\mathbb{Z}$-graded chain complexes. (We call the general version "over the sphere spectrum" because the sphere spectrum $S$ is the unit object of the monoidal structure on spectra, so that all spectra are $S$-modules in the same way that all abelian groups are $\mathbb{Z}$-modules.) Classically, this sort of Ext and Tor over $H\mathbb{Z}$ do coincide with the traditional versions defined using resolutions and chain complexes, so constructively I believe they should be the "correct" definitions.

Unfortunately, we don't know how to talk about ring spectra or modules over them in ordinary HoTT, because both require infinitely many coherence data. This could be solvable with two-level type theory, but I don't think anyone has pursued such a direction yet.

Answer 2

I posted an answer citing my work with Jarl Flaten on defining Ext groups constructively at https://mathoverflow.net/a/447555/952, where I also mention that you can use this to define other derived functors, all without resolutions.