# 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 – John Wiltshire-Gordon Jun 3 '14 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? – Zhen Lin Jun 3 '14 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'! – Jacques Carette Jun 3 '14 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)$. – Zhen Lin Jun 3 '14 at 3:00
• Have you looked at Dugger's primer on homotopy colimits? – Tyler Lawson Jun 4 '14 at 5:28

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. – Jacques Carette Jun 3 '14 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.) – Mike Shulman Jun 4 '14 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. – Urs Schreiber Jun 4 '14 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. – Urs Schreiber Jun 4 '14 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.