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.

alreadyhomological (even homotopical) algebra? E.g. I understand derived functors as basically being "Ack, I defined my functor on the $1$-category of modules, but I really meant to have a functor on the $\infty$-category of chain complexes!" So if you're already defining things directly on the $\infty$-categories, there's nothing more to do. $\endgroup$ – user13113 Nov 22 '17 at 23:536more comments