# coend formulation of homotopy colimit

I have recently been trying to learn about homotopy colimits. In so doing, I have gone through way too many papers, and now I can't find the one which introduced homotopy colimits via a coend computation.

Note that I am interested in the "local" formulation (to use the terminology of Shulman's paper), as I really want to perform very concrete computations. Furthermore, I am most interested in purely categorical formulations, as the background computations all happen in type theory, not topological spaces.

Part of the motivation is to understand the paper Ring completion of rig categories, and unravel the construction given there in simpler terms.

• I heartily recommend math.harvard.edu/~eriehl/cathtpy.pdf Jun 3, 2014 at 2:11
• I'm not sure I understand what you mean by "in type theory". If your type theory is intensional, then you already have homotopy limits, or at least, homotopy products and homotopy equualisers. If not, where is the connection with homotopy theory? Jun 3, 2014 at 2:42
• @ZhenLin: I understand type theory. I understand classical (aka topological without categories) homotopy theory. I am an absolute beginner at 'merging' them, so I do not actually understand your comment. Plus 'have' is really not the same as 'can compute with'! Jun 3, 2014 at 2:54
• In intensional type theory, everything is automatically homotopy-invariant. So for example, the homotopy equaliser of $f, g : X \to Y$ is just $\sum_{x : X} f (x) =_X g (x)$. Jun 3, 2014 at 3:00
• Have you looked at Dugger's primer on homotopy colimits? Jun 4, 2014 at 5:28

## 3 Answers

The coend technique for computing homotopy colimits is reviewed on the nLab at

This follows the beautiful article

which I'd suspect might be the one you had seen and then lost sight of.

• What is on the nLab unfortunately is the "global" story, which is really hard to use for computations. Same with requiring model categories. Jun 3, 2014 at 21:38
• @JacquesCarette The nlab also includes the local formulas, such as at the place Urs linked to. Gambino also. The only extra thing added is a cofibrant replacement, which is necessary in general to get the right answer, but in practice can often be dispensed with. (In homotopy type theory, there is no cofibrant replacement, but then neither are these formulas likely to be much help, since they construct homotopy colimits out of ordinary colimits, which are not present either.) Jun 4, 2014 at 3:02
• Regarding cofibrant replacement, I suppose the point to highlight is that for computing the homotopy colimit of a single diagram, only that single diagram needs to be cofibrantly replaced. If however one wants the homotopy colimit as a functor ("globally") then one needs to choose a functorial cofibrant replacement of all diagrams at once. But, as Mike said, that does not affect anything in the discussion of the coend description of homotopy colimits. Jun 4, 2014 at 9:37
• Regarding the need for model categories: The discussion of homotopy colimits via coends depends exclusively on the cofibration structure. I'd think for any sensible structure of a category of cofibrations for which the coend satisfies the axioms of a left Quillen bifunctor the same formulas all still apply. Jun 4, 2014 at 9:39

Have a look at chapter 6, in particular 6.8, of the HoTT book for the treatment of homotopy colimits.

Regarding coends, perhaps, you were looking for this paper: A Higher-Order Calculus for Categories.

The excellent Homotopy (limits and) colimits by Emily Riehl is probably contained in her Categorial homotopy theory that John Wiltshire-Gordon mentions in his comment, but it is more focused.