sTeX for dynamic, research-level mathematics

[sorsted]

I am a researcher in mathematics. As someone who has also worked on semantic mathematics markup (in the form of my package SemanTeX), sTeX caught my attention. Congratulations on your recent, gigantic update, by the way. Looking through the new, much more detailed manual, I am curious about how the package is meant to be used for research-level mathematics, beyond simple calculus expressions.

The manual explains in detail how to write calculus equations and how to automate the insertion of parentheses in expressions like (a+b)\cdot c. It also tells me how to program functions taking a fixed number of arguments and specifying their domain and codomain. This is all very good, but still close to the level of mathematics regarded as applied logic.

But research-level mathematics is a much more dynamic, chaotic mess. Variables can suddenly act as maps, maps can act as variables, notations can change on the go, and the value of a function may be another function.

Take the case of a functor, for instance. If F is a functor, I can apply it to an object x and get an object F(x), or I can apply it to a map f and get a map F(f). So depending on what I apply F to, the output will be an object with a varying number of arguments.

Or imagine that I consider the cohomology H^{\bullet}(X, \mathcal{F}) of X with values in a sheaf \mathcal{F}, but that when \mathcal{F} is the constant sheaf on the complex numbers, I just write H^{\bullet}(X) (this is quite common practice).

Or imagine that I take a scheme X and then consider its functor of points X(R) = \Hom(\Spec R, X).

Or what if I want to define the pushforward sheaf as f_{*}(\mathcal{F})(U) = \mathcal{F}(f^{-1}(U))?

How am I supposed to typeset such situations in sTeX?

[kohlhase]

Hi @sorsted good to hear from you, and we are aware of SemanTeX. I agree that research mathematics is quite a challenge for any semantic markup system; indeed the more semantic it is the more.

We have been concentrating on education-level maths a couple of reasons that include your's

1. a prerequisite for semantic annotation is that we understand (and can thus fix) the meaning of what we are writing down. As you very nicely point out, this is often not (yet) the case in research mathematics, and pen and paper is a more flexible medium when meaning changes are part of the creative process.
2. The second reason is that research mathematics has a longer tail (of needed prerequisites) than educational maths and is therefore more tedious to annotate.
3. In any markup there is an economic tradeoff: is the investment into markup going to pay off in terms of the help I get from semantic servicers. You can usually amortize the semantization investment, if you have more (best many more) readers that profit from semantic services than authors (who have to invest into semantization). Here educational materials score better than research maths.

But other than this, I see no principal problems with doing research-level maths in sTeX. Indeed, one semantic service I see that might make the investment into research maths worthwile is computer-supported change management in larger research projects (maybe even collaborative). Think you have to change a definition from the start of the project, which parts of your proof attempt are affected and need to be redone.

[kohlhase]

All in all I see sTeX more at the publication stage (or the writing up carefully stage) of doing mathematics than at the explorative stage.

Maybe you are interested in jointly annotating some (completed) paper of your's in sTeX, so that we get a more detailed look. We will probably have problems to understand the maths, but we could supply the sTeX knowledge

[Jazzpirate]

Hi @sorsted - Nice to meet you :)

But research-level mathematics is a much more dynamic, chaotic mess. Variables can suddenly act as maps, maps can act as variables, notations can change on the go, and the value of a function may be another function.

Right - which is why it is important that sTeX is/remains flexiformal - where the semantics is clear and precise, it can be used. Where it can't (yet?) it doesn't have to be. In the long term, the more we understand about what's "required", the more we can expand the scope of what's possible. All the mathstructure, copymodule etc mechanism for example are the result of many years of trying to understand how to "properly" formalize the Bourbaki-style algebraic theories in a "natural" manner.

Take the case of a functor, for instance. If F is a functor, I can apply it to an object x and get an object F(x), or I can apply it to a map f and get a map F(f). So depending on what I apply F to, the output will be an object with a varying number of arguments.

I would disagree: "Formally", a functor is a structure consisting of two functions, one on objects and one (polymorphic) on morphisms - they just happen to have the same notation :) Admittedly, that answer probably makes a lot more sense to "formal" mathematicians than (I'm tempted to say "real") "informal" mathematicians. That is the trade-off between formality and "naturality" I guess: Occasionally one is forced to think about the "strictly formal" definitions of things - anecdotally, such definitions however seem to always exist (which unfortunately is very distinct from saying that they're always convenient to use!)

My formalization of functors can be found here, by the way: https://gl.mathhub.info/sTeX/CategoryTheory/-/blob/main/source/mod/Functor.en.tex

[Jazzpirate]

By the way, to showcase why we even care: This is what MMT/RusTeX do with the linked tex-file (and my godawful CSS javascript hacking, which is soon-to-be replaced by someone who actually knows what they're doing :D) https://mmt.beta.vollki.kwarc.info/:sTeX/browser?archive=sTeX/CategoryTheory&filepath=mod/Functor.en.xhtml

And here is what MMT can extract as actually fully formal content (which is boring to look at, but informative for formal-methods-people): https://mmt.beta.vollki.kwarc.info/?http://mathhub.info/sTeX/CategoryTheory/mod/Functor.en.omdoc

[Jazzpirate]

For completeness/documentation/posteriority's sake in detail:

Variables can suddenly act as maps

Anything can be applied to anything using the \apply-semantic-macro from the default meta-theory, e.g. \apply{x}{a,b,c,d} will typeset x(a,d,c,d). As a semantic macro, \apply can be provided new notations like any other sTeX-symbol.

maps can act as variables

The operator-notation of a symbol allows for using a "function-like" symbol with arity > 0 directly, e.g. given \symdef{somefunction}[args=3,op=f]{...}, then \somefunction! will simply typeset f without taking arguments.

notations can change on the go

New notations can be provided at any point. In math mode, the starred variant \semanticmacro* allows for typesetting using a custom notation (see documentation)

and the value of a function may be another function.

Not a problem, using operator-notations :)

Take the case of a functor, for instance.

See above

Or imagine that I consider the cohomology H^{\bullet}(X, \mathcal{F}) of X with values in a sheaf \mathcal{F}, but that when \mathcal{F} is the constant sheaf on the complex numbers, I just write H^{\bullet}(X) (this is quite common practice).

Semantically, those are two distinct symbols - a generic \symdef{cohomology}[args=2]{H^{\bullet}(#1, #2)} and a specialized \symdef{cohomologyonC}[args=1,def=\bind{x}{\cohomology{x}{\sheafOnC}}]{H^{\bullet}(#1)}

Or imagine that I take a scheme X and then consider its functor of points X(R) = \Hom(\Spec R, X).

Or what if I want to define the pushforward sheaf as f_{*}(\mathcal{F})(U) = \mathcal{F}(f^{-1}(U))?

I don't understand these situations or the problems associated with them well enough to comment, unfortunately

[sorsted]

Sorry for the late reply, I had a busy weekend. :-)

Maybe you are interested in jointly annotating some (completed) paper of your's in sTeX, so that we get a more detailed look. We will probably have problems to understand the maths, but we could supply the sTeX knowledge

We can try! :-) At least we can at some point in the not-so-distant future (when I become a bit less busy with the stuff I’m doing right now). I think the most natural choice would be this one, which has the most formal and stringent notation out of the papers I have written.

Variables can suddenly act as maps

Anything can be applied to anything using the \apply-semantic-macro from the default meta-theory, e.g. \apply{x}{a,b,c,d} will typeset x(a,d,c,d). As a semantic macro, \apply can be provided new notations like any other sTeX-symbol.

maps can act as variables

The operator-notation of a symbol allows for using a "function-like" symbol with arity > 0 directly, e.g. given \symdef{somefunction}[args=3,op=f]{...}, then \somefunction! will simply typeset f without taking arguments.

Oh, I’ve been there. For a very long time, SemanTeX also distinguished very clearly between variables (taking no arguments) and maps (taking arguments). Theoretically, this sounded like the natural way to do it, and I used a similar syntax to yours (with ! replaced by .). But alas, math does not speak this language. It changes too much and too rapidly. As I said in one of my examples, a scheme X (arguably the most important type of space studied in algebraic geometry) is commonly regarded as a functor from rings to sets (the so-called functor of points). So what happened in practice was that I would define some objects as variables and others as maps and quickly get confused about which ones were which. As a result, I would often forget . in important places. At best, this would create weird situations in the text. At worst, it would cause the entire system to crash.

Eventually, I gave up on this and just decided that variables and maps were one and the same thing. So I did the most blasphemous thing in all of LaTeX programming and used g-type arguments (the TeX gurus still have me for this). So any variable \vx can also be used as a map by typing \vx{\vt}. This immediately lifted all my burdens and allowed me to concentrate on typing the math as I think it, rather than how computer scientists would probably want me to think it. I think that this fundamental discrepancy between the math approach and the computer science approach is part of what makes it hard to create a math typesetting engine that effectively captures the underlying semantics.

Or imagine that I consider the cohomology H^{\bullet}(X, \mathcal{F}) of X with values in a sheaf \mathcal{F}, but that when \mathcal{F} is the constant sheaf on the complex numbers, I just write H^{\bullet}(X) (this is quite common practice).

Semantically, those are two distinct symbols - a generic \symdef{cohomology}[args=2]{H^{\bullet}(#1, #2)} and a specialized \symdef{cohomologyonC}[args=1,def=\bind{x}{\cohomology{x}{\sheafOnC}}]{H^{\bullet}(#1)}

That is completely true. However, trust me when I say this, because I have spent a lot of time thinking about semantic typesetting from the point of view of a researcher: It gets extremely cumbersome. Sure, we can have cohomology with or without coefficients. Or we can have relative cohomology H^{\bullet}(X,A) for some subset A \subset X. Or we can have non-equivariant cohomology H or equivariant cohomology H_G with respect to the action of a group G. Or we can have Čech cohomology \check{H}. Or we can have hyper-cohomology \mathbb{H}. Or we can have equivariant, relative, Čech hyper-cohomology with coefficients, \check{\mathbb{H}}_{G}^{\bullet}(X, A, \mathcal{F}). Or any other combination of these. So you end up with 2^n macros for n tending towards infinity.

You can try doing that, and I did, but eventually, any math researcher will give up on this and probably just end up typing the notation directly. In fact, these issues were what caused me to develop SemanTeX in the first place. This allows me to type something like

\cohomology[
    equivar=\gpG,
    rel=\vA,
    cech,
    hyper,
    coef=\sheafF,
    *
]{ \vX }

This can be accomplished using the “parse routine”.

[Jazzpirate]

We can try! :-) At least we can at some point in the not-so-distant future (when I become a bit less busy with the stuff I’m doing right now). I think the most natural choice would be this one, which has the most formal and stringent notation out of the papers I have written.

Sounds like a fun challenge :) My algebraic geometry is very rusty at best, and as you can imagine I hardly understand a word of the abstract, but the nice thing about sTeX (in comparison to other fully formal systems, like interactive theorem provers etc) is that we can always leave gaps when semantifying things, so I will not have to become a master in algebraic geometry to get a decent amount of formal semantics in there - especially with your help.

To avoid some confusion, I should preface this with a disclaimer though: The primary goal of sTeX is not to make typesetting mathematics easier - it is to allow for annotating mathematical document fragments with their formal semantics. This is an important point, because it

1. implies that using sTeX to its fullest will necessarily make things harder for authors a priori (which of course does not mean that it should not be as easy and painless as possible), and
2. thigs that are formally conceptually distinct, should be made distinct when using sTeX macros, even if they have the same notations/syntax.

For example, a scheme (as a locally ringed space that admits a covering...) is a decidedly distinct thing (from a formal point of view) from the functor of points associated with the scheme - this becomes somewhat obvious if you think of the definitions of both in pure ZFC, for example (although that would be an extremely formal position to take).

What this means for us is that we would want to make this distinction explicit in sTeX. This is a definite drawback for well-informed authors writing for well-informed readers, since as mentioned, it only makes things harder for them if they are "forced" to suddenly distinguish between things that are natural for them to equivocate in practice, and under the assumption that "everyone knows what this means anyway".

However, it is a strong advantage to distinguish between the two when writing for a less-informed audience, from a pedagogical point of view, in particular in conjunction with semantics-aware services that can actually act on the provided semantics! For example, if we go back to the distinction between the imagined \cohomology and \cohomologyOnC-macros, an sTeXified paper would allow for a less-informed reader wondering "wait, what scheme is this supposed to be the cohomology on again?" to just hover over a term and a pop-up would inform them which one it is (assuming that \cohomologyOnC is associated with a definition-fragment that tells them). Similarly, someone who knows about schemes but who has not yet fully grasped how functors on points work, who might be confused by a notation like X(R) could hover over the term and be presented with the definition of the functor on points.

This hovering-over-terms-thing is just a first low-hanging-fruit we could quickly implement of what software can offer in terms of semantic added-value services, of course. Our hope is that the "pain" associated with annotating things formally will soon be considered sufficiently worthwhile in the face of such services. For example, we recently submitted the following paper on and in sTeX, for which you are probably not the intended audience, but precisely because of that I would hope that you can see the value in having the paper be an active document with all the technical terms being "semantified": https://mmt.beta.vollki.kwarc.info/:sTeX/browser?archive=Papers&filepath=stex-mmt/paper.xhtml

Also, it's probably not a coincidence that the largest collection of sTeX documents we currently have are all of Michael's lecture notes, where we are actively working on providing students with semantics-based services.

But, as Michael mentioned and I will also freely admit, the cost-benefit-analysis for active research mathematics will probably not be in our favor as of yet.

Another aspect to mention here, however, is that sTeX has a sophisticated module system intended to somewhat painlessly import and export semantic macros between small document fragments that serve as kind-of "lexicographic entries" for reuse. What this means is that ideally, the pain of properly formally semantifying mathematical concepts can be left to the community and can be done collaboratively, while the pain of subsequently reusing these once-semantified-concepts should be ideally negligable - in particular in conjunction with a proper IDE that helps with finding, importing and using semantic macros from a large library. Such an IDE is currently in the works, and such a library already exists in the form of the smglom (see https://gl.mathhub.info/smglom/, although the smglom predates our recent massive developments of sTeX, so it very much underutilizes what we can do by now).

[sorsted]

However, it is a strong advantage to distinguish between the two when writing for a less-informed audience, from a pedagogical point of view, in particular in conjunction with semantics-aware services that can actually act on the provided semantics! For example, if we go back to the distinction between the imagined \cohomology and \cohomologyOnC-macros, an sTeXified paper would allow for a less-informed reader wondering "wait, what scheme is this supposed to be the cohomology on again?" to just hover over a term and a pop-up would inform them which one it is (assuming that \cohomologyOnC is associated with a definition-fragment that tells them). Similarly, someone who knows about schemes but who has not yet fully grasped how functors on points work, who might be confused by a notation like X(R) could hover over the term and be presented with the definition of the functor on points.

And I completely agree on that. SemanTeX has exactly the same purpose. What I am warning you against is making the syntax too “stiff” and non-flexible, at least if you want your system to become accessible to authors. One way to provide flexibility is through keyval syntax. My single keyval-based cohomology macro above contains exactly the same information as your two (or 2^n) different cohomology macros do. Accordingly, my macro could be programmed to make exactly the same annotations, including additional information accessible by hovering over the math.

As for the functor of points, this is my take on it: Unless you plan on writing all of your math out in pure first order logic, any semantic interpretation of math syntax will involve some guessing. For instance, you provide commands like \addition and \multiplication. Addition and multiplication where? In the complex numbers? In a vector space? In an arbitrary ring? And as you say yourself, you supply an abstract macro \apply, but whatever “apply” means can be an almost philosophical question. The goal of a semantic markup system is to provide enough information for the system to be able to make a qualified, more or less concrete guess as to what is meant.

Therefore, typing the functor of points X(R) as \schemeX{\ringR} or \apply{X}{R} is not really a problem, as long as the system is told that whenever you apply a scheme to something, that means the functor of points. I don’t know how you would program that in sTeX, but in SemanTeX, you could in principle do something like

\SetupClass\Schemes{
    append keys[1]={
        {arg}{
            % this appends the "argument" key with extra code
            hover description={functor of points},
            smglom library={algebraic geometry/scheme theory/functor of points},
        },
    },
}

The keys “hover description” and “smglom library” are, of course, a completely made up syntax, but they could probably already be implemented as the system is now. Now \schemeX{\ringR} will automatically run the code I just added.

Alternatively, if we want to allow more than one use of the argument key for schemes, one could instead do

\SetupClass\Schemes{
    define keys={
        {functor of points}{
            % this adds the key "functor of points"
            hover description={functor of points},
            smglom library={algebraic geometry/scheme theory/functor of points},
        },
    },
}

Now I can type \schemeX[functor of points]{\ringR} to get the same result.

[Jazzpirate]

Ah. Yes, I get your point, and I agree - navigating the space between flexibility and formality is a real tight-rope to walk on.

One way to provide flexibility is through keyval syntax. My single keyval-based cohomology macro above contains exactly the same information as your two (or 2^n) different cohomology macros do.

This is true as long as we stay within LaTeX. It gets more tricky once we go to MMT/OMDoc (the backend language we use to represent the semantics formally), where there is no real analogue for such key-value-pairs... a syntax like yours would probably have to be "elaborated" into the 2^n different symbols - either by the sTeX-package or by the subsequent import. But this is definitely worth keeping in mind and thinking about...

Unless you plan on writing all of your math out in pure first order logic, any semantic interpretation of math syntax will involve some guessing.

Some guessing (or, rather, strict inference) is already involved, but by and large, actual heuristic guessing we try to avoid as much as possible - although we wouldn't go to pure first-order logic. There are more adequate logics for our purposes - or, rather, since we don't want to fixate one one such logical foundation (exactly because we want to be more flexible): there are representational principles commonly used in more advanced logical foundations that we are influenced by, that we can use for our purposes and which offer more flexibility than FOL.

For instance, you provide commands like \addition and \multiplication. Addition and multiplication where? In the complex numbers? In a vector space? In an arbitrary ring?

Indeed, for us, all of those would be separate symbols, since they have distinct semantics. All rings/fields/vector spaces carry their own additions, multiplications, zeros, ones, etc. Also, addition and multiplication on real numbers would be distinct from those on the integers (but connected via "subtyping"-principles to ensure compatibility). Yes, that makes things more cumbersome, but this "making things explicit" is indeed what we're aiming for; up to a point at least - some "implicit coercion" between related "types"/functions is certainly desirable and even necessary, but where and to what degree is occasionally limited by existing automated-inference-technology, and in other places some point in a negotiable design space with various trade-offs involved that would need to be considered. You strike me as very much arguing from the standpoint of wanting to maximize ease-of-use for authors - and rightfully so, that standpoint is very much appreciated. On the flipside though, we are constrained by further algorithmic considerations. In the extreme case, fully infering everything is of course AI-complete ;)

And as you say yourself, you supply an abstract macro \apply, but whatever “apply” means can be an almost philosophical question. The goal of a semantic markup system is to provide enough information for the system to be able to make a qualified, more or less concrete guess as to what is meant.

Very true! From the point of view of LaTeX, this doesn't matter much, since the sTeX-package itself only generates the semantic annotations and takes care of the type setting. From the point of view of MMT/OMDoc, situational semantics of something generic like "application" is extensible and refinable by providing corresponding programmatic rules (modularly). For example, one such rule already says that "a sequence s applied to an index i computes to the i-th component of s".

Therefore, typing the functor of points X(R) as \schemeX{\ringR} or \apply{X}{R} is not really a problem, as long as the system is told that whenever you apply a scheme to something, that means the functor of points.

True - it would be possible to provide a situational rule that automatically inserts the "functor-of-points-function" to turn the scheme into the associated functor. I'm not sure that in this specific example, that is something that should happen automatically, though - this (at least to me) feels very much like the kind of thing that should indeed be made explicit. After all, wehether we do it manually or automatically, we either way would want/need a (somewhat formal or informal) definition of what a functor-of-points associated with a scheme even is, and of course an associated symbol for it - meaning, such a functor-of-points-function \fop should exist anyway, at which point it does not seem too much effort to just write \fop{<some scheme>}{...} rather than \apply{<some scheme>}{...}.

I don’t know how you would program that in sTeX, but in SemanTeX, you could in principle do something like

\SetupClass\Schemes{
  append keys[1]={
      {arg}{
          % this appends the "argument" key with extra code
          hover description={functor of points},
          smglom library={algebraic geometry/scheme theory/functor of points},
      },
  },
}

The keys “hover description” and “smglom library” are, of course, a completely made up syntax, but they could probably already be implemented as the system is now. Now \schemeX{\ringR} will automatically run the code I just added.

Alternatively, if we want to allow more than one use of the argument key for schemes, one could instead do

\SetupClass\Schemes{
  define keys={
      {functor of points}{
          % this adds the key "functor of points"
          hover description={functor of points},
          smglom library={algebraic geometry/scheme theory/functor of points},
      },
  },
}

Now I can type \schemeX[functor of points]{\ringR} to get the same result.

Mmmhm - I'm still not convinced when it comes to the specific case of schemes and functors for the reasons above, but generally, this idea is indeed intriguing - I'm easily convinced that there will be situations where we would want something like this.

I think at this point I would suggest a zoom meeting some time in the future, once you're less busy?

[sorsted]

I think at this point I would suggest a zoom meeting some time in the future, once you're less busy?

Yes, I’m completely up for that! I’m currently working as a postdoc in representation theory in Jerusalem, and I’m desperately trying to prove my worth to my host before my time here runs out xD. That is what currently keeps me busy ;-). But let us indeed Zoom and exchange ideas soon, hopefully later this Summer. :-)

[Jazzpirate]

Yes, I’m completely up for that! I’m currently working as a postdoc in representation theory in Jerusalem, and I’m desperately trying to prove my worth to my host before my time here runs out xD. That is what currently keeps me busy ;-)

Oh, yes, indeed, that is certainly not something I would want to keep you from. Then all the best with your effort and I would love to hear from you once you have less on your plate :)

[sorsted]

Oh, yes, indeed, that is certainly not something I would want to keep you from. Then all the best with your effort and I would love to hear from you once you have less on your plate :)

Thank you! And don’t worry, I’m not just saying this as an excuse. I will get back to you as soon as possible. :-)

[sorsted]

Hi, just here with an update to show I’m still alive: I have started the process of editing that paper of mine to make it ready to be annotated. This means tidying up the code, which as developed over many years as SemanTeX was being developed, so that others than myself can actually read it. Stay tuned. ;-)

[Jazzpirate]

Hi @sorsted - looking forward to hear from you. In the meantime, we have submitted a paper to the TeX Users Group converence, which I will present (in our timezone) sunday morning. If you're free, you'd be welcome to attend (registration is free), and I'm going to demonstrate somewhat in depth what we can do with sTeX (beyond mere LaTeX->PDF things): https://tug.org/tug2022/program.html (the paper is also linked in the schedule)

[sorsted]

Hi @Jazzpirate, thanks for the update. I have now registered and hope to be able to attend your presentation. :-)

[sorsted]

Hello again, @kohlhase and @Jazzpirate. Hehe, just when you thought I had forgotten you, I finally returned. ;-)

Nice TUG talk by the way, @Jazzpirate. :-)

It’s been a few busy months. I managed to get a new postdoctoral position in Haifa, Israel, so my job situation is a lot more secure now. Hence I finally managed to find some time for preparing the paper in question for sTeX’ing, as suggested by the two of you. :-)

Anyway, the article I mentioned was the very first one I ever wrote, and SemanTeX was being developed along with it. As that package has undergone a lot (!!!) of changes over the years, the source code of the article has changed along with it. So it was, to say it mildly, a giant mess that needed a lot of cleaning up. That took some work, but I think it has finally reached a presentable state where I am no longer embarrassed to let others read it.

I provide two versions of the paper: One written with SemanTeX and one where the SemanTeX code has been stripped via the companion package, stripsemantex, which is also available on CTAN. Therefore, the second one consists of generated code with almost no user macros, but it’s still very much readable, if you ask me. I would really like to know whether or not SemanTeX can be made to output sTeX code, so I suggest that any attempts at sTeX’ing it should start with the first version. But what do you think? :-)

Anyway, if you’re still up for it, we can also set up a Zoom meeting at some point in the foreseeable future, as suggested by the two of you. ;-)

\begin{filecontents*}{references.bib}
@article{comodules,
    author = {Arkhipov, Sergey and Ørsted, Sebastian},
    year = {2021},
    pages = {1-35},
    volume = {7},
    journal = {European Journal of Mathematics},
    doi = {10.1007/s40879-020-00439-4},
    title = {Homotopy limits in the category of dg-categories in terms of $\mathrm{A}_{\infty}$-comodules},
}

@article{explicit,
    author={Block, Jonathan and Holstein, Julian {V.S.} and Wei, Zhaoting},
    title={Explicit homotopy limits of dg-categories and twisted complexes},
    year={2017},
    journal={Homology, Homotopy and Applications},
    volume={19(2)},
    pages={343-371},
}

@online{dugger,
    year={2008},
    hyphenation={american},
    author={Dugger, Daniel},
    title={A primer on homotopy colimits},
    url={http://pages.uoregon.edu/ddugger/hocolim.pdf},
}

@article{gambino_simplicial,
    author = {Gambino, Nicola},
    title = {Weighted limits in simplicial homotopy theory},
    journal = {Journal of Pure and Applied Algebra},
    volume = {214},
    number = {7},
    pages = {1193 - 1199},
    year = {2010},
    %issn = "0022-4049",
    %doi = "https://doi.org/10.1016/j.jpaa.2009.10.006",
    %url = "http://www.sciencedirect.com/science/article/pii/S0022404909002412",
}

@book{hir,
    author={Hirschhorn, Philip S.},
    year={2003},
    title={Model Categories and Their Localizations},
    publisher={American Mathematical Society},
    series={Mathematical Surveys and Monographs},
    volume={99},
}

@book{hovey,
    hyphenation={american},
    author={Hovey, Mark},
    title={Model categories},
    year={1999},
    publisher={American Mathematical Society},
    series={Mathematical Surveys and Monographs},
    volume={63},
    url={https://web.math.rochester.edu/people/faculty/doug/otherpapers/hovey-model-cats.pdf},
}

@book{htt,
    hyphenation={american},
    author={Lurie, Jacob},
    title={Higher Topos Theory},
    year={2009},
    series={Annals of Mathematics Studies},
    number={170},
    publisher={Princeton University Press},
}

@book{riehl,
    hyphenation={american},
    author={Riehl, Emily},
    year={2014},
    title={Categorical Homotopy Theory},
    publisher={Cambridge University Press},
}
\end{filecontents*}

\documentclass[a4paper,oneside,article,english,leqno,10pt]{memoir}

\newif\ifprenumber % if theorems should use format number. type
\prenumbertrue

\makeatletter

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[shorthands=off]{babel}
\usepackage[noDcommand,slantedGreeks]{kpfonts}

\frenchspacing

\usepackage{mathtools, microtype}

\usepackage[shortlabels]{enumitem}

\AddToHook{bfseries}{\boldmath}

\usepackage[autostyle,english=american]{csquotes}

\usepackage[backend=biber,citestyle=authoryear-icomp,bibstyle=authoryear,
    uniquename=init,giveninits=true,autolang=hyphen]{biblatex}
\addbibresource{references.bib}
\nobibintoc

\let\textdef=\textbf

\usepackage[thmmarks,amsmath]{ntheorem}

\def\@nthm@theorem{Theorem}
\def\@nthm@proposition{Proposition}
\def\@nthm@corollary{Corollary}
\def\@nthm@lemma{Lemma}
\def\@nthm@claim{Claim}
\def\@nthm@definition{Definition}
\def\@nthm@example{Example}
\def\@nthm@exercise{Exercise}
\def\@nthm@remark{Remark}
\def\@nthm@proof{Proof}

\makeatletter
\newtheoremstyle{notitle}% for exercises
{\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator]}%
{\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##3\theorem@separator]}

\newtheoremstyle{notitlebreak}% for exercises with a break
{\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont ##2\theorem@separator}\hbox{\strut}}}]}%
{\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##3\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{prenumber}%
  {\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##1\theorem@separator]}%
  {\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##3\theorem@separator]}

\newtheoremstyle{prenumberbreak}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##2\theorem@separator\ ##1\theorem@separator}\hbox{\strut}}}]}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##2\theorem@separator\ ##3\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{customplain}%
  {\item[\hskip\labelsep \theorem@headerfont ##1\ ##2\theorem@separator]}%
  {\item[\hskip\labelsep \theorem@headerfont ##3\ ##2\theorem@separator]}

\newtheoremstyle{custombreak}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont
          ##1\ ##2\theorem@separator}\hbox{\strut}}}]}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##3\ ##2\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{postnumpara}%
  {\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator]}%
  {\item[\hskip\labelsep \theorem@headerfont ##3\ ##2\theorem@separator]}

\newtheoremstyle{postnumparabreak}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont
          ##2\theorem@separator}\hbox{\strut}}}]}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##3\ ##2\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{nonumberplainflex}% for proof environments, see below
    {\item[\theorem@headerfont\hskip\labelsep ##1\theorem@separator]}%
    {\item[\theorem@headerfont\hskip \labelsep ##3\theorem@separator]}

\newtheoremstyle{nonumberbreakflex}%
    {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont
        ##1\theorem@separator}\hbox{\strut}}}]}%
    {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
        ##3\theorem@separator}\hbox{\strut}}}]}

\theoremseparator{.}

\theorembodyfont{\normalfont}

\ifprenumber
    \theoremstyle{notitle}
\else
    \theoremstyle{postnumpara}
\fi

%\newtheorem{para}{}[chapter]
\newtheorem{para}[equation]{}

\ifprenumber
    \theoremstyle{prenumber}
\else
    \theoremstyle{customplain}
\fi

\theorembodyfont{\itshape}

\newtheorem{theorem}[equation]{\@nthm@theorem}
\newtheorem{fact}[equation]{Fact}
\newtheorem{corollary}[equation]{\@nthm@corollary}
\newtheorem{proposition}[equation]{\@nthm@proposition}
\newtheorem{lemma}[equation]{\@nthm@lemma}
\newtheorem{claim}[equation]{\@nthm@claim}
\newtheorem{conjecture}[equation]{Conjecture}

\theorembodyfont{\normalfont}
\newtheorem{definition}[equation]{\@nthm@definition}
\newtheorem{textexercise}[equation]{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remark}[equation]{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{example}[equation]{\@nthm@example}

\theoremstyle{notitle}
\newtheorem{exercise}{\@nthm@exercise}[chapter]

\theoremstyle{nonumberplainflex}
\theoremsymbol{\ensuremath{\square}}
\theoremheaderfont{\itshape\bfseries}
\newtheorem{proof}{\@nthm@proof}

%Unnumbered variants

\theoremstyle{nonumberplainflex}
\theoremheaderfont{\normalfont\bfseries}
\theoremsymbol{}

\theorembodyfont{\normalfont}

\newtheorem{paranonumber}{}

\theorembodyfont{\itshape}
\newtheorem{theoremnonumber}{\@nthm@theorem}
\newtheorem{factnonumber}{Fact}
\newtheorem{corollarynonumber}{\@nthm@corollary}
\newtheorem{propositionnonumber}{\@nthm@proposition}
\newtheorem{lemmanonumber}{\@nthm@lemma}
\newtheorem{claimnonumber}{\@nthm@claim}

\theorembodyfont{\normalfont}
\newtheorem{definitionnonumber}{\@nthm@definition}
\newtheorem{textexercisenonumber}{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remarknonumber}{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{examplenonumber}{\@nthm@example}

%Break variants with line break right after the heading

\theoremsymbol{}
\theoremheaderfont{\normalfont\bfseries}

\ifprenumber
    \theoremstyle{notitlebreak}
\else
    \theoremstyle{postnumparabreak}
\fi

\newtheorem{parabreak}[equation]{}

\ifprenumber
    \theoremstyle{prenumberbreak}
\else
    \theoremstyle{custombreak}
\fi

\theorembodyfont{\itshape}
\newtheorem{theorembreak}[equation]{\@nthm@theorem}
\newtheorem{factbreak}[equation]{Fact}
\newtheorem{corollarybreak}[equation]{\@nthm@corollary}
\newtheorem{propositionbreak}[equation]{\@nthm@proposition}
\newtheorem{lemmabreak}[equation]{\@nthm@lemma}
\newtheorem{claimbreak}[equation]{\@nthm@claim}
\newtheorem{conjecturebreak}[equation]{Conjecture}

\theorembodyfont{\normalfont}
\newtheorem{definitionbreak}[equation]{\@nthm@definition}
\newtheorem{textexercisebreak}[equation]{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remarkbreak}[equation]{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{examplebreak}[equation]{\@nthm@example}

\theoremsymbol{}

\theoremstyle{notitlebreak}
\newtheorem{exercisebreak}[exercise]{\@nthm@exercise}

\theoremstyle{nonumberbreakflex}
\theoremsymbol{\ensuremath{\square}}
\theoremheaderfont{\itshape\bfseries}
\newtheorem{proofbreak}{\@nthm@proof}

% Unnumbered break variants:

\theoremstyle{nonumberbreakflex}
\theoremheaderfont{\normalfont\bfseries}
\theoremsymbol{}
\theorembodyfont{\normalfont}

\newtheorem{parabreaknonumber}{}

\theorembodyfont{\itshape}

\newtheorem{theorembreaknonumber}{\@nthm@theorem}
\newtheorem{factbreaknonumber}{Fact}
\newtheorem{corollarybreaknonumber}{\@nthm@corollary}
\newtheorem{propositionbreaknonumber}{\@nthm@proposition}
\newtheorem{lemmabreaknonumber}{\@nthm@lemma}
\newtheorem{claimbreaknonumber}{\@nthm@claim}
\newtheorem{conjecturebreaknonumber}{Conjecture}

\theorembodyfont{\normalfont}
\newtheorem{definitionbreaknonumber}{\@nthm@definition}
\newtheorem{textexercisebreaknonumber}{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remarkbreaknonumber}{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{examplebreaknonumber}{\@nthm@example}

% Links at references. The "hidelinks" option makes the links colour-neutral
\usepackage[hidelinks]{hyperref}

\usepackage[nameinlink]{cleveref}

\crefname{para}{}{}
\crefname{theorem}{Theorem}{Theorems}
\crefname{claim}{Claim}{Claims}
\crefname{conjecture}{Conjecture}{Conjectures}
\crefname{fact}{Fact}{Facts}
\crefname{definition}{Definition}{Definitions}
\crefname{example}{Example}{Examples}
\crefname{corollary}{Corollary}{Corollaries}
\crefname{proposition}{Proposition}{Propositions}
\crefname{lemma}{Lemma}{Lemmata}
\crefname{remark}{Remark}{Remarks}
\crefname{claim}{Claim}{Claims}
\crefname{exercise}{Exercise}{Exercises}
\crefname{textexercise}{Exercise}{Ecercises}

\crefalias{parabreak}{para}

\crefalias{theorembreak}{theorem}

\crefalias{conjecturebreak}{conjecture}

\crefalias{claimbreak}{claim}

\crefalias{factbreak}{fact}

\crefalias{definitionbreak}{definition}

\crefalias{examplebreak}{example}

\crefalias{corollarybreak}{corollary}

\crefalias{propositionbreak}{proposition}

\crefalias{lemmabreak}{lemma}

\crefalias{claimbreak}{claim}

\crefalias{remarkbreak}{remark}

\crefalias{textexercisebreak}{textexercise}

\newcommand{\crefrangeconjunction}{--} %gives e.g. "table~1--2" instead of "table 1 to~2"

% Now to define environments for theorem parts

\newlist{paralist}{enumerate}{2}
\setlist[paralist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{paralisti}{theorem}

\newlist{theoremlist}{enumerate}{2}
\setlist[theoremlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{theoremlisti}{theorem}

\newlist{corollarylist}{enumerate}{2}
\setlist[corollarylist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{corollarylisti}{corollary}

\newlist{propositionlist}{enumerate}{2}
\setlist[propositionlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{propositionlisti}{proposition}

\newlist{lemmalist}{enumerate}{2}
\setlist[lemmalist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{lemmalisti}{lemma}

\newlist{definitionlist}{enumerate}{2}
\setlist[definitionlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{definitionlisti}{definition}

\newlist{textexerciselist}{enumerate}{2}
\setlist[textexerciselist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{textexerciselisti}{textexercise}

\newlist{remarklist}{enumerate}{2}
\setlist[remarklist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{remarklisti}{remark}

\newlist{examplelist}{enumerate}{2}
\setlist[examplelist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{examplelisti}{example}

\newlist{exerciselist}{enumerate}{2}
\setlist[exerciselist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{exerciselisti}{exercise}

\newlist{claimlist}{enumerate}{2}
\setlist[claimlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{claimlisti}{claim}

% The \localref command, allowing references to, say, part (ii) of a theorem without having the theorem number in front; this happens by default due to the above settings

%\makeatletter
\newcounter{localreftmpcnt} %
\newcommand\alphsubformat[1]{\textup{(\roman{#1})}} %adapt ....
\newcommand\localref[2][\alphsubformat]{%
    \ifcsname r@#2@cref\endcsname
    \cref@getcounter {#2}{\mylabel}%
    \setcounter{localreftmpcnt}{\mylabel}%
    \hyperref[#2]{%
        \alphsubformat{localreftmpcnt}%
    }%
    \else ?? \fi}   
%\makeatother

\title{Homotopy (co)limits via homotopy (co)ends in general combinatorial model categories}
\date{\today}
\author{Sergey Arkhipov and Sebastian Ørsted}

\hypersetup{
    pdfauthor={\@author},
    pdftitle={Ω-modules and the affine Hecke category},
}

\numberwithin{equation}{section}

\newcommand\longto{\longrightarrow}
\newcommand\into{\hookrightarrow}

\newcommand\categoryformat[1]{{\operatorname{#1}}}
\newcommand\modelstructureproj{\mathup{Proj}}
\newcommand\modelstructureinj{\mathup{Inj}}
\newcommand\modelstructurereedy{\mathup{Reedy}}

\def\varlim@@auxiliary#1#2#3{%
  \vtop{\m@th\ialign{##\cr
    \hfil$#1\operator@font #3$\hfil\cr
    \noalign{\nointerlineskip\kern0\ex@}
    \expandafter#2\ifx#1\scriptscriptstyle\scriptscriptstyle\else\scriptstyle\fi\cr
    \noalign{\nointerlineskip\kern-\ex@}\cr}}%
}
\def\varlim@@#1#2{%
    \varlim@@auxiliary#1#2%
}

\newcommand\dirlimcommand[1]{\mathop{\mathpalette\varlim@@{{\rightarrowfill@}{#1}}}\nmlimits@}
\newcommand\invlimcommand[1]{\mathop{\mathpalette\varlim@@{{\leftarrowfill@}{#1}}}\nmlimits@}

\usepackage{tikz}
\usetikzlibrary{quotes,babel}
\usetikzlibrary{cd}

\tikzcdset{
  arrow style=tikz,
}

\tikzset{
  >/.tip={Stealth[length=2.9pt, width=4.4pt, inset=1.8pt]},
  tikzcd left hook/.tip={Hooks[
      left,
      length=2pt,
      width=5.5pt,
    ]},
}

\newcommand\invdot{\mathrlap{.}}
\newcommand\invcomma{\mathrlap{,}}

\newcommand\noloc{%
  \nobreak
  \mspace{6mu plus 1mu}
  {:}
  \nonscript\mkern-\thinmuskip
  \mathpunct{}
  \mspace{2mu}
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                                                         %
%            THE SEMANTEX PART OF THE PREAMBLE            %
%                                                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\usepackage{semantex}

\SemantexSetup{
    semtex file=true,
}

\NewVariableClass\MyVar[
    output=\MyVar,
    define keys={
        {op}{upper=\mathup{op}},
    },
    define keys={
        {proj}{model structure={\modelstructureproj}},
        {inj}{model structure={\modelstructureinj}},
        {reedy}{model structure={\modelstructurereedy}},
        {reedy+}{lower=+},
        {reedy-}{lower=-},
        {*kan}{ lower=*,no par },
        {!kan}{ lower=!,no par },
        {*res}{ upper=*,no par },
        {boundary}{ left return, symbol put left=\partial },
        {simp *}{ i * },
        {cosimp *}{ d * },
    },
    define keys[1]={
        {diag}{ upper={#1} },
        {powering}{ upper={#1} },
        {comma category}{right return,symbol put right={/#1}},
        {model structure}{lower={#1}},
        {latching}{left return, symbol put left=L_{#1}},
        {matching}{left return, symbol put left=M_{#1}},
        {simp}{ sep lower={#1} },
        {cosimp}{ sep upper={#1} },
    },
]

\NewObject\MyVar\slot{{-}}

\NewObject\MyVar\va{a}
\NewObject\MyVar\vb{b}
\NewObject\MyVar\vc{c}
\NewObject\MyVar\vd{d}
\NewObject\MyVar\ve{e}
\NewObject\MyVar\vf{f}
\NewObject\MyVar\vg{g}
\NewObject\MyVar\vh{h}
\NewObject\MyVar\vi{i}
\NewObject\MyVar\vj{j}
\NewObject\MyVar\vk{k}
\NewObject\MyVar\vl{l}
\NewObject\MyVar\vm{m}
\NewObject\MyVar\vn{n}
\NewObject\MyVar\vo{o}
\NewObject\MyVar\vp{p}
\NewObject\MyVar\vq{q}
\NewObject\MyVar\vr{r}
\NewObject\MyVar\vs{s}
\NewObject\MyVar\vt{t}
\NewObject\MyVar\vu{u}
\NewObject\MyVar\vv{v}
\NewObject\MyVar\vw{w}
\NewObject\MyVar\vx{x}
\NewObject\MyVar\vy{y}
\NewObject\MyVar\vz{z}

\NewObject\MyVar\vA{A}
\NewObject\MyVar\vB{B}
\NewObject\MyVar\vC{C}
\NewObject\MyVar\vD{D}
\NewObject\MyVar\vE{E}
\NewObject\MyVar\vF{F}
\NewObject\MyVar\vG{G}
\NewObject\MyVar\vH{H}
\NewObject\MyVar\vI{I}
\NewObject\MyVar\vJ{J}
\NewObject\MyVar\vK{K}
\NewObject\MyVar\vL{L}
\NewObject\MyVar\vM{M}
\NewObject\MyVar\vN{N}
\NewObject\MyVar\vO{O}
\NewObject\MyVar\vP{P}
\NewObject\MyVar\vQ{Q}
\NewObject\MyVar\vR{R}
\NewObject\MyVar\vS{S}
\NewObject\MyVar\vT{T}
\NewObject\MyVar\vU{U}
\NewObject\MyVar\vV{V}
\NewObject\MyVar\vW{W}
\NewObject\MyVar\vX{X}
\NewObject\MyVar\vY{Y}
\NewObject\MyVar\vZ{Z}

\NewObject\MyVar\valpha{\alpha}
\NewObject\MyVar\vvaralpha{\varalpha}
\NewObject\MyVar\vbeta{\beta}
\NewObject\MyVar\vgamma{\gamma}
\NewObject\MyVar\vdelta{\delta}
\NewObject\MyVar\vepsilon{\epsilon}
\NewObject\MyVar\vvarepsilon{\varepsilon}
\NewObject\MyVar\vzeta{\zeta}
\NewObject\MyVar\veta{\eta}
\NewObject\MyVar\vtheta{\theta}
\NewObject\MyVar\viota{\iota}
\NewObject\MyVar\vkappa{\kappa}
\NewObject\MyVar\vlambda{\lambda}
\NewObject\MyVar\vmu{\mu}
\NewObject\MyVar\vnu{\nu}
\NewObject\MyVar\vxi{\xi}
\NewObject\MyVar\vpi{\pi}
\NewObject\MyVar\vvarpi{\varpi}
\NewObject\MyVar\vrho{\rho}
\NewObject\MyVar\vsigma{\sigma}
\NewObject\MyVar\vtau{\tau}
\NewObject\MyVar\vupsilon{\upsilon}
\NewObject\MyVar\vphi{\phi}
\NewObject\MyVar\vvarphi{\varphi}
\NewObject\MyVar\vchi{\chi}
\NewObject\MyVar\vpsi{\psi}
\NewObject\MyVar\vomega{\omega}

\NewObject\MyVar\vGamma{\Gamma}
\NewObject\MyVar\vDelta{\Delta}
\NewObject\MyVar\vTheta{\Theta}
\NewObject\MyVar\vLambda{\Lambda}
\NewObject\MyVar\vXi{\Xi}
\NewObject\MyVar\vPi{\Pi}
\NewObject\MyVar\vSigma{\Sigma}
\NewObject\MyVar\vUpsilon{\Upsilon}
\NewObject\MyVar\vPhi{\Phi}
\NewObject\MyVar\vPsi{\Psi}
\NewObject\MyVar\vOmega{\Omega}

\NewObject\MyVar\numZ{\mathbb{Z}}
\NewObject\MyVar\catC{\mathscr{C}}
\NewObject\MyVar\catGamma[copy=\vGamma]
\NewObject\MyVar\fibrep[copy=\vR]
\NewObject\MyVar\nerve[copy=\vN]
\NewObject\MyVar\const{\mathup{const}}
\NewObject\MyVar\simp[copy=\vDelta]
\NewObject\MyVar\point{*}
\NewObject\MyVar\vemptyset{\varnothing}
\NewObject\MyVar\Hom{\operatorname{Hom}}

\NewObject\MyVar\catsimplex{\mathbf{\Deltaup}}[
    define keys={
        {plus}{lower=+},
    },
]

\NewObject\MyVar\ordset[left par={[},right par={]}]
\NewObject\MyVar\tup{}

\NewObject\MyVar\catset{\categoryformat{Set}}
\NewObject\MyVar\catfun{\categoryformat{Fun}}
\NewObject\MyVar\catsset{\categoryformat{SSet}}

\NewVariableClass\MathOp[ % Mathematical operator
    parent=\MyVar,
    no par,
]

\NewObject\MathOp\catob{\operatorname{Ob}}

\NewObject\MathOp\catend{\int}[
    define keys={
        {rder}{ left return, symbol put left=\mathbb{R}\! },
    },
]
\NewObject\MathOp\catcoend{\int}[grading position=lower]

\NewObject\MathOp\Prod{\prod}
\NewObject\MathOp\Coprod{\coprod}

%Inverse and direct limits that look nicer:

\NewObject\MathOp\dirlim{\dirlimcommand{lim}}
\NewObject\MathOp\invlim{\invlimcommand{lim}}
\NewObject\MathOp\dirholim{\dirlimcommand{holim}}
\NewObject\MathOp\invholim{\invlimcommand{holim}}

\NewSymbolClass\MyRel
\NewObject\MyRel\iso{\cong}

\NewVariableClass\BinOp[
    define keys={
        {Lder}{upper=L},
        {Rder}{upper=R},
        {limits}{
            return,command=\mathop,inner return,symbol put right=\limits,
            math class=\mathbin,
        },
    },
    set arg dots=\dotsb,
    never par,
    prepend keys[1]={
        {arg}{
            return,
            set keys x={
                set arg sep=\SemantexDataGetExpNot{symbol},
            },
        },
    },
    parse options={
        int if greater T={ \SemantexIntGet{number of arguments} } { 0 }
        {
            symbol={},
            output=\MyVar,
        },
    },
]

\NewObject\BinOp\varpushout{\mathbin{\textstyle\coprod}}
\NewObject\BinOp\varpullback{\mathbin{\textstyle\prod}}

\NewObject\BinOp\copowering{\otimes}

\NewObject\BinOp\fibre{\times}

\NewVariableClass\InvBinOp[parent=\BinOp, set arg dots=\dotsm]

\NewObject\BinOp\mult{\cdot}
\NewObject\BinOp\comp{\circ}
\NewObject\InvBinOp\invmult{}
\NewObject\InvBinOp\invcomp{}

\makeatother

\begin{document}

\maketitle

\begin{abstract}
    \noindent We prove and explain several classical
    formulae for homotopy (co)limits
    in general (combinatorial) model categories
    which are not necessarily simplicially enriched.
    Importantly, we prove versions of the Bousfield--Kan formula and the fat totalization formula in this complete generality. We finish with a proof that homotopy-final functors
    preserve homotopy limits, again in complete generality.

    \medskip

    \scriptsize\noindent
    Keywords:
    homotopy limit, category theory, Bousfield--Kan formula,
    \\model categories, simplicial sets, derived functors

    \medskip

    \noindent MSC:
    18G55,
    18D99,
    55U35,
    18G30
\end{abstract}

\numberwithin{equation}{chapter}

\noindent If \( \catC \)~is a model category (we assume all model categories to be complete and cocomplete) and \( \catGamma \)~a (small) category,
we denote by \( \catC[diag=\catGamma] = \catfun{ \catGamma , \catC } \)
the category of functors~\( \catGamma \to \catC \), which we shall also refer to as \enquote{diagrams} of shape~\( \catGamma \).
It is natural to call a map of diagrams~\( \valpha \colon \vF \to \vG \)
in~\( \catC[diag=\catGamma] \) a \emph{weak equivalence}
if \( \valpha[\vgamma]  \colon \vF{\vgamma} \to \vG{\vgamma} \)
is a weak equivalence in~\( \catC \) for all objects~\( \vgamma \in \catGamma \).
We shall refer to such weak equivalences as \textdef{componentwise} weak equivalences.
But then we immediately run into the problem that the limit functor~\( \smash{ \invlim \colon \catC[diag=\catGamma] \to \catC } \)
does not in general preserve weak equivalences. Since \( \invlim \)~is a right adjoint, this leads us into trying to \emph{derive} it. The right derived functor of~\( \invlim \) is called the \textdef{homotopy limit} and is
denoted~\( \invholim \colon \catC[diag=\catGamma] \to \catC \).
Dually, the left derived functor of~\( \dirlim \)
is called the \textdef{homotopy colimit} and is denoted~\( \dirholim \).

For many purposes, the abstract existence of homotopy limits is all you need. However, there are also many cases where a concrete, minimalistic realization of them is useful for working with abstract notions.
For instance, this paper grew out of an attempt to concretize a concept from derived algebraic geometry. More specifically, we wanted to develop a homological algebra model for the dg-category of quasi-coherent sheaves on a dg-scheme which are equivariant with respect to the action of a group dg-scheme.
This question was addressed in~\textcite{explicit} where a partial result was obtained under serious restrictions (Proposition~13).
The general case was stated as a conjecture, see~Conjecture~1 in the same paper.
In the companion paper to this one, \textcite{comodules},
we cover the general case and prove that conjecture (see~Theorem~4.1.1), and the key result of homotopical nature is proved in the present note
(see~\cref{ex:fat_totalization}).

Quillen's model category machinery tells us how to derive the limit:
We must equip the diagram category~\( \catC[diag=\catGamma] \)
with a model structure with componentwise weak equivalences and in which the
limit functor~\( \invlim \colon \catC[diag=\catGamma] \to \catC \) is a right Quillen functor.
In this case, the derived functor is given by
\(
    \invholim{ \vF } = \invlim { \fibrep { \vF } }
\)
for some fibrant replacement~\( \fibrep { \vF } \)
in~\( \catC[diag=\catGamma,smash] \).
Indeed, such a model structure on~\( \catC[diag=\catGamma] \) exists e.g.\ if the model category~\( \catC \) is \emph{combinatorial} \parencite[see][Propositions A.2.8.2 and~A.2.8.7]{htt}.
More precisely, we have
the \textit{injective model structure}~\( \catC[diag=\catGamma,inj,smash] \)
where weak equivalences and cofibrations are calculated componentwise.

The injective model structure being in general rather complicated, calculating such a replacement of a diagram in practice becomes very involved for all but the simplest shapes of the category~\( \catGamma \). Therefore, traditionally, other tools have been used.
One of the most popular techniques involves
\emph{adding a parameter} to the limit functor~\( \invlim[\catGamma] \)
before deriving it. The result is the \emph{end}
bifunctor~\(
    \catend[\catGamma]
    \colon
    \fibre{ \catGamma[op] , \catGamma }
    \to
    \catC
\)
(introduced below) which is in general much easier to derive.

One of the classical accounts of this technique is
\textcite{hir}
who mainly works in the setting of \emph{simplicial model categories}, which are model categories enriched
over simplicial sets, and which furthermore are equipped with
a \emph{powering} functor
\[
    \fibre{ \catsset[op] , \catC }
    \longto
    \catC,
    \qquad
    \tup{ \vK , \vc }
    \longmapsto
    \vc[powering=\vK],
\]
and a \emph{copowering} functor
\[
    \fibre{ \catsset , \catC }
    \longto
    \catC,
    \qquad
    \tup{ \vK , \vc }
    \longmapsto
    \copowering{ \vK , \vc },
\]
satisfying
some compatibility relations with the model structure.
He then establishes the classical \textdef{Bousfield--Kan formula}
\begin{equation}\label{eq:bousfield_kan}
    \invholim { \vF }
    =
    \catend[ \vgamma\in\catGamma ]{
        \vF{\vgamma}[powering=\nerve{\catGamma[comma category=\vgamma]}]
    }
    ,
\end{equation}
where we write~\( \nerve{ \catGamma[comma category=\vgamma] } \) for the
nerve of the comma category of maps in~\( \catGamma \)
with codomain~\( \vgamma \).
Or rather, he uses this formula as his \emph{definition}
of homotopy limits (see~definition~18.1.8).
A proof that this formula agrees with the general
definition of homotopy limits is due to
\textcite[equation~(2)]{gambino_simplicial}
using the machinery of Quillen 2-functors.

\citeauthor{hir} then generalizes this formula to arbitrary model categories in chapter~19, definition~19.1.5.
He shows that even for non-simplicial model categories,
one can replace simplicial
powerings and copowerings by a weaker notion,
unique up to homotopy in a certain sense.
He then again takes the formula~\eqref{eq:bousfield_kan}
to be his \emph{definition} of a homotopy limit.

This paper is devoted to proving (see~\cref{res:bousfield_kan}) that indeed, the formula~\eqref{eq:bousfield_kan} agrees with the general definition of a homotopy limit
(similarly to what \citeauthor{gambino_simplicial}
did in the simplicial setting), at
least in the case when the model category~\( \catC \)
is \emph{combinatorial}.
(This assumption is not a great problem since combinatoriality is what provides us with a model structure on the category~\( \catC[diag=\catGamma] \) in the first place, which is what guarantees that homotopy limits as we defined them above make sense).
To the authors' knowledge, such a proof has not been carried out in the
literature before.
Finally, in \cref{sec:homotopy-initial}, we discuss preservation of homotopy limits by homotopy-initial functors, observing why this classical property also can be proved using our machinery.
As an application, we obtain the classical and fundamental fat totalization formula in the previously mentioned~\cref{ex:fat_totalization}.
There is, of course, a dual result for coends.

\chapter{The projective and injective model structures}

If \( \catC \)~is a model category and \( \catGamma \)~any category, it is natural to demand of any model structure on the functor category
\(
    \catC[diag=\catGamma]
    = \catfun{ \catGamma , \catC }
\)
that weak equivalences must be calculated componentwise.
The two most natural model structures one can hope for (which may or may not exist) are
\begin{itemize}
    \item The \textdef{projective model structure}~%
    \( \catC[diag=\catGamma,proj] \)
    where weak equivalences and fibrations are calculated componentwise.
    \item The \textdef{injective model structure}~%
    \( \catC[diag=\catGamma,inj] \)
    where weak equivalences and cofibrations are calculated componentwise.
\end{itemize}
Both model structures are known to exist when \( \catC \)~is a \emph{combinatorial} model category, see
\textcite[Proposition~A.2.8.2]{htt}.
We shall also use the attributes \textquote{projective(ly)} and \textquote{injective(ly)} when referring to these model structures, so e.g.~\textquote{projectively cofibrant} means cofibrant in the projective model structure.

\begin{propositionbreak}[Proposition {\parencite[Proposition~A.2.8.7]{htt}}]%
    \label{res:Kan_extensions_Quillen_adjunctions}
    If \( \catC \)~is a model category and \( \vf \colon \catGamma\to\catGamma[prime] \) a functor,
    denote by~\( \vf[*res] \) the restriction functor
    \(\smash{
        \catC[diag={\catGamma[prime]}]
        \to
        \catC[diag={\catGamma}]
    }\).
    Then \( \vf[*res] \)~fits as the right and left adjoint of Quillen adjunctions
    \[
    \begin{tikzcd}[sep=scriptsize]
        \vf[!kan]
        \colon
        \catC[diag=\catGamma,proj]
        \ar[r,yshift=1.5pt]
        &
        \ar[l,yshift=-1.5pt]
        \catC[diag=\catGamma[prime],proj]
        \noloc
        \vf[*res]
    \end{tikzcd}
        \qquad\text{resp.}\qquad
    \begin{tikzcd}[sep=scriptsize]
        \vf[*res]
        \colon
        \catC[diag=\catGamma[prime],inj]
        \ar[r,yshift=1.5pt]
        &
        \ar[l,yshift=-1.5pt]
        \catC[diag=\catGamma,inj]
        \noloc
        \vf[*kan]
    \end{tikzcd}
    \]
    whenever the model structures in question exist.
    In particular, the adjunctions
    \(\smash{
        \dirlim
        \colon
        \catC[diag=\catGamma,proj]
        \rightleftarrows
        \catC
        \noloc
        \const
    }\)
    and
    \(\smash{
        \const
        \colon
        \catC
        \rightleftarrows
        \catC[diag=\catGamma,inj]
        \noloc
        \invlim
    }\)
    are Quillen adjunctions.
\end{propositionbreak}

The adjoints \( \vf[!kan] \) and~\( \vf[*kan] \) are the usual \textdef[left Kan extension]{left} and \textdef[right Kan extension]{right Kan extensions} along~\( \vf \), which are given by
limits
\begin{equation}\label{eq:kan_extensions}
    \vf[!kan]{ \vF }{ \vgamma[prime] }
    =
    \dirlim[ \vf{\vgamma}\to\vgamma[prime] ]{ \vF{\vgamma} }
    \qquad\text{and}\qquad
    \vf[*kan]{ \vF }{ \vgamma[prime] }
    =
    \invlim[ \vgamma[prime]\to\vf{\vgamma} ]{ \vF{\vgamma} }
    .
\end{equation}
These limits are taken over the categories of maps~\( \vf{\vgamma} \to \vgamma[prime] \) (resp.~\( \vgamma[prime] \to \vf{\vgamma} \))
in~\( \catGamma[prime] \)
for varying~\( \vgamma \in \catGamma \).

\begin{corollary}
    Assume that the projective model structure~\( \catC[diag=\catGamma,proj,smash] \) exists.
    \begin{corollarylist}
        \item\label{res:simple_cofibrations}
        If \( \vvarphi \colon \vc \to \vc[prime] \) is a (trivial) cofibration in~\( \catC \) and~\( \vgamma[0] \in \catGamma \) is an object, then the coproduct map
        \(
            \Coprod[\catGamma{ \vgamma[0] ,\slot }]{ \vvarphi }
            \colon
            \Coprod[\catGamma{ \vgamma[0] ,\slot }]{ \vc }
            \to
            \Coprod[\catGamma{ \vgamma[0] ,\slot }]{ \vc[prime] }
        \)
        is a (trivial) cofibration in~%
        \( \catC[diag=\catGamma,proj,smash] \).
        We shall refer to such (trivial) cofibrations as \textdef[simple (trivial) projective cofibration]{simple projective cofibrations}\index{cofibration!projective!simple}.
        \item\label{res:preserve_simple_cofibrations}
        If \( \vf \colon \catGamma \to \catGamma[prime] \)~is a functor, then
        \(
            \vf[!kan]
            \colon
            \catC[diag={\catGamma},proj]
            \to
            \catC[diag={\catGamma[prime]},proj]
        \)
        preserves simple (trivial) projective cofibrations,
        taking \( \Coprod[\catGamma{ \vgamma[0] ,\slot }]{ \vvarphi } \)
        to~%
        \( \Coprod[ \catGamma[prime]{ \vf { \vgamma[0] } ,\slot } ]{ \vvarphi } \).
    \end{corollarylist}
\end{corollary}

In fact, what we call the simple (trivial) cofibrations form a generating set
for the model category~\( \catC[diag=\catGamma,proj,smash] \), whereas
the situation is more complicated for~\( \catC[diag=\catGamma,inj,smash] \), see \textcite[Proposition~A.2.8.2]{htt}.

\begin{proof}
    Applying~\cref{res:Kan_extensions_Quillen_adjunctions} to the
    embedding~\( \viota \colon \vgamma[0] \into \catGamma \) of the full subcategory with~\( \vgamma[0] \) as the only object,
    we get that \( \viota[!kan]{ \vvarphi } \)~is a (trivial) cofibration.
    Now
    \(
        \viota[!kan]{ \vvarphi }
        =
        \Coprod[ \catGamma { \vgamma[0],\slot }, smash ]{ \vvarphi }
    \)
    by the above colimit formula for left Kan extension.
    The statement~\localref{res:preserve_simple_cofibrations}
    follows
    by applying Kan extensions to the diagram
    \[\begin{tikzcd}[sep=small]
        \vgamma[0] \ar[r,hook] \ar[d]   & \catGamma \ar[d,"\vf"]
    \\
        \vf { \vgamma[0] } \ar[r,hook]  & \catGamma[prime]
    \end{tikzcd}\]
    and using that Kan extensions, being adjoints to restriction, respect compositions.
\end{proof}

\chapter{The Reedy model structure}

A third approach exists to equip diagram categories~\( \catC[diag=\catGamma] \) with a model structure, provided the category~\( \catGamma \) has the structure of a \emph{Reedy} category.
A category~\( \catGamma \) is called \textdef{Reedy} if it contains two subcategories
\( \catGamma[reedy+] , \catGamma[reedy-] \subset \catGamma \),
each containing all objects, such that
\begin{itemize}
    \item there exists a degree function
    \( \catob{\catGamma} \to \numZ \),
    such that non-identity morphisms from~\( \catGamma[reedy+] \) strictly raise the degree
    and non-identity morphisms from~\( \catGamma[reedy-] \) strictly lower the degree (more generally, an ordinal number can be used instead of~\( \numZ \));
    \item each morphism \( \vf \in \catGamma \) factors \emph{uniquely} as \( \vf = \invcomp{ \vg , \vh } \) for \( \vg \in \catGamma[reedy+] \) and
    \( \vh \in \catGamma[reedy-] \).
\end{itemize}

We note that a direct category is Reedy with
\( \catGamma[reedy+] = \catGamma \),
and that an inverse category is Reedy with
\( \catGamma[reedy-] = \catGamma \).
If \( \catGamma \)~is Reedy, then so is~\( \catGamma[op] \),
with
\( \catGamma[op,spar,reedy+] = \catGamma[reedy-,spar,op] \)
and
\( \catGamma[op,spar,reedy-] = \catGamma[reedy+,spar,op] \).

\begin{example}\label{ex:delta_reedy}
    The simplex category~\( \catsimplex \) is Reedy with~\( \catsimplex[reedy+] \) consisting of injective maps and \( \catsimplex[reedy-] \)~consisting of surjective maps.
    The degree function does the obvious thing,
    \( \ordset{\vn} \mapsto \vn \).
\end{example}

If \( \catGamma \)~is a Reedy category and \( \catC \)~is any model category, and if \( \vF \in \catC[diag=\catGamma] \)~is a diagram, we define the \textdef[latching object]{latching} and \textdef[matching object]{matching objects} by
\[
    \vF[latching=\vgamma]
    = \dirlim[
            \MyVar{
                \valpha\underset{\smash{\neq}}{ \to }\vgamma
            }[spar]
            \in
            \catGamma[reedy+]
        ]{ \vF { \valpha } }
\qquad\text{and}\qquad
    \vF[matching=\vgamma]
    = \invlim[
            \MyVar{
                \vgamma\underset{\smash{\neq}}{\to}\valpha
            }[spar]
            \in
            \catGamma[reedy-]
        ]{ \vF { \valpha } }.
\]
In other words, the limit (resp.,\ colimit) runs over the category of all \emph{non-identity} maps \( \valpha \to \vgamma \) in~\( \catGamma[reedy+] \) (resp.,\ \( \vgamma \to \valpha \) in~\( \catGamma[reedy-] \)).
The \textdef{latching map} is the canonical map
\( \vF[latching=\vgamma,smash] \to \vF{\vgamma} \),
and the \textdef{matching map} is the canonical map
\( \vF{\vgamma} \to \vF[matching=\vgamma,smash] \).

If \( \vf \colon \vF \to \vG \) is a map in~\( \catC[diag=\catGamma] \), then the \textdef{relative latching map}
and the \textdef{relative matching map} are the maps
\[
    \vF { \vgamma }
    \varpushout[ limits, \vF[{latching=\vgamma}] ]
    \vG[latching=\vgamma]
    \longto
    \vG { \vgamma }
    \qquad\text{resp.}\qquad
    \vF { \vgamma }
    \longto
    \vG { \vgamma }
    \varpullback[ limits, \vG[{matching=\vgamma}] ]
    \vF[matching=\vgamma]
\]
given by the universal property of the pushout resp.~pullback. We say that \( \vf \)~is a \textdef{(trivial) Reedy cofibration} (resp.~\textdef{fibration}) if the relative latching map is a (trivial) cofibration (resp.~fibration) in~\( \catC \).
If \( \vF = \vemptyset \) (resp.~\( \vF = \point \)), we recover the latching (resp.~matching) map.
For our arbitrary model category~\( \catC \), this defines a model structure on~\( \catC[diag=\catGamma,smash] \), called the \textdef{Reedy model structure}, see
\textcite[Theorem~15.3.4]{hir}.
The weak equivalences are componentwise weak equivalences.
We shall write~\( \catC[diag=\catGamma,reedy,smash] \) when we equip the diagram category with this model structure.

\chapter{Homotopy limits}

Let \( \catGamma \) and~\( \catC \) be categories, \( \catC \)~complete and cocomplete, and let~\( \vH \colon \fibre{ \catGamma[op] , \catGamma } \to \catC \) a bifunctor. The \textdef{end} of~\( \vH \) is an object
\( \smash{
    \catend[\catGamma]{ \vH } = \catend[\vgamma \in \catGamma]{ \vH { \vgamma , \vgamma } }
    }
\)
in~\( \catC \), together with morphisms~\(
    \catend[\catGamma]{ \vH }
    \to
    \vH { \vgamma , \vgamma }
\) for all~\( \vgamma \in \catGamma \), such that for any~\( \vf \colon \vgamma \to \vgamma[prime] \), the following diagram commutes:
\begin{equation*}
\begin{tikzcd}
    \catend[\catGamma]{ \vH } \ar[r] \ar[d]
            & \vH { \vgamma , \vgamma } \ar[d, "{\vH { \vgamma , \vf }}"]
\\
    \vH { \vgamma[prime] , \vgamma[prime] } \ar[r, "{\vH { \vf , \vgamma[prime] }}"']
            & \vH { \vgamma , \vgamma[prime] }
            \invdot
\end{tikzcd}
\end{equation*}
Furthermore, \( \catend[\catGamma]{ \vH } \)~is universal with this property in the sense that if \( \vA \)~is another object of~\( \catC \) with a collection of arrows~\( \vA \to \vH { \vgamma , \vgamma } \) for all~\( \vgamma \), subject to the same commutativity conditions, then these factor through a unique arrow~\( \smash{\vA\to \catend[\catGamma]{ \vH } } \).
There is a dual notion of a \emph{coend}, denoted instead by~\(\smash{ \catcoend[\catGamma]{ \vH } } \), which we shall not spell out.

\begin{remark}
    A diagram~\( \vF \in \catC[diag=\catGamma] \) may be regarded as a diagram in~\( \catC[diag=\fibre{\catGamma[op],\catGamma}] \) which is
    constant with respect to the first variable. In that case, it follows from the universal property of the end that
    \( \catend[\catGamma]{ \vF } = \invlim[\catGamma]{ \vF } \)
    recovers the limit of the diagram.
\end{remark}

\begin{remark}\label{res:end_adjunction}
    The end fits as the right adjoint of the adjunction
    \[\begin{tikzcd}[sep=scriptsize]
        \Coprod[ \Hom[\catGamma] ]
        \colon
        \catC \ar[r, yshift=1.5pt]
            & \catC[diag=\fibre{\catGamma[op],\catGamma}]
            \ar[l,yshift=-1.5pt]
            \noloc
            \catend[\catGamma]\invdot
    \end{tikzcd}\]
    The left adjoint takes~\( \vA \in \catC \) to the bifunctor
    \( \Coprod[ \Hom[\catGamma]{\slot ,\slot } ]{ \vA } \colon \fibre{\catGamma[op],\catGamma}\to\catC \).
    In the literature, this is usually written as an adjunction
    \[
        \catset[diag=\fibre{\catGamma[op],\catGamma},par=\big]{
            \Hom[\catGamma] ,
            \catC { \vA , \vF }
        }
        \iso
        \catC[diag=\fibre{\catGamma[op],\catGamma},par=\big]{
            \vA , \textstyle \catend[\catGamma]{ \vF }
        }
    \]
    for \( \vA \in \catC \), which is just the well-known statemant that the end is the
    \emph{weighted limit}~\(
        \catC[diag=\fibre{\catGamma[op],\catGamma}]
        \to
        \catC
    \)
    with weight~\( \Hom[\catGamma] \).
\end{remark}

The following theorem is the basis for all our homotopy limit
formulae:

\begin{theorem}\label{res:end_functor_quillen}
    Let~\( \catC \) be a model category and~\( \catGamma \) a category. Regard the functor category~\( \catC[diag=\fibre{\catGamma[op],\catGamma}] \) as a model category in any of the following ways:
    \begin{theoremlist}
        \item\label{res:end_functor_quillen_gammaop_gamma} as~\(
            \catC[diag=\fibre{\catGamma[op],\catGamma}]
            = \catC[
                diag=\catGamma[op],
                proj,
                spar,
                diag=\catGamma,
                inj,
            ]
        \)
        (assuming this model structure exists);
        \item\label{res:end_functor_quillen_gamma_gammaop} as~\(
            \catC[diag=\fibre{\catGamma[op],\catGamma}]
            = \catC[
                diag=\catGamma,
                proj,
                spar,
                diag=\catGamma[op],
                inj,
            ]
        \)
        (assuming this model structure exists);
        \item\label{res:end_functor_quillen_reedy} as~\(
            \catC[diag=\fibre{\catGamma[op],\catGamma}]
            = \catC[
                diag=\fibre{\catGamma[op],\catGamma},
                reedy,
            ]
        \)
        (assuming \( \catGamma \)~is Reedy).
    \end{theoremlist}
    Then the end functor~\(
        \catend[\catGamma]
        \colon
        \catC[diag=\fibre{\catGamma[op],\catGamma}]
        \to
        \catC
    \)
    is right Quillen.
\end{theorem}

\begin{proof}
    We initially prove the first statement, the second one being dual.
    By \cref{res:end_adjunction}, it suffices to check that the left
    adjoint~\( \Coprod[ \Hom[\catGamma] ] \)
    takes (trivial) cofibations in~\( \catC \) to (trivial) cofibations in~\(
        \catC[
            diag=\catGamma[op],
            proj,
            spar,
            diag=\catGamma,
            inj,
            smash,
        ]
    \).
    If \( \vc \to \vc[prime] \)~is a (trivial) cofibration in~\( \catC \), then
    we must therefore consider the map~\(
        \Coprod [ \catGamma {\slot ,\slot } ]{ \vc }
        \to
        \Coprod [ \catGamma {\slot ,\slot } ]{ \vc[prime] }
    \)
    in~\(
        \catC[
            diag=\catGamma[op],
            proj,
            spar,
            diag=\catGamma,
            inj,
            smash,
        ]
    \).
    Checking that this is a (trivial) injective cofibration
    over~\( \catGamma \)
    amounts, by definition, to checking this componentwise. But for a fixed~\( \vgamma[0] \in\catGamma \), this component is
    \(
        \Coprod[ \catGamma{\slot , \vgamma[0] } ]{ \vc }
        \to
        \Coprod[ \catGamma{\slot , \vgamma[0] } ]{ \vc[prime] },
    \)
    which is a simple (trivial) projective cofibration
    in~\( \catC[diag=\catGamma[op],smash] \).

    For the Reedy case, we recall from
    \textcite[Example~A.2.9.22]{htt}
    and \textcite[Theorem~15.5.2]{hir}
    that being a (trivial) cofibration in the model category~\(
        \catC[diag=\fibre{\catGamma,\catGamma[op]},reedy,smash]
        = \catC[diag=\catGamma,reedy,spar,diag=\catGamma[op],reedy,smash]
    \)
    is equivalent to the restriction being a (trivial) cofibration
    in
    \[
        \catC[
            diag={\catGamma[reedy+]},proj,
            spar=\big,smash,
            diag={\catGamma[op,spar,reedy+]},proj,
        ]
        =
        \catC[
            diag={\catGamma[reedy+]},proj,
            spar=\big,smash,
            diag={\catGamma[reedy-,spar,op]},proj,
        ].
    \]
    But we have, by the unique factorization property of Reedy categories, that
    \[
        \Coprod[ \catGamma{ \slot ,\slot } ]{ \vc }
        = \Coprod[ \vgamma[0] \in \catGamma ]{
            \Coprod [ \catGamma[reedy-] {\slot , \vgamma[0] } ]{
                \Coprod [ \catGamma[reedy+] { \vgamma[0] ,\slot } ]{ \vc }
            }
        }
    \]
    for any~\( \vc\in\catC \).
    These consist of coproducts of exactly the same form as the ones appearing in the definition of simple (trivial) projective cofibrations
    (\cref{res:simple_cofibrations}).
    Thus we find that for any (trivial) cofibration~\( \vc\to\vc[prime] \) in~\( \catC \),
    the map~\(
        \Coprod[ \catGamma {\slot ,\slot } ]{ \vc }
        \to
        \Coprod[ \catGamma {\slot ,\slot } ]{ \vc[prime] }
    \)
    is a (trivial) cofibration
    in~\( \catC[diag=\fibre{\catGamma[op],\catGamma},reedy,smash] \).
\end{proof}

Thus we can derive the end using any of these three model structures, when available.
Write~\(
    \catend[rder,\catGamma]
    \colon
    \catC[diag=\fibre{\catGamma[op],\catGamma}]
    \to
    \catC
\)
for the derived functor, which we shall call the \textdef{homotopy end}.

\begin{corollary}\label{res:homotopy_limits_via_ends}
    If \( \catC \)~is a combinatorial model category and \( \catGamma \)~a category, then for a diagram~\( \vF \in \catC[diag=\catGamma] \),
    \[\textstyle
        \invholim[\catGamma]{ \vF }
        = \catend[rder,\catGamma]{ \vF }
        = \catend [ \catGamma]{ \fibrep{ \vF } }
        ,
    \]
    where \( \fibrep \)~is a fibrant replacement with respect to the model structure~\(
        \catC[diag=\catGamma,proj,spar,diag=\catGamma[op],inj,smash]
    \)
    or, if \( \catGamma \)~is Reedy,
    in~\(
        \catC[diag=\fibre{\catGamma[op],\catGamma},reedy,smash]
    \).
\end{corollary}

\begin{proof}
    First write
    \(
        \invholim { \vF }
        =
        \invlim { \fibrep[\catGamma]{ \vF } }
    \)
    for some fibrant replacement functor~\( \fibrep[\catGamma] \)
    in~\( \catC[diag=\catGamma,inj,smash] \).
    Now \cref{res:Kan_extensions_Quillen_adjunctions}
    and~\textcite[Remark~A.2.8.6]{htt} show that the constant functor embedding~\(
        \catC[diag=\catGamma,inj,smash]
        \into
        \catC[diag=\catGamma[op],proj,spar,diag=\catGamma,inj,smash]
    \)
    is right Quillen and thus preserves fibrant objects.
    Thus \( \fibrep[\catGamma]{ \vF } \)~is also fibrant
    in~\( \catC[diag=\catGamma[op],proj,spar,diag=\catGamma,inj,smash] \).
    This proves the first equality sign. The second one is clear.
\end{proof}

Of course, even though \( \vF \) as a diagram in~\( \catC[diag=\fibre{\catGamma[op],\catGamma}] \) was constant with respect to the first variable, \( \fibrep{ \vF } \) is in general not. Remarkably, since ends calculate naturality between the two variables, this often makes calculations of homotopy limits more manageable, compared to resolving the diagram inside~\( \catC[diag=\catGamma,inj,smash] \).

\begin{corollary}\label{res:holim_direct_category}
    Suppose \( \catGamma \)~is a direct category,
    and let~\(
        \smash{
            \fibrep
            \colon
            \catC
            \to
            \catC[diag=\catGamma[op],inj]
        }
    \)
    be a functor that takes~\( \vc\in\catC \) to a fibrant replacement of the constant diagram at~\( \vc \).
    Then
    \[\textstyle
        \invholim[\catGamma]{ \vF }
        =
        \catend[\vgamma\in\catGamma]{
            \fibrep{ \vF{\vgamma} }{\vgamma}
        }.
    \]
\end{corollary}

\begin{proof}
    Clearly, \( \fibrep{ \vF } \)~is a
    fibrant replacement
    inside~\(
        \catC[
            diag=\catGamma[op],
            inj,
            spar,
            diag=\catGamma,
            proj,
            smash,
        ]
    \).
    By  \textcite[Example~A.2.9.22]{htt}
    and \textcite[Theorem~15.5.2]{hir},
    this model category is equal
    to
    \[
        \catC[
            diag=\catGamma[op],
            inj,
            spar=\big,
            smash,
            diag=\catGamma,
            proj,
        ]
        =
        \catC[
            diag=\catGamma[op],
            reedy,
            spar=\big,
            smash,
            diag=\catGamma,
            reedy,
        ]
        =
        \catC[
            diag=\catGamma,
            reedy,
            spar=\big,
            smash,
            diag=\catGamma[op],
            reedy,
        ]
        =
        \catC[
            diag=\catGamma,
            proj,
            spar=\big,
            smash,
            diag=\catGamma[op],
            inj,
        ]
    ,
    \]
    so the result follows from~\cref{res:end_functor_quillen}.
\end{proof}

\chapter{Bousfield--Kan formula}

In \textcite[chapter~19]{hir}, homotopy limits are being developed
for arbitrary model categories via a machinery of simplicial resolutions. In this section, we use \cref{res:end_functor_quillen}/\cref{res:homotopy_limits_via_ends} to explain why this machinery works.
Throughout, we denote by~\( \catsset \)
the category of simplicial sets endowed with the Quillen model structure.

If \( \catC \)~is a (complete) category and~\( \vX[simp *] \in \catC[diag=\catsimplex[op]] \)
a simplicial diagram in~\( \catC \), we may extend~\( \vX[simp *] \)
to a continuous functor~\( \vX \colon \catsset[op] \to \catC \)
via the right Kan extension
along
the Yoneda embedding~\(
    \catsimplex[op] \into \catsset[op]
\):
\[
    \vX[powering=\vK]
    =
    \invlim[\simp[{d=\vn}]\to\vK]{ \vX[simp=\vn] },
    \qquad
    \vK\in\catsset.
\]
If \( \catC \)~is a model category, the matching object at~\( \ordset{\vn} \)
is~\( \vX[simp *,matching=\vn] = \vX[powering=\simp[{d=\vn}][boundary]] \),
and so \( \vX[simp *] \)~being Reedy-fibrant
is equivalent
to the map~\(\smash{
    \vX[{simp=\vn}]
    =
    \vX[powering=\simp[{d=\vn}]]
    \to
    \vX[powering=\simp[{d=\vn}][boundary]]
}\)
being a fibration in~\( \catC \) for all~\( \vn \).

We need the following technical lemma:

\begin{lemmabreak}[{{Lemma \parencite[Proposition~3.6.8]{hovey}}}]\label{res:hovey_lemma}
    Let~\( \catC \) be a model category
    and \( \vF \colon \catsset \to \catC \) a functor preserving colimits and cofibrations. Then \( \vF \)~preserves trivial cofibrations if and only if \( \smash{ \vF{\simp[d=\vn]} \to \vF{\simp[d=0]} } \)~is a weak equivalence for all~\( \vn \).
\end{lemmabreak}

\begin{theorem}[Theorem (Bousfield--Kan formula)]\label{res:bousfield_kan}
    Suppose \( \catC \)~is a combinatorial model category,~\( \catGamma \)
    a category, and~\( \vF \in \catC[diag=\catGamma] \).
    Let~\(
        \fibrep
        \colon
        \catC
        \to
        \catC[diag=\catsimplex[op],smash]
    \)
    be a functor that takes~\( \vc \in \catC \)
    to a Reedy-fibrant replacement of the constant \( \catsimplex[op] \)-diagram at~\( \vc \).
    Let furthermore~\( \vK \in \catsset[diag=\catGamma,proj,smash] \)
    be a projectively cofibrant resolution of the point.
    Then
    \[
        {\textstyle\invholim[\catGamma]{ \vF }}
        =
        \catend[\vgamma\in\catGamma]{
            \fibrep{\vF{\vgamma}}[
                powering={\vK[arg=\vgamma]},
            ]
        }.
    \]
\end{theorem}

\begin{proof}
    Clearly,
    \( \smash{ \fibrep{ \vF{\slot} }[simp *] } \)~is a fibrant replacement
    of~\( \vF \)
    with respect to the model structure~\(
        \catC[
            diag=\catsimplex[op],
            reedy,
            spar,
            diag=\catGamma,
            proj,
            smash,
        ]
    \).
    The theorem will follow if we prove that
    \( \fibrep{ \vF{\slot} }[powering={\vK[arg=\slot]}] \)~is
    a fibrant replacements of~\( \vF \)
    in~\(
        \catC[
            diag=\catGamma,
            proj,
            spar,
            diag=\catGamma[op],
            inj,
            smash,
        ]
    \).
    This will follow from Ken Brown's Lemma if we prove
    that the continuous functor
    \[
        \catsset[diag=\catGamma,proj,spar=\big,op]
        \longto
        \catC[diag=\catGamma,proj,spar=\big,smash,diag=\catGamma[op],inj],
        \qquad
        \vK[arg=\slot]
        \longmapsto
        \fibrep{ \vF{\slot} }[powering={\vK[arg=\slot]}]
        ,
    \]
    takes opposites of (trivial) cofibrations to (trivial) fibrations.
    (Trivial) cofibrations
    in~\( \catsset[diag=\catGamma,proj,smash] \)
    are generated from \emph{simple} (trivial) projective
    cofibrations via pushouts and retracts, c.f.~\textcite[Proposition~A.2.8.2]{htt}. Thus by continuity of the functor,
    it suffices to prove the statement for \emph{simple} (trivial) cofibrations.
    We therefore let \(
        \Coprod[\catGamma{\vgamma[0],\slot}]{ \vK }
        \into
        \Coprod[\catGamma{\vgamma[0],\slot}]{ \vL }
    \)~be one such, where \( \vK\into\vL \)
    is a (trivial) cofibration and~\( \vgamma[0] \in \catGamma \).
    This is mapped to
    \[\textstyle
        \Prod[\catGamma{\vgamma[0],\slot}]{
            \fibrep{\vF{\slot}}[powering=\vL]
        }
        \to
        \Prod[\catGamma{\vgamma[0],\slot}]{
            \fibrep{\vF{\slot}}[powering=\vK]
        }.
    \]
    Thus we must show that the composition
    \[
        \catsset[op]
        \xrightarrow{\Prod[\catGamma{\vgamma[0],\slot}]}
        \catsset[diag=\catGamma[op],proj,spar=\big,op]
        \longto
        \catC[diag=\catGamma,proj,spar=\big,smash,diag=\catGamma[op],inj],
        \qquad
        \textstyle
        \vK
        \longmapsto
        \Prod[\catGamma{\vgamma[0],\slot}]{
            \fibrep{ \vF{\slot} }[powering={\vK}]
        },
    \]
    takes (trivial) cofibrations to (trivial) fibrations.
    Checking that it takes cofibrations to fibrations amounts to checking this for the generating cofibrations~\( \simp[d=\vn][boundary]\into\simp[d=\vn] \) in~\( \catsset \). This holds by the assumption that \( \fibrep{\vF{\slot}}[simp *] \) is componentwise Reedy-fibrant.
    Since the functor takes colimits to limits,
    the claim now follows from the (dual of) the lemma.
\end{proof}

\begin{remark}
    One may prove
    \parencite[see e.g.][Proposition~14.8.9]{hir}
    that the diagram~\( \vK{ \slot } = \nerve{ \catGamma[comma category=\slot] } \in \catsset[diag=\catGamma,proj,smash] \),
    taking~\( \vgamma \)
    to the nerve~\( \nerve{ \catGamma[comma category=\vgamma] } \)
    of the comma category~\( \catGamma[comma category=\vgamma] \) of all maps in~\( \catGamma \) with codomain~\( \vgamma \),
    is a projectively cofibrant resolution of the point. Thus we have
    \begin{equation}\label{eq:classical_bousfield_kan}
        {\textstyle\invholim[\catGamma]{ \vF }}
        =
        \catend[\vgamma\in\catGamma]{
            \fibrep{\vF{\vgamma}}[
                powering={\nerve{ \catGamma[comma category=\vgamma] }},
            ]
        },
    \end{equation}
    which is the classical form of the Bousfield--Kan formula~\eqref{eq:bousfield_kan}.
\end{remark}

\chapter{Homotopy-initial functors}\label{sec:homotopy-initial}

A functor~\( \vf \colon \catGamma \to \catGamma[prime] \)
is called \textdef{homotopy-initial} if for all objects~\( \vgamma[prime] \in \catGamma[prime] \),
the nerve~\( \nerve{ \vf[comma category=\vgamma[prime]] } \)
is contractible as a simplicial set;
here \( \vf[comma category=\vgamma[prime]] \) denotes the comma category whose objects are pairs~\( \tup{ \vgamma , \valpha } \)
where \( \valpha \) is a
map~\( \vf{ \vgamma } \to \vgamma[prime] \).
A morphism~\(
    \tup{ \vgamma[1] , \valpha }
    \to
    \tup{ \vgamma[2] , \valpha }
\)
is a morphism~\( \vgamma[1] \to \vgamma[2] \)
in~\( \catGamma \) making the diagram
\[\begin{tikzcd}[row sep=0em]
    \vf{\vgamma[1]}
    \ar[dd] \ar[rd]
\\
        & \vgamma[prime]
\\
    \vf{\vgamma[2]} \ar[ru]
\end{tikzcd}\]
commute. We aim to reprove, using our more modern language, the statement that homotopy-initial functors preserve homotopy limits.
This relies on a few technical lemmas:

\begin{lemma}\label{res:kan_extension_nerve}
    If \( \vf \colon \catGamma \to \catGamma[prime] \)
    is a functor, then~\(
        \vf[!kan]{ \nerve{ \catGamma[comma category=\slot] } }
        =
        \nerve{ \vf[comma category=\slot] }
        \in
        \catsset[diag=\catGamma[prime]]
    \).
    In particular,
    since \(
        \nerve{ \catGamma[comma category=\slot] }
        \in
        \catsset[diag=\catGamma,proj,smash]
    \)
    is cofibrant,
    \(
        \nerve{ \vf[comma category=\slot] }
        \in
        \catsset[diag=\catGamma[prime],proj,smash]
    \)
    is cofibrant
    by \cref{res:Kan_extensions_Quillen_adjunctions}.
\end{lemma}

\begin{proof}
    Since colimits in diagram categories
    over cocomplete categories can be checked componentwise,
    this boils down to the observation
    \[
        \dirlim[ \vf{\vgamma} \to \vgamma[prime] ]{
            \nerve{ \catGamma[comma category=\vgamma] }[simp=\vn]
        }
        =
        \nerve{ \vf[comma category=\vgamma[prime]] }[simp=\vn]
        .
    \]
\end{proof}

The following lemma is inspired
by \textcite[Proposition~19.6.6]{hir}.
See also \textcite[Lemma~8.1.4]{riehl}.

\begin{lemmabreak}\label{res:change_of_diagrams}
    Suppose that \( \catC \)
    is a complete category and that \( \catGamma \)
    and~\( \catGamma[prime] \) are two categories
    with a functor~\( \vf \colon \catGamma \to \catGamma[prime] \).
    Then
    we have
    \[
        \catend[\vgamma\in\catGamma]{
            \vF{\vf{\vgamma}}[powering=\nerve{\catGamma[comma category=\vgamma]}]
        }
        =
        \catend[\vgamma[prime]\in\catGamma[prime]]{
            \vF{\vgamma[prime]}[powering=
                \nerve{ \vf[comma category=\vgamma[prime]] }
            ]
        }
    \]
    for~\( \vF \in \catC[diag=\catsimplex[op],spar,smash,diag=\catGamma] \)
    (see the previous chapter for an explanation of the
    power notation).
\end{lemmabreak}

\begin{proof}
    For the purpose of the proof, we recall
    that the Kan extension formulas
    in~\eqref{eq:kan_extensions} may
    be equivalently written in terms of (co)ends:
    \[
        \vf[!kan]{\vF}{\vgamma[prime]}
        =
        \catcoend[\vgamma\in\catGamma]{
            \fibre{
                \catGamma[prime]{\vf{\vgamma},\vgamma[prime]} ,
                \vF{\vgamma}
            }
        }
        \qquad\text{and}\qquad
        \vf[*kan]{\vF}{\vgamma[prime]}
        =
        \catend[\vgamma\in\catGamma]{
            \vF{\vgamma}[powering=\catGamma[prime]{\vgamma[prime],\vf{\vgamma}}]
        }
        .
    \]
    Here we are using the natural copowering and powering of~\( \catset \) on~\( \catC \),
    given by~\( \copowering{ \vS , \vc } = \Coprod[\vS]{\vc} \)
    and~\( \vc[powering=\vS] = \Prod[\vS]{\vc} \)
    for~\( \vS \in \catset \) and~\( \vc \in \catC \),
    which make sense whenever \( \catC \)
    is complete resp.~cocomplete.
    We shall furthermore make use of the
    so-called
    \enquote{co-Yoneda lemma} which says that
    \[
        \vG{\vf{\vgamma}}
        =
        \catend[\vgamma[prime]\in\catGamma[prime]]{
            \vG{\vgamma[prime]}[
                powering=\catGamma[prime]{\vf{\vgamma},\vgamma[prime]}
            ]
        }
        \qquad
        \text{for all }
        \vG \in \catC[diag=\catGamma[prime]]
        .
    \]
    Finally, we use \enquote{Fubini's theorem} for ends,
    which says that ends, being limits, commute.
    This together yields
    \begin{align*}
        \catend[\vgamma\in\catGamma]{
            \vF{\vf{\vgamma}}[powering=\nerve{\catGamma[comma category=\vgamma]}]
        }
        &=
        \catend[\vgamma\in\catGamma]{
            \catend[\ordset{\vn}\in\catsimplex]{
                \vF{\vf{\vgamma}}[\vn,powering={\nerve{\catGamma[comma category=\vgamma]}[simp=\vn]}]
            }
        }
    \\
        &=
        \catend[\vgamma\in\catGamma]{
            \catend[\ordset{\vn}\in\catsimplex]{
                \catend[\vgamma[prime]\in\catGamma[prime]]{
                    \vF{\vgamma[prime]}[
                        \vn,
                        powering=\catGamma[prime]{\vf{\vgamma},\vgamma[prime]},
                        spar=\big,
                        powering={\nerve{\catGamma[comma category=\vgamma]}[simp=\vn]},
                    ]
                }
            }
        }
\\
        &=
        \catend[\vgamma\in\catGamma]{
            \catend[\ordset{\vn}\in\catsimplex]{
                \catend[\vgamma[prime]\in\catGamma[prime]]{
                    \vF{\vgamma[prime]}[
                        \vn,
                        powering=\fibre{
                            \catGamma[prime]{\vf{\vgamma},\vgamma[prime]} ,
                            \nerve{\catGamma[comma category=\vgamma]}[simp=\vn]
                        },
                    ]
                }
            }
        }
\\
        &=
        \catend[\ordset{\vn}\in\catsimplex]{
            \catend[\vgamma[prime]\in\catGamma[prime]]{
                \vF{\vgamma[prime]}[\vn,powering={
                    \catcoend[\vgamma\in\catGamma]{
                        \fibre{
                            \catGamma[prime]{\vf{\vgamma},\vgamma[prime]} ,
                            \nerve{\catGamma[comma category=\vgamma]}[simp=\vn]
                        }
                    }
                }]
            }
        }
\\
        &=
            \catend[\vgamma[prime]\in\catGamma[prime]]{
                \vF{\vgamma[prime]}[powering={
                    \vf[!kan]{
                        \nerve{ \catGamma[comma category=\slot] }{\vgamma[prime]}
                    }
                }]
            }
        =
        \catend[\vgamma[prime]\in\catGamma[prime]]{
            \vF{\vgamma[prime]}[powering={
                \nerve{ \vf[comma category=\vgamma[prime]] }
            }]
        }
    \end{align*}
    where the last equality sign is due
    to \cref{res:kan_extension_nerve}.
\end{proof}

\begin{theorembreak}[{Theorem \parencite[Theorem~19.6.7]{hir}}]\label{res:homotopy_initial}
    Suppose \( \catC \)~is a combinatorial model category
    and~\( \catGamma, \catGamma[prime] \) two categories.
    If \( \vf \colon \catGamma \to \catGamma[prime] \)~is
    homotopy-initial, then we have
    \[\textstyle
        \invholim[\catGamma[prime]]{\vF}
        =
        \invholim[\catGamma]{ \vf[*res]{\vF} }
    \]
    for all~\( \vF \in \catC[diag=\catGamma[prime]] \).
\end{theorembreak}

\begin{proof}
    \Cref{res:bousfield_kan} and equation~\eqref{eq:classical_bousfield_kan}
    show that
    \[
        {
            \textstyle
            \invholim[\catGamma]{ \vf[*res]{\vF} }
        }
        =
        \catend[\vgamma[prime]\in\catGamma[prime]]{
            \fibrep{\vF{\vgamma[prime]}}[powering=
                \nerve{ \vf[comma category=\vgamma[prime]] }
            ]           
        }
        .
    \]
    Since \( \nerve{ \vf[comma category=\vgamma[prime]] } \)
    is contractible for all~\( \vgamma[prime]\),
    \( \nerve{ \vf[comma category=\slot ] } \)~is a projectively cofibrant
    resolution of the point
    by \cref{res:kan_extension_nerve}.
    Thus the right-hand side is
    exactly~\( \invholim[\catGamma[prime]]{\vF}\)
    by~\cref{res:bousfield_kan}.
\end{proof}

\begin{examplebreak}[Example: Fat totalization formula]\label{ex:fat_totalization}
    Recall from \cref{ex:delta_reedy} that the simplex category~\( \catsimplex \)
    is Reedy with~\( \catsimplex[plus] \)
    being the subcategory containing only injective maps.
    The inclusion \(\smash{ \viota\colon \catsimplex[plus]\into\catsimplex }\) is
    homotopy-initial
    (\cite[see e.g.][Example~8.5.12]{riehl}
    or \cite[Example~21.2]{dugger}), hence
    \(\smash{
        \invholim[\catsimplex]{ \vX[cosimp *] } 
        =
        \invholim[\catsimplex[plus]]{ \vX[cosimp *] }
    }\)
    for all~\( \smash{ \vX[cosimp *] \in \catC[diag=\catsimplex] } \).
    As \( \catsimplex[plus] \)~is a direct category, we obtain
    from~\cref{res:holim_direct_category} that we may
    calculate~\( \invholim[\catsimplex]{ \vX[cosimp *] } \)
    as
    \[\textstyle
        \invholim[\catsimplex] { \vX[cosimp *] }
        =
        \catend[\catsimplex[plus]]{
            \fibrep{
                \vX[cosimp=\vn]
            }[simp=\vn]
        }
    \]
    for some functor
    \( \smash{
        \fibrep
        \colon
        \catC
        \to
        \catC[diag={\catsimplex[plus,op]}]
    } \)
    that takes~\( \vx \) to an injectively (i.e.~Reedy-) fibrant replacement of the constant diagram at~\( \vx \)
    (alternatively, this follows from \cref{res:bousfield_kan} using the well-known fact that the standard simplex~\( \simp[d *] \) is projectively cofibrant over~\( \catsimplex[plus] \),
    see e.g. \cite[Example~11.5.6]{riehl}).
    This is the so-called \textdef{fat totalization}
    formula for homotopy limits over~\( \catsimplex \).
    The dual formula for homotopy colimits over~\( \catsimplex[op] \)
    is called the \textdef{fat geometric realization}
    formula.
\end{examplebreak}

The fat totalization formula is one of the main technical tools used in the companion paper to this one,
\textcite{comodules},
to develop a homological model for the dg-derived categories of quasi-coherent sheaves on a dg-scheme in terms of the dg-derived categories of quasi-coherent sheaves on a covering.
This solves the classical problem that \enquote{triangulated categories don't glue well} entirely using concrete homological constructions, unlike the existing \( \infty \)-categorical treatments which only give abstract constructions. Our construction makes it possible to directly apply classical, homological techniques like Koszul duality.

%\chapter*{Acknowledgements}
%
%We would like to thank Edouard Balzin, Marcel B\"okstedt, and Stefan Schwede for many fruitful discussions and for reading through a draft of this paper. Special thanks to Henning Haahr Andersen for many years of great discussions, help, and advice, and for making our cooperation possible in the first place. This paper was written mostly while the authors were visiting the Max Planck Institute for Mathematics in Bonn, Germany. We would like to express our gratitude to the institute for inviting us and for providing us with an excellent and stimulating working environment.

\newpage
\printbibliography

\end{document}

\begin{filecontents*}{references.bib}
@article{comodules,
    author = {Arkhipov, Sergey and Ørsted, Sebastian},
    year = {2021},
    pages = {1-35},
    volume = {7},
    journal = {European Journal of Mathematics},
    doi = {10.1007/s40879-020-00439-4},
    title = {Homotopy limits in the category of dg-categories in terms of $\mathrm{A}_{\infty}$-comodules},
}

@article{explicit,
    author={Block, Jonathan and Holstein, Julian {V.S.} and Wei, Zhaoting},
    title={Explicit homotopy limits of dg-categories and twisted complexes},
    year={2017},
    journal={Homology, Homotopy and Applications},
    volume={19(2)},
    pages={343-371},
}

@online{dugger,
    year={2008},
    hyphenation={american},
    author={Dugger, Daniel},
    title={A primer on homotopy colimits},
    url={http://pages.uoregon.edu/ddugger/hocolim.pdf},
}

@article{gambino_simplicial,
    author = {Gambino, Nicola},
    title = {Weighted limits in simplicial homotopy theory},
    journal = {Journal of Pure and Applied Algebra},
    volume = {214},
    number = {7},
    pages = {1193 - 1199},
    year = {2010},
    %issn = "0022-4049",
    %doi = "https://doi.org/10.1016/j.jpaa.2009.10.006",
    %url = "http://www.sciencedirect.com/science/article/pii/S0022404909002412",
}

@book{hir,
    author={Hirschhorn, Philip S.},
    year={2003},
    title={Model Categories and Their Localizations},
    publisher={American Mathematical Society},
    series={Mathematical Surveys and Monographs},
    volume={99},
}

@book{hovey,
    hyphenation={american},
    author={Hovey, Mark},
    title={Model categories},
    year={1999},
    publisher={American Mathematical Society},
    series={Mathematical Surveys and Monographs},
    volume={63},
    url={https://web.math.rochester.edu/people/faculty/doug/otherpapers/hovey-model-cats.pdf},
}

@book{htt,
    hyphenation={american},
    author={Lurie, Jacob},
    title={Higher Topos Theory},
    year={2009},
    series={Annals of Mathematics Studies},
    number={170},
    publisher={Princeton University Press},
}

@book{riehl,
    hyphenation={american},
    author={Riehl, Emily},
    year={2014},
    title={Categorical Homotopy Theory},
    publisher={Cambridge University Press},
}
\end{filecontents*}

\documentclass[a4paper,oneside,article,english,leqno,10pt]{memoir}

\newif\ifprenumber % if theorems should use format number. type
\prenumbertrue

\makeatletter

\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[shorthands=off]{babel}
\usepackage[noDcommand,slantedGreeks]{kpfonts}

\frenchspacing

\usepackage{mathtools, microtype}

\usepackage[shortlabels]{enumitem}

\AddToHook{bfseries}{\boldmath}

\usepackage[autostyle,english=american]{csquotes}

\usepackage[backend=biber,citestyle=authoryear-icomp,bibstyle=authoryear,
    uniquename=init,giveninits=true,autolang=hyphen]{biblatex}
\addbibresource{references.bib}
\nobibintoc

\let\textdef=\textbf

\usepackage[thmmarks,amsmath]{ntheorem}

\def\@nthm@theorem{Theorem}
\def\@nthm@proposition{Proposition}
\def\@nthm@corollary{Corollary}
\def\@nthm@lemma{Lemma}
\def\@nthm@claim{Claim}
\def\@nthm@definition{Definition}
\def\@nthm@example{Example}
\def\@nthm@exercise{Exercise}
\def\@nthm@remark{Remark}
\def\@nthm@proof{Proof}

\makeatletter
\newtheoremstyle{notitle}% for exercises
{\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator]}%
{\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##3\theorem@separator]}

\newtheoremstyle{notitlebreak}% for exercises with a break
{\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont ##2\theorem@separator}\hbox{\strut}}}]}%
{\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##3\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{prenumber}%
  {\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##1\theorem@separator]}%
  {\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator\ ##3\theorem@separator]}

\newtheoremstyle{prenumberbreak}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##2\theorem@separator\ ##1\theorem@separator}\hbox{\strut}}}]}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##2\theorem@separator\ ##3\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{customplain}%
  {\item[\hskip\labelsep \theorem@headerfont ##1\ ##2\theorem@separator]}%
  {\item[\hskip\labelsep \theorem@headerfont ##3\ ##2\theorem@separator]}

\newtheoremstyle{custombreak}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont
          ##1\ ##2\theorem@separator}\hbox{\strut}}}]}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##3\ ##2\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{postnumpara}%
  {\item[\hskip\labelsep \theorem@headerfont ##2\theorem@separator]}%
  {\item[\hskip\labelsep \theorem@headerfont ##3\ ##2\theorem@separator]}

\newtheoremstyle{postnumparabreak}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont
          ##2\theorem@separator}\hbox{\strut}}}]}%
  {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
          ##3\ ##2\theorem@separator}\hbox{\strut}}}]}

\newtheoremstyle{nonumberplainflex}% for proof environments, see below
    {\item[\theorem@headerfont\hskip\labelsep ##1\theorem@separator]}%
    {\item[\theorem@headerfont\hskip \labelsep ##3\theorem@separator]}

\newtheoremstyle{nonumberbreakflex}%
    {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont
        ##1\theorem@separator}\hbox{\strut}}}]}%
    {\item[\rlap{\vbox{\hbox{\hskip\labelsep \theorem@headerfont 
        ##3\theorem@separator}\hbox{\strut}}}]}

\theoremseparator{.}

\theorembodyfont{\normalfont}

\ifprenumber
    \theoremstyle{notitle}
\else
    \theoremstyle{postnumpara}
\fi

%\newtheorem{para}{}[chapter]
\newtheorem{para}[equation]{}

\ifprenumber
    \theoremstyle{prenumber}
\else
    \theoremstyle{customplain}
\fi

\theorembodyfont{\itshape}

\newtheorem{theorem}[equation]{\@nthm@theorem}
\newtheorem{fact}[equation]{Fact}
\newtheorem{corollary}[equation]{\@nthm@corollary}
\newtheorem{proposition}[equation]{\@nthm@proposition}
\newtheorem{lemma}[equation]{\@nthm@lemma}
\newtheorem{claim}[equation]{\@nthm@claim}
\newtheorem{conjecture}[equation]{Conjecture}

\theorembodyfont{\normalfont}
\newtheorem{definition}[equation]{\@nthm@definition}
\newtheorem{textexercise}[equation]{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remark}[equation]{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{example}[equation]{\@nthm@example}

\theoremstyle{notitle}
\newtheorem{exercise}{\@nthm@exercise}[chapter]

\theoremstyle{nonumberplainflex}
\theoremsymbol{\ensuremath{\square}}
\theoremheaderfont{\itshape\bfseries}
\newtheorem{proof}{\@nthm@proof}

%Unnumbered variants

\theoremstyle{nonumberplainflex}
\theoremheaderfont{\normalfont\bfseries}
\theoremsymbol{}

\theorembodyfont{\normalfont}

\newtheorem{paranonumber}{}

\theorembodyfont{\itshape}
\newtheorem{theoremnonumber}{\@nthm@theorem}
\newtheorem{factnonumber}{Fact}
\newtheorem{corollarynonumber}{\@nthm@corollary}
\newtheorem{propositionnonumber}{\@nthm@proposition}
\newtheorem{lemmanonumber}{\@nthm@lemma}
\newtheorem{claimnonumber}{\@nthm@claim}

\theorembodyfont{\normalfont}
\newtheorem{definitionnonumber}{\@nthm@definition}
\newtheorem{textexercisenonumber}{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remarknonumber}{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{examplenonumber}{\@nthm@example}

%Break variants with line break right after the heading

\theoremsymbol{}
\theoremheaderfont{\normalfont\bfseries}

\ifprenumber
    \theoremstyle{notitlebreak}
\else
    \theoremstyle{postnumparabreak}
\fi

\newtheorem{parabreak}[equation]{}

\ifprenumber
    \theoremstyle{prenumberbreak}
\else
    \theoremstyle{custombreak}
\fi

\theorembodyfont{\itshape}
\newtheorem{theorembreak}[equation]{\@nthm@theorem}
\newtheorem{factbreak}[equation]{Fact}
\newtheorem{corollarybreak}[equation]{\@nthm@corollary}
\newtheorem{propositionbreak}[equation]{\@nthm@proposition}
\newtheorem{lemmabreak}[equation]{\@nthm@lemma}
\newtheorem{claimbreak}[equation]{\@nthm@claim}
\newtheorem{conjecturebreak}[equation]{Conjecture}

\theorembodyfont{\normalfont}
\newtheorem{definitionbreak}[equation]{\@nthm@definition}
\newtheorem{textexercisebreak}[equation]{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remarkbreak}[equation]{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{examplebreak}[equation]{\@nthm@example}

\theoremsymbol{}

\theoremstyle{notitlebreak}
\newtheorem{exercisebreak}[exercise]{\@nthm@exercise}

\theoremstyle{nonumberbreakflex}
\theoremsymbol{\ensuremath{\square}}
\theoremheaderfont{\itshape\bfseries}
\newtheorem{proofbreak}{\@nthm@proof}

% Unnumbered break variants:

\theoremstyle{nonumberbreakflex}
\theoremheaderfont{\normalfont\bfseries}
\theoremsymbol{}
\theorembodyfont{\normalfont}

\newtheorem{parabreaknonumber}{}

\theorembodyfont{\itshape}

\newtheorem{theorembreaknonumber}{\@nthm@theorem}
\newtheorem{factbreaknonumber}{Fact}
\newtheorem{corollarybreaknonumber}{\@nthm@corollary}
\newtheorem{propositionbreaknonumber}{\@nthm@proposition}
\newtheorem{lemmabreaknonumber}{\@nthm@lemma}
\newtheorem{claimbreaknonumber}{\@nthm@claim}
\newtheorem{conjecturebreaknonumber}{Conjecture}

\theorembodyfont{\normalfont}
\newtheorem{definitionbreaknonumber}{\@nthm@definition}
\newtheorem{textexercisebreaknonumber}{\@nthm@exercise}
\theoremsymbol{\ensuremath{\triangle}}
\newtheorem{remarkbreaknonumber}{\@nthm@remark}

\theoremsymbol{\ensuremath{\scriptstyle\bigcirc}}
\newtheorem{examplebreaknonumber}{\@nthm@example}

% Links at references. The "hidelinks" option makes the links colour-neutral
\usepackage[hidelinks]{hyperref}

\usepackage[nameinlink]{cleveref}

\crefname{para}{}{}
\crefname{theorem}{Theorem}{Theorems}
\crefname{claim}{Claim}{Claims}
\crefname{conjecture}{Conjecture}{Conjectures}
\crefname{fact}{Fact}{Facts}
\crefname{definition}{Definition}{Definitions}
\crefname{example}{Example}{Examples}
\crefname{corollary}{Corollary}{Corollaries}
\crefname{proposition}{Proposition}{Propositions}
\crefname{lemma}{Lemma}{Lemmata}
\crefname{remark}{Remark}{Remarks}
\crefname{claim}{Claim}{Claims}
\crefname{exercise}{Exercise}{Exercises}
\crefname{textexercise}{Exercise}{Ecercises}

\crefalias{parabreak}{para}

\crefalias{theorembreak}{theorem}

\crefalias{conjecturebreak}{conjecture}

\crefalias{claimbreak}{claim}

\crefalias{factbreak}{fact}

\crefalias{definitionbreak}{definition}

\crefalias{examplebreak}{example}

\crefalias{corollarybreak}{corollary}

\crefalias{propositionbreak}{proposition}

\crefalias{lemmabreak}{lemma}

\crefalias{claimbreak}{claim}

\crefalias{remarkbreak}{remark}

\crefalias{textexercisebreak}{textexercise}

\newcommand{\crefrangeconjunction}{--} %gives e.g. "table~1--2" instead of "table 1 to~2"

% Now to define environments for theorem parts

\newlist{paralist}{enumerate}{2}
\setlist[paralist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{paralisti}{theorem}

\newlist{theoremlist}{enumerate}{2}
\setlist[theoremlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{theoremlisti}{theorem}

\newlist{corollarylist}{enumerate}{2}
\setlist[corollarylist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{corollarylisti}{corollary}

\newlist{propositionlist}{enumerate}{2}
\setlist[propositionlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{propositionlisti}{proposition}

\newlist{lemmalist}{enumerate}{2}
\setlist[lemmalist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{lemmalisti}{lemma}

\newlist{definitionlist}{enumerate}{2}
\setlist[definitionlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{definitionlisti}{definition}

\newlist{textexerciselist}{enumerate}{2}
\setlist[textexerciselist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{textexerciselisti}{textexercise}

\newlist{remarklist}{enumerate}{2}
\setlist[remarklist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{remarklisti}{remark}

\newlist{examplelist}{enumerate}{2}
\setlist[examplelist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{examplelisti}{example}

\newlist{exerciselist}{enumerate}{2}
\setlist[exerciselist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{exerciselisti}{exercise}

\newlist{claimlist}{enumerate}{2}
\setlist[claimlist]{
    label=\textup{(\roman*)},
    ref=\theequation\textup{(\roman*)},
    resume,
}
\crefalias{claimlisti}{claim}

% The \localref command, allowing references to, say, part (ii) of a theorem without having the theorem number in front; this happens by default due to the above settings

%\makeatletter
\newcounter{localreftmpcnt} %
\newcommand\alphsubformat[1]{\textup{(\roman{#1})}} %adapt ....
\newcommand\localref[2][\alphsubformat]{%
    \ifcsname r@#2@cref\endcsname
    \cref@getcounter {#2}{\mylabel}%
    \setcounter{localreftmpcnt}{\mylabel}%
    \hyperref[#2]{%
        \alphsubformat{localreftmpcnt}%
    }%
    \else ?? \fi}   
%\makeatother

\title{Homotopy (co)limits via homotopy (co)ends in general combinatorial model categories}
\date{\today}
\author{Sergey Arkhipov and Sebastian Ørsted}

\hypersetup{
    pdfauthor={\@author},
    pdftitle={Ω-modules and the affine Hecke category},
}

\numberwithin{equation}{section}

\newcommand\longto{\longrightarrow}
\newcommand\into{\hookrightarrow}

\newcommand\categoryformat[1]{{\operatorname{#1}}}
\newcommand\modelstructureproj{\mathup{Proj}}
\newcommand\modelstructureinj{\mathup{Inj}}
\newcommand\modelstructurereedy{\mathup{Reedy}}

\def\varlim@@auxiliary#1#2#3{%
  \vtop{\m@th\ialign{##\cr
    \hfil$#1\operator@font #3$\hfil\cr
    \noalign{\nointerlineskip\kern0\ex@}
    \expandafter#2\ifx#1\scriptscriptstyle\scriptscriptstyle\else\scriptstyle\fi\cr
    \noalign{\nointerlineskip\kern-\ex@}\cr}}%
}
\def\varlim@@#1#2{%
    \varlim@@auxiliary#1#2%
}

\newcommand\dirlimcommand[1]{\mathop{\mathpalette\varlim@@{{\rightarrowfill@}{#1}}}\nmlimits@}
\newcommand\invlimcommand[1]{\mathop{\mathpalette\varlim@@{{\leftarrowfill@}{#1}}}\nmlimits@}

\usepackage{tikz}
\usetikzlibrary{quotes,babel}
\usetikzlibrary{cd}

\tikzcdset{
  arrow style=tikz,
}

\tikzset{
  >/.tip={Stealth[length=2.9pt, width=4.4pt, inset=1.8pt]},
  tikzcd left hook/.tip={Hooks[
      left,
      length=2pt,
      width=5.5pt,
    ]},
}

\newcommand\invdot{\mathrlap{.}}
\newcommand\invcomma{\mathrlap{,}}

\newcommand\noloc{%
  \nobreak
  \mspace{6mu plus 1mu}
  {:}
  \nonscript\mkern-\thinmuskip
  \mathpunct{}
  \mspace{2mu}
}

\DeclareRobustCommand\sbullet{%
  \mathord{\mathpalette\sbullet@{0.5}}%
}
\newcommand\sbullet@[2]{%
  \vcenter{\hbox{\scalebox{#2}{$\m@th#1\bullet$}}}%
}
\makeatother

\begin{document}

\maketitle

\begin{abstract}
    \noindent We prove and explain several classical
    formulae for homotopy (co)limits
    in general (combinatorial) model categories
    which are not necessarily simplicially enriched.
    Importantly, we prove versions of the Bousfield--Kan formula and the fat totalization formula in this complete generality. We finish with a proof that homotopy-final functors
    preserve homotopy limits, again in complete generality.

    \medskip

    \scriptsize\noindent
    Keywords:
    homotopy limit, category theory, Bousfield--Kan formula,
    \\model categories, simplicial sets, derived functors

    \medskip

    \noindent MSC:
    18G55,
    18D99,
    55U35,
    18G30
\end{abstract}

\numberwithin{equation}{chapter}

\noindent If \( \mathscr{C} \)~is a model category (we assume all model categories to be complete and cocomplete) and \( \Gamma \)~a (small) category,
we denote by \( \mathscr{C}^{\Gamma} = \categoryformat{Fun} (\Gamma, \mathscr{C}) \)
the category of functors~\( \Gamma \to \mathscr{C} \), which we shall also refer to as \enquote{diagrams} of shape~\( \Gamma \).
It is natural to call a map of diagrams~\( \alpha \colon F \to G \)
in~\( \mathscr{C}^{\Gamma} \) a \emph{weak equivalence}
if \( \alpha_{\gamma}  \colon F(\gamma) \to G(\gamma) \)
is a weak equivalence in~\( \mathscr{C} \) for all objects~\( \gamma \in \Gamma \).
We shall refer to such weak equivalences as \textdef{componentwise} weak equivalences.
But then we immediately run into the problem that the limit functor~\( \smash{ \invlimcommand{lim} \colon \mathscr{C}^{\Gamma} \to \mathscr{C} } \)
does not in general preserve weak equivalences. Since \( \invlimcommand{lim} \)~is a right adjoint, this leads us into trying to \emph{derive} it. The right derived functor of~\( \invlimcommand{lim} \) is called the \textdef{homotopy limit} and is
denoted~\( \invlimcommand{holim} \colon \mathscr{C}^{\Gamma} \to \mathscr{C} \).
Dually, the left derived functor of~\( \dirlimcommand{lim} \)
is called the \textdef{homotopy colimit} and is denoted~\( \dirlimcommand{holim} \).

For many purposes, the abstract existence of homotopy limits is all you need. However, there are also many cases where a concrete, minimalistic realization of them is useful for working with abstract notions.
For instance, this paper grew out of an attempt to concretize a concept from derived algebraic geometry. More specifically, we wanted to develop a homological algebra model for the dg-category of quasi-coherent sheaves on a dg-scheme which are equivariant with respect to the action of a group dg-scheme.
This question was addressed in~\textcite{explicit} where a partial result was obtained under serious restrictions (Proposition~13).
The general case was stated as a conjecture, see~Conjecture~1 in the same paper.
In the companion paper to this one, \textcite{comodules},
we cover the general case and prove that conjecture (see~Theorem~4.1.1), and the key result of homotopical nature is proved in the present note
(see~\cref{ex:fat_totalization}).

Quillen's model category machinery tells us how to derive the limit:
We must equip the diagram category~\( \mathscr{C}^{\Gamma} \)
with a model structure with componentwise weak equivalences and in which the
limit functor~\( \invlimcommand{lim} \colon \mathscr{C}^{\Gamma} \to \mathscr{C} \) is a right Quillen functor.
In this case, the derived functor is given by
\(
    \invlimcommand{holim} F = \invlimcommand{lim} R(F) \)
for some fibrant replacement~\( R(F) \)
in~\( \smash{\mathscr{C}^{\Gamma}} \).
Indeed, such a model structure on~\( \mathscr{C}^{\Gamma} \) exists e.g.\ if the model category~\( \mathscr{C} \) is \emph{combinatorial} \parencite[see][Propositions A.2.8.2 and~A.2.8.7]{htt}.
More precisely, we have
the \textit{injective model structure}~\( \smash{\mathscr{C}_{\modelstructureinj}^{\Gamma}} \)
where weak equivalences and cofibrations are calculated componentwise.

The injective model structure being in general rather complicated, calculating such a replacement of a diagram in practice becomes very involved for all but the simplest shapes of the category~\( \Gamma \). Therefore, traditionally, other tools have been used.
One of the most popular techniques involves
\emph{adding a parameter} to the limit functor~\( \invlimcommand{lim}_{\Gamma} \)
before deriving it. The result is the \emph{end}
bifunctor~\(
    \int_{\Gamma}
    \colon
    \Gamma^{\mathup{op}} \times \Gamma  \to
    \mathscr{C}
\)
(introduced below) which is in general much easier to derive.

One of the classical accounts of this technique is
\textcite{hir}
who mainly works in the setting of \emph{simplicial model categories}, which are model categories enriched
over simplicial sets, and which furthermore are equipped with
a \emph{powering} functor
\[
    \categoryformat{SSet}^{\mathup{op}} \times \mathscr{C}  \longto
    \mathscr{C},
    \qquad
    (K, c)
    \longmapsto
    c^{K},
\]
and a \emph{copowering} functor
\[
    \categoryformat{SSet} \times \mathscr{C}    \longto
    \mathscr{C},
    \qquad
    (K, c)
    \longmapsto
    K \otimes c ,
\]
satisfying
some compatibility relations with the model structure.
He then establishes the classical \textdef{Bousfield--Kan formula}
\begin{equation}\label{eq:bousfield_kan}
    \invlimcommand{holim} F     =
    \int_{\gamma \in \Gamma} F(\gamma)^{N(\Gamma /\gamma)}  ,
\end{equation}
where we write~\( N(\Gamma /\gamma) \) for the
nerve of the comma category of maps in~\( \Gamma \)
with codomain~\( \gamma \).
Or rather, he uses this formula as his \emph{definition}
of homotopy limits (see~definition~18.1.8).
A proof that this formula agrees with the general
definition of homotopy limits is due to
\textcite[equation~(2)]{gambino_simplicial}
using the machinery of Quillen 2-functors.

\citeauthor{hir} then generalizes this formula to arbitrary model categories in chapter~19, definition~19.1.5.
He shows that even for non-simplicial model categories,
one can replace simplicial
powerings and copowerings by a weaker notion,
unique up to homotopy in a certain sense.
He then again takes the formula~\eqref{eq:bousfield_kan}
to be his \emph{definition} of a homotopy limit.

This paper is devoted to proving (see~\cref{res:bousfield_kan}) that indeed, the formula~\eqref{eq:bousfield_kan} agrees with the general definition of a homotopy limit
(similarly to what \citeauthor{gambino_simplicial}
did in the simplicial setting), at
least in the case when the model category~\( \mathscr{C} \)
is \emph{combinatorial}.
(This assumption is not a great problem since combinatoriality is what provides us with a model structure on the category~\( \mathscr{C}^{\Gamma} \) in the first place, which is what guarantees that homotopy limits as we defined them above make sense).
To the authors' knowledge, such a proof has not been carried out in the
literature before.
Finally, in \cref{sec:homotopy-initial}, we discuss preservation of homotopy limits by homotopy-initial functors, observing why this classical property also can be proved using our machinery.
As an application, we obtain the classical and fundamental fat totalization formula in the previously mentioned~\cref{ex:fat_totalization}.
There is, of course, a dual result for coends.

\chapter{The projective and injective model structures}

If \( \mathscr{C} \)~is a model category and \( \Gamma \)~any category, it is natural to demand of any model structure on the functor category
\(
    \mathscr{C}^{\Gamma}
    = \categoryformat{Fun} (\Gamma, \mathscr{C})
\)
that weak equivalences must be calculated componentwise.
The two most natural model structures one can hope for (which may or may not exist) are
\begin{itemize}
    \item The \textdef{projective model structure}~%
    \( \mathscr{C}_{\modelstructureproj}^{\Gamma} \)
    where weak equivalences and fibrations are calculated componentwise.
    \item The \textdef{injective model structure}~%
    \( \mathscr{C}_{\modelstructureinj}^{\Gamma} \)
    where weak equivalences and cofibrations are calculated componentwise.
\end{itemize}
Both model structures are known to exist when \( \mathscr{C} \)~is a \emph{combinatorial} model category, see
\textcite[Proposition~A.2.8.2]{htt}.
We shall also use the attributes \textquote{projective(ly)} and \textquote{injective(ly)} when referring to these model structures, so e.g.~\textquote{projectively cofibrant} means cofibrant in the projective model structure.

\begin{propositionbreak}[Proposition {\parencite[Proposition~A.2.8.7]{htt}}]%
    \label{res:Kan_extensions_Quillen_adjunctions}
    If \( \mathscr{C} \)~is a model category and \( f \colon \Gamma\to\Gamma' \) a functor,
    denote by~\( f^{*} \) the restriction functor
    \(\smash{
        \mathscr{C}^{\Gamma'}
        \to
        \mathscr{C}^{\Gamma}
    }\).
    Then \( f^{*} \)~fits as the right and left adjoint of Quillen adjunctions
    \[
    \begin{tikzcd}[sep=scriptsize]
        f_{!}
        \colon
        \mathscr{C}_{\modelstructureproj}^{\Gamma}
        \ar[r,yshift=1.5pt]
        &
        \ar[l,yshift=-1.5pt]
        \mathscr{C}_{\modelstructureproj}^{\Gamma'}
        \noloc
        f^{*}
    \end{tikzcd}
        \qquad\text{resp.}\qquad
    \begin{tikzcd}[sep=scriptsize]
        f^{*}
        \colon
        \mathscr{C}_{\modelstructureinj}^{\Gamma'}
        \ar[r,yshift=1.5pt]
        &
        \ar[l,yshift=-1.5pt]
        \mathscr{C}_{\modelstructureinj}^{\Gamma}
        \noloc
        f_{*}
    \end{tikzcd}
    \]
    whenever the model structures in question exist.
    In particular, the adjunctions
    \(\smash{
        \dirlimcommand{lim}
        \colon
        \mathscr{C}_{\modelstructureproj}^{\Gamma}
        \rightleftarrows
        \mathscr{C}
        \noloc
        \mathup{const}
    }\)
    and
    \(\smash{
        \mathup{const}
        \colon
        \mathscr{C}
        \rightleftarrows
        \mathscr{C}_{\modelstructureinj}^{\Gamma}
        \noloc
        \invlimcommand{lim}
    }\)
    are Quillen adjunctions.
\end{propositionbreak}

The adjoints \( f_{!} \) and~\( f_{*} \) are the usual \textdef[left Kan extension]{left} and \textdef[right Kan extension]{right Kan extensions} along~\( f \), which are given by
limits
\begin{equation}\label{eq:kan_extensions}
    f_{!} F (\gamma')
    =
    \dirlimcommand{lim}_{f(\gamma) \to \gamma'} F(\gamma)   \qquad\text{and}\qquad
    f_{*} F (\gamma')
    =
    \invlimcommand{lim}_{\gamma' \to f(\gamma)} F(\gamma)   .
\end{equation}
These limits are taken over the categories of maps~\( f(\gamma) \to \gamma' \) (resp.~\( \gamma' \to f(\gamma) \))
in~\( \Gamma' \)
for varying~\( \gamma \in \Gamma \).

\begin{corollary}
    Assume that the projective model structure~\( \smash{\mathscr{C}_{\modelstructureproj}^{\Gamma}} \) exists.
    \begin{corollarylist}
        \item\label{res:simple_cofibrations}
        If \( \varphi \colon c \to c' \) is a (trivial) cofibration in~\( \mathscr{C} \) and~\( \gamma_{0} \in \Gamma \) is an object, then the coproduct map
        \(
            \coprod_{\Gamma (\gamma_{0}, -)} \varphi            \colon
            \coprod_{\Gamma (\gamma_{0}, -)} c          \to
            \coprod_{\Gamma (\gamma_{0}, -)} c'         \)
        is a (trivial) cofibration in~%
        \( \smash{\mathscr{C}_{\modelstructureproj}^{\Gamma}} \).
        We shall refer to such (trivial) cofibrations as \textdef[simple (trivial) projective cofibration]{simple projective cofibrations}\index{cofibration!projective!simple}.
        \item\label{res:preserve_simple_cofibrations}
        If \( f \colon \Gamma \to \Gamma' \)~is a functor, then
        \(
            f_{!}
            \colon
            \mathscr{C}_{\modelstructureproj}^{\Gamma}
            \to
            \mathscr{C}_{\modelstructureproj}^{\Gamma'}
        \)
        preserves simple (trivial) projective cofibrations,
        taking \( \coprod_{\Gamma (\gamma_{0}, -)} \varphi \)
        to~%
        \( \coprod_{\Gamma'(f(\gamma_{0}), -)} \varphi \).
    \end{corollarylist}
\end{corollary}

In fact, what we call the simple (trivial) cofibrations form a generating set
for the model category~\( \smash{\mathscr{C}_{\modelstructureproj}^{\Gamma}} \), whereas
the situation is more complicated for~\( \smash{\mathscr{C}_{\modelstructureinj}^{\Gamma}} \), see \textcite[Proposition~A.2.8.2]{htt}.

\begin{proof}
    Applying~\cref{res:Kan_extensions_Quillen_adjunctions} to the
    embedding~\( \iota \colon \gamma_{0} \into \Gamma \) of the full subcategory with~\( \gamma_{0} \) as the only object,
    we get that \( \iota_{!} \varphi \)~is a (trivial) cofibration.
    Now
    \(
        \iota_{!} \varphi       =
        \smash{\coprod_{\Gamma (\gamma_{0}, -)}} \varphi    \)
    by the above colimit formula for left Kan extension.
    The statement~\localref{res:preserve_simple_cofibrations}
    follows
    by applying Kan extensions to the diagram
    \[\begin{tikzcd}[sep=small]
        \gamma_{0} \ar[r,hook] \ar[d]   & \Gamma \ar[d,"f"]
    \\
        f(\gamma_{0}) \ar[r,hook]   & \Gamma'
    \end{tikzcd}\]
    and using that Kan extensions, being adjoints to restriction, respect compositions.
\end{proof}

\chapter{The Reedy model structure}

A third approach exists to equip diagram categories~\( \mathscr{C}^{\Gamma} \) with a model structure, provided the category~\( \Gamma \) has the structure of a \emph{Reedy} category.
A category~\( \Gamma \) is called \textdef{Reedy} if it contains two subcategories
\( \Gamma_{+} , \Gamma_{-} \subset \Gamma \),
each containing all objects, such that
\begin{itemize}
    \item there exists a degree function
    \( \operatorname{Ob} \Gamma \to \mathbb{Z} \),
    such that non-identity morphisms from~\( \Gamma_{+} \) strictly raise the degree
    and non-identity morphisms from~\( \Gamma_{-} \) strictly lower the degree (more generally, an ordinal number can be used instead of~\( \mathbb{Z} \));
    \item each morphism \( f \in \Gamma \) factors \emph{uniquely} as \( f = g h \) for \( g \in \Gamma_{+} \) and
    \( h \in \Gamma_{-} \).
\end{itemize}

We note that a direct category is Reedy with
\( \Gamma_{+} = \Gamma \),
and that an inverse category is Reedy with
\( \Gamma_{-} = \Gamma \).
If \( \Gamma \)~is Reedy, then so is~\( \Gamma^{\mathup{op}} \),
with
\( (\Gamma^{\mathup{op}})_{+} = (\Gamma_{-})^{\mathup{op}} \)
and
\( (\Gamma^{\mathup{op}})_{-} = (\Gamma_{+})^{\mathup{op}} \).

\begin{example}\label{ex:delta_reedy}
    The simplex category~\( \mathbf{\Deltaup} \) is Reedy with~\( \mathbf{\Deltaup}_{+} \) consisting of injective maps and \( \mathbf{\Deltaup}_{-} \)~consisting of surjective maps.
    The degree function does the obvious thing,
    \( [n] \mapsto n \).
\end{example}

If \( \Gamma \)~is a Reedy category and \( \mathscr{C} \)~is any model category, and if \( F \in \mathscr{C}^{\Gamma} \)~is a diagram, we define the \textdef[latching object]{latching} and \textdef[matching object]{matching objects} by
\[
    L_{\gamma} F
    = \dirlimcommand{lim}_{(\alpha \underset{\smash{\neq}}{\to} \gamma) \in \Gamma_{+}} F(\alpha) \qquad\text{and}\qquad
    M_{\gamma} F
    = \invlimcommand{lim}_{(\gamma \underset{\smash{\neq}}{\to} \alpha) \in \Gamma_{-}} F(\alpha) .
\]
In other words, the limit (resp.,\ colimit) runs over the category of all \emph{non-identity} maps \( \alpha \to \gamma \) in~\( \Gamma_{+} \) (resp.,\ \( \gamma \to \alpha \) in~\( \Gamma_{-} \)).
The \textdef{latching map} is the canonical map
\( \smash{L_{\gamma} F} \to F(\gamma) \),
and the \textdef{matching map} is the canonical map
\( F(\gamma) \to \smash{M_{\gamma} F} \).

If \( f \colon F \to G \) is a map in~\( \mathscr{C}^{\Gamma} \), then the \textdef{relative latching map}
and the \textdef{relative matching map} are the maps
\[
    F(\gamma)
    \mathbin{\mathop{\mathbin{\textstyle \coprod}} \limits_{L_{\gamma} F}}
    L_{\gamma} G
    \longto
    G(\gamma)
    \qquad\text{resp.}\qquad
    F(\gamma)
    \longto
    G(\gamma)
    \mathbin{\mathop{\mathbin{\textstyle \prod}} \limits_{M_{\gamma} G}}
    M_{\gamma} F
\]
given by the universal property of the pushout resp.~pullback. We say that \( f \)~is a \textdef{(trivial) Reedy cofibration} (resp.~\textdef{fibration}) if the relative latching map is a (trivial) cofibration (resp.~fibration) in~\( \mathscr{C} \).
If \( F = \varnothing \) (resp.~\( F = * \)), we recover the latching (resp.~matching) map.
For our arbitrary model category~\( \mathscr{C} \), this defines a model structure on~\( \smash{\mathscr{C}^{\Gamma}} \), called the \textdef{Reedy model structure}, see
\textcite[Theorem~15.3.4]{hir}.
The weak equivalences are componentwise weak equivalences.
We shall write~\( \smash{\mathscr{C}_{\modelstructurereedy}^{\Gamma}} \) when we equip the diagram category with this model structure.

\chapter{Homotopy limits}

Let \( \Gamma \) and~\( \mathscr{C} \) be categories, \( \mathscr{C} \)~complete and cocomplete, and let~\( H \colon \Gamma^{\mathup{op}} \times \Gamma \to \mathscr{C} \) a bifunctor. The \textdef{end} of~\( H \) is an object
\( \smash{
    \int_{\Gamma} H = \int_{\gamma \in \Gamma} H(\gamma, \gamma)    }
\)
in~\( \mathscr{C} \), together with morphisms~\(
    \int_{\Gamma} H     \to
    H(\gamma, \gamma)
\) for all~\( \gamma \in \Gamma \), such that for any~\( f \colon \gamma \to \gamma' \), the following diagram commutes:
\begin{equation*}
\begin{tikzcd}
    \int_{\Gamma} H \ar[r] \ar[d]
            & H(\gamma, \gamma) \ar[d, "{H(\gamma, f)}"]
\\
    H(\gamma', \gamma') \ar[r, "{H(f, \gamma')}"']
            & H(\gamma, \gamma')
            \invdot
\end{tikzcd}
\end{equation*}
Furthermore, \( \int_{\Gamma} H \)~is universal with this property in the sense that if \( A \)~is another object of~\( \mathscr{C} \) with a collection of arrows~\( A \to H(\gamma, \gamma) \) for all~\( \gamma \), subject to the same commutativity conditions, then these factor through a unique arrow~\( \smash{A\to \int_{\Gamma} H } \).
There is a dual notion of a \emph{coend}, denoted instead by~\(\smash{ \int^{\Gamma} H } \), which we shall not spell out.

\begin{remark}
    A diagram~\( F \in \mathscr{C}^{\Gamma} \) may be regarded as a diagram in~\( \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma } \) which is
    constant with respect to the first variable. In that case, it follows from the universal property of the end that
    \( \int_{\Gamma} F = \invlimcommand{lim}_{\Gamma} F \)
    recovers the limit of the diagram.
\end{remark}

\begin{remark}\label{res:end_adjunction}
    The end fits as the right adjoint of the adjunction
    \[\begin{tikzcd}[sep=scriptsize]
        \coprod_{\operatorname{Hom}_{\Gamma}}
        \colon
        \mathscr{C} \ar[r, yshift=1.5pt]
            & \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma }
            \ar[l,yshift=-1.5pt]
            \noloc
            \int_{\Gamma}\invdot
    \end{tikzcd}\]
    The left adjoint takes~\( A \in \mathscr{C} \) to the bifunctor
    \( \coprod_{\operatorname{Hom}_{\Gamma} (-, -)} A \colon \Gamma^{\mathup{op}} \times \Gamma \to\mathscr{C} \).
    In the literature, this is usually written as an adjunction
    \[
        \categoryformat{Set}^{\Gamma^{\mathup{op}} \times \Gamma } \bigl(\operatorname{Hom}_{\Gamma}, \mathscr{C} (A, F) \bigr)
        \cong
        \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma } \bigl(A, \textstyle \int_{\Gamma} F \bigr)
    \]
    for \( A \in \mathscr{C} \), which is just the well-known statemant that the end is the
    \emph{weighted limit}~\(
        \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma }
        \to
        \mathscr{C}
    \)
    with weight~\( \operatorname{Hom}_{\Gamma} \).
\end{remark}

The following theorem is the basis for all our homotopy limit
formulae:

\begin{theorem}\label{res:end_functor_quillen}
    Let~\( \mathscr{C} \) be a model category and~\( \Gamma \) a category. Regard the functor category~\( \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma } \) as a model category in any of the following ways:
    \begin{theoremlist}
        \item\label{res:end_functor_quillen_gammaop_gamma} as~\(
            \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma }
            = (\mathscr{C}_{\modelstructureproj}^{\Gamma^{\mathup{op}}})_{\modelstructureinj}^{\Gamma}
        \)
        (assuming this model structure exists);
        \item\label{res:end_functor_quillen_gamma_gammaop} as~\(
            \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma }
            = (\mathscr{C}_{\modelstructureproj}^{\Gamma})_{\modelstructureinj}^{\Gamma^{\mathup{op}}}
        \)
        (assuming this model structure exists);
        \item\label{res:end_functor_quillen_reedy} as~\(
            \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma }
            = \mathscr{C}_{\modelstructurereedy}^{\Gamma^{\mathup{op}} \times \Gamma }
        \)
        (assuming \( \Gamma \)~is Reedy).
    \end{theoremlist}
    Then the end functor~\(
        \int_{\Gamma}
        \colon
        \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma }
        \to
        \mathscr{C}
    \)
    is right Quillen.
\end{theorem}

\begin{proof}
    We initially prove the first statement, the second one being dual.
    By \cref{res:end_adjunction}, it suffices to check that the left
    adjoint~\( \coprod_{\operatorname{Hom}_{\Gamma}} \)
    takes (trivial) cofibations in~\( \mathscr{C} \) to (trivial) cofibations in~\(
        \smash{(\mathscr{C}_{\modelstructureproj}^{\Gamma^{\mathup{op}}})_{\modelstructureinj}^{\Gamma}}
    \).
    If \( c \to c' \)~is a (trivial) cofibration in~\( \mathscr{C} \), then
    we must therefore consider the map~\(
        \coprod_{\Gamma (-, -)} c       \to
        \coprod_{\Gamma (-, -)} c'  \)
    in~\(
        \smash{(\mathscr{C}_{\modelstructureproj}^{\Gamma^{\mathup{op}}})_{\modelstructureinj}^{\Gamma}}
    \).
    Checking that this is a (trivial) injective cofibration
    over~\( \Gamma \)
    amounts, by definition, to checking this componentwise. But for a fixed~\( \gamma_{0} \in\Gamma \), this component is
    \(
        \coprod_{\Gamma (-, \gamma_{0})} c      \to
        \coprod_{\Gamma (-, \gamma_{0})} c' ,
    \)
    which is a simple (trivial) projective cofibration
    in~\( \smash{\mathscr{C}^{\Gamma^{\mathup{op}}}} \).

    For the Reedy case, we recall from
    \textcite[Example~A.2.9.22]{htt}
    and \textcite[Theorem~15.5.2]{hir}
    that being a (trivial) cofibration in the model category~\(
        \smash{\mathscr{C}_{\modelstructurereedy}^{\Gamma \times \Gamma^{\mathup{op}} }}
        = \smash{(\mathscr{C}_{\modelstructurereedy}^{\Gamma})_{\modelstructurereedy}^{\Gamma^{\mathup{op}}}}
    \)
    is equivalent to the restriction being a (trivial) cofibration
    in
    \[
        \smash{\bigl(\mathscr{C}_{\modelstructureproj}^{\Gamma_{+}} \bigr)}_{\modelstructureproj}^{(\Gamma^{\mathup{op}})_{+}}
        =
        \smash{\bigl(\mathscr{C}_{\modelstructureproj}^{\Gamma_{+}} \bigr)}_{\modelstructureproj}^{(\Gamma_{-})^{\mathup{op}}}.
    \]
    But we have, by the unique factorization property of Reedy categories, that
    \[
        \coprod_{\Gamma (-, -)} c       = \coprod_{\gamma_{0} \in \Gamma} \coprod_{\Gamma_{-} (-, \gamma_{0})} \coprod_{\Gamma_{+} (\gamma_{0}, -)} c   \]
    for any~\( c\in\mathscr{C} \).
    These consist of coproducts of exactly the same form as the ones appearing in the definition of simple (trivial) projective cofibrations
    (\cref{res:simple_cofibrations}).
    Thus we find that for any (trivial) cofibration~\( c\to c' \) in~\( \mathscr{C} \),
    the map~\(
        \coprod_{\Gamma (-, -)} c       \to
        \coprod_{\Gamma (-, -)} c'  \)
    is a (trivial) cofibration
    in~\( \smash{\mathscr{C}_{\modelstructurereedy}^{\Gamma^{\mathup{op}} \times \Gamma }} \).
\end{proof}

Thus we can derive the end using any of these three model structures, when available.
Write~\(
    \mathbb{R} \!\int_{\Gamma}
    \colon
    \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma }
    \to
    \mathscr{C}
\)
for the derived functor, which we shall call the \textdef{homotopy end}.

\begin{corollary}\label{res:homotopy_limits_via_ends}
    If \( \mathscr{C} \)~is a combinatorial model category and \( \Gamma \)~a category, then for a diagram~\( F \in \mathscr{C}^{\Gamma} \),
    \[\textstyle
        \invlimcommand{holim}_{\Gamma} F        = \mathbb{R} \!\int_{\Gamma} F      = \int_{\Gamma} R(F)        ,
    \]
    where \( R \)~is a fibrant replacement with respect to the model structure~\(
        \smash{(\mathscr{C}_{\modelstructureproj}^{\Gamma})_{\modelstructureinj}^{\Gamma^{\mathup{op}}}}
    \)
    or, if \( \Gamma \)~is Reedy,
    in~\(
        \smash{\mathscr{C}_{\modelstructurereedy}^{\Gamma^{\mathup{op}} \times \Gamma }}
    \).
\end{corollary}

\begin{proof}
    First write
    \(
        \invlimcommand{holim} F         =
        \invlimcommand{lim} R_{\Gamma} (F)  \)
    for some fibrant replacement functor~\( R_{\Gamma} \)
    in~\( \smash{\mathscr{C}_{\modelstructureinj}^{\Gamma}} \).
    Now \cref{res:Kan_extensions_Quillen_adjunctions}
    and~\textcite[Remark~A.2.8.6]{htt} show that the constant functor embedding~\(
        \smash{\mathscr{C}_{\modelstructureinj}^{\Gamma}}
        \into
        \smash{(\mathscr{C}_{\modelstructureproj}^{\Gamma^{\mathup{op}}})_{\modelstructureinj}^{\Gamma}}
    \)
    is right Quillen and thus preserves fibrant objects.
    Thus \( R_{\Gamma} (F) \)~is also fibrant
    in~\( \smash{(\mathscr{C}_{\modelstructureproj}^{\Gamma^{\mathup{op}}})_{\modelstructureinj}^{\Gamma}} \).
    This proves the first equality sign. The second one is clear.
\end{proof}

Of course, even though \( F \) as a diagram in~\( \mathscr{C}^{\Gamma^{\mathup{op}} \times \Gamma } \) was constant with respect to the first variable, \( R(F) \) is in general not. Remarkably, since ends calculate naturality between the two variables, this often makes calculations of homotopy limits more manageable, compared to resolving the diagram inside~\( \smash{\mathscr{C}_{\modelstructureinj}^{\Gamma}} \).

\begin{corollary}\label{res:holim_direct_category}
    Suppose \( \Gamma \)~is a direct category,
    and let~\(
        \smash{
            R
            \colon
            \mathscr{C}
            \to
            \mathscr{C}_{\modelstructureinj}^{\Gamma^{\mathup{op}}}
        }
    \)
    be a functor that takes~\( c\in\mathscr{C} \) to a fibrant replacement of the constant diagram at~\( c \).
    Then
    \[\textstyle
        \invlimcommand{holim}_{\Gamma} F        =
        \int_{\gamma \in \Gamma} R(F(\gamma)) (\gamma) .
    \]
\end{corollary}

\begin{proof}
    Clearly, \( R(F) \)~is a
    fibrant replacement
    inside~\(
        \smash{(\mathscr{C}_{\modelstructureinj}^{\Gamma^{\mathup{op}}})_{\modelstructureproj}^{\Gamma}}
    \).
    By  \textcite[Example~A.2.9.22]{htt}
    and \textcite[Theorem~15.5.2]{hir},
    this model category is equal
    to
    \[
        \smash{\bigl(\mathscr{C}_{\modelstructureinj}^{\Gamma^{\mathup{op}}} \bigr)}_{\modelstructureproj}^{\Gamma}
        =
        \smash{\bigl(\mathscr{C}_{\modelstructurereedy}^{\Gamma^{\mathup{op}}} \bigr)}_{\modelstructurereedy}^{\Gamma}
        =
        \smash{\bigl(\mathscr{C}_{\modelstructurereedy}^{\Gamma} \bigr)}_{\modelstructurereedy}^{\Gamma^{\mathup{op}}}
        =
        \smash{\bigl(\mathscr{C}_{\modelstructureproj}^{\Gamma} \bigr)}_{\modelstructureinj}^{\Gamma^{\mathup{op}}}
    ,
    \]
    so the result follows from~\cref{res:end_functor_quillen}.
\end{proof}

\chapter{Bousfield--Kan formula}

In \textcite[chapter~19]{hir}, homotopy limits are being developed
for arbitrary model categories via a machinery of simplicial resolutions. In this section, we use \cref{res:end_functor_quillen}/\cref{res:homotopy_limits_via_ends} to explain why this machinery works.
Throughout, we denote by~\( \categoryformat{SSet} \)
the category of simplicial sets endowed with the Quillen model structure.

If \( \mathscr{C} \)~is a (complete) category and~\( X_{\sbullet} \in \mathscr{C}^{\mathbf{\Deltaup}^{\mathup{op}}} \)
a simplicial diagram in~\( \mathscr{C} \), we may extend~\( X_{\sbullet} \)
to a continuous functor~\( X \colon \categoryformat{SSet}^{\mathup{op}} \to \mathscr{C} \)
via the right Kan extension
along
the Yoneda embedding~\(
    \mathbf{\Deltaup}^{\mathup{op}} \into \categoryformat{SSet}^{\mathup{op}}
\):
\[
    X^{K}
    =
    \invlimcommand{lim}_{\Delta^{n} \to K} X_{n} ,
    \qquad
    K\in\categoryformat{SSet}.
\]
If \( \mathscr{C} \)~is a model category, the matching object at~\( [n] \)
is~\( M_{n} X_{\sbullet} = X^{\partial \Delta^{n}} \),
and so \( X_{\sbullet} \)~being Reedy-fibrant
is equivalent
to the map~\(\smash{
    X_{n}
    =
    X^{\Delta^{n}}
    \to
    X^{\partial \Delta^{n}}
}\)
being a fibration in~\( \mathscr{C} \) for all~\( n \).

We need the following technical lemma:

\begin{lemmabreak}[{{Lemma \parencite[Proposition~3.6.8]{hovey}}}]\label{res:hovey_lemma}
    Let~\( \mathscr{C} \) be a model category
    and \( F \colon \categoryformat{SSet} \to \mathscr{C} \) a functor preserving colimits and cofibrations. Then \( F \)~preserves trivial cofibrations if and only if \( \smash{ F(\Delta^{n}) \to F(\Delta^{0}) } \)~is a weak equivalence for all~\( n \).
\end{lemmabreak}

\begin{theorem}[Theorem (Bousfield--Kan formula)]\label{res:bousfield_kan}
    Suppose \( \mathscr{C} \)~is a combinatorial model category,~\( \Gamma \)
    a category, and~\( F \in \mathscr{C}^{\Gamma} \).
    Let~\(
        R
        \colon
        \mathscr{C}
        \to
        \smash{\mathscr{C}^{\mathbf{\Deltaup}^{\mathup{op}}}}
    \)
    be a functor that takes~\( c \in \mathscr{C} \)
    to a Reedy-fibrant replacement of the constant \( \mathbf{\Deltaup}^{\mathup{op}} \)-diagram at~\( c \).
    Let furthermore~\( K \in \smash{\categoryformat{SSet}_{\modelstructureproj}^{\Gamma}} \)
    be a projectively cofibrant resolution of the point.
    Then
    \[
        {\textstyle\invlimcommand{holim}_{\Gamma} F }
        =
        \int_{\gamma \in \Gamma} (R(F(\gamma))^{K(\gamma)}).
    \]
\end{theorem}

\begin{proof}
    Clearly,
    \( \smash{ R(F(-))_{\sbullet} } \)~is a fibrant replacement
    of~\( F \)
    with respect to the model structure~\(
        \smash{(\mathscr{C}_{\modelstructurereedy}^{\mathbf{\Deltaup}^{\mathup{op}}})_{\modelstructureproj}^{\Gamma}}
    \).
    The theorem will follow if we prove that
    \( R(F(-))^{K(-)} \)~is
    a fibrant replacements of~\( F \)
    in~\(
        \smash{(\mathscr{C}_{\modelstructureproj}^{\Gamma})_{\modelstructureinj}^{\Gamma^{\mathup{op}}}}
    \).
    This will follow from Ken Brown's Lemma if we prove
    that the continuous functor
    \[
        \bigl(\categoryformat{SSet}_{\modelstructureproj}^{\Gamma} \bigr)^{\mathup{op}}
        \longto
        \smash{\bigl(\mathscr{C}_{\modelstructureproj}^{\Gamma} \bigr)}_{\modelstructureinj}^{\Gamma^{\mathup{op}}},
        \qquad
        K(-)
        \longmapsto
        R(F(-))^{K(-)}
        ,
    \]
    takes opposites of (trivial) cofibrations to (trivial) fibrations.
    (Trivial) cofibrations
    in~\( \smash{\categoryformat{SSet}_{\modelstructureproj}^{\Gamma}} \)
    are generated from \emph{simple} (trivial) projective
    cofibrations via pushouts and retracts, c.f.~\textcite[Proposition~A.2.8.2]{htt}. Thus by continuity of the functor,
    it suffices to prove the statement for \emph{simple} (trivial) cofibrations.
    We therefore let \(
        \coprod_{\Gamma (\gamma_{0}, -)} K      \into
        \coprod_{\Gamma (\gamma_{0}, -)} L  \)~be one such, where \( K\into L \)
    is a (trivial) cofibration and~\( \gamma_{0} \in \Gamma \).
    This is mapped to
    \[\textstyle
        \prod_{\Gamma (\gamma_{0}, -)} R(F(-))^{L}      \to
        \prod_{\Gamma (\gamma_{0}, -)} R(F(-))^{K} .
    \]
    Thus we must show that the composition
    \[
        \categoryformat{SSet}^{\mathup{op}}
        \xrightarrow{\prod_{\Gamma (\gamma_{0}, -)}}
        \bigl(\categoryformat{SSet}_{\modelstructureproj}^{\Gamma^{\mathup{op}}} \bigr)^{\mathup{op}}
        \longto
        \smash{\bigl(\mathscr{C}_{\modelstructureproj}^{\Gamma} \bigr)}_{\modelstructureinj}^{\Gamma^{\mathup{op}}},
        \qquad
        \textstyle
        K
        \longmapsto
        \prod_{\Gamma (\gamma_{0}, -)} R(F(-))^{K} ,
    \]
    takes (trivial) cofibrations to (trivial) fibrations.
    Checking that it takes cofibrations to fibrations amounts to checking this for the generating cofibrations~\( \partial \Delta^{n}\into\Delta^{n} \) in~\( \categoryformat{SSet} \). This holds by the assumption that \( R(F(-))_{\sbullet} \) is componentwise Reedy-fibrant.
    Since the functor takes colimits to limits,
    the claim now follows from the (dual of) the lemma.
\end{proof}

\begin{remark}
    One may prove
    \parencite[see e.g.][Proposition~14.8.9]{hir}
    that the diagram~\( K(-) = N(\Gamma /-) \in \smash{\categoryformat{SSet}_{\modelstructureproj}^{\Gamma}} \),
    taking~\( \gamma \)
    to the nerve~\( N(\Gamma /\gamma) \)
    of the comma category~\( \Gamma /\gamma \) of all maps in~\( \Gamma \) with codomain~\( \gamma \),
    is a projectively cofibrant resolution of the point. Thus we have
    \begin{equation}\label{eq:classical_bousfield_kan}
        {\textstyle\invlimcommand{holim}_{\Gamma} F }
        =
        \int_{\gamma \in \Gamma} (R(F(\gamma))^{N(\Gamma /\gamma)}),
    \end{equation}
    which is the classical form of the Bousfield--Kan formula~\eqref{eq:bousfield_kan}.
\end{remark}

\chapter{Homotopy-initial functors}\label{sec:homotopy-initial}

A functor~\( f \colon \Gamma \to \Gamma' \)
is called \textdef{homotopy-initial} if for all objects~\( \gamma' \in \Gamma' \),
the nerve~\( N(f/\gamma') \)
is contractible as a simplicial set;
here \( f/\gamma' \) denotes the comma category whose objects are pairs~\( (\gamma, \alpha) \)
where \( \alpha \) is a
map~\( f(\gamma) \to \gamma' \).
A morphism~\(
    (\gamma_{1}, \alpha)
    \to
    (\gamma_{2}, \alpha)
\)
is a morphism~\( \gamma_{1} \to \gamma_{2} \)
in~\( \Gamma \) making the diagram
\[\begin{tikzcd}[row sep=0em]
    f(\gamma_{1})
    \ar[dd] \ar[rd]
\\
        & \gamma'
\\
    f(\gamma_{2}) \ar[ru]
\end{tikzcd}\]
commute. We aim to reprove, using our more modern language, the statement that homotopy-initial functors preserve homotopy limits.
This relies on a few technical lemmas:

\begin{lemma}\label{res:kan_extension_nerve}
    If \( f \colon \Gamma \to \Gamma' \)
    is a functor, then~\(
        f_{!} N(\Gamma /-)      =
        N(f/-)
        \in
        \categoryformat{SSet}^{\Gamma'}
    \).
    In particular,
    since \(
        N(\Gamma /-)
        \in
        \smash{\categoryformat{SSet}_{\modelstructureproj}^{\Gamma}}
    \)
    is cofibrant,
    \(
        N(f/-)
        \in
        \smash{\categoryformat{SSet}_{\modelstructureproj}^{\Gamma'}}
    \)
    is cofibrant
    by \cref{res:Kan_extensions_Quillen_adjunctions}.
\end{lemma}

\begin{proof}
    Since colimits in diagram categories
    over cocomplete categories can be checked componentwise,
    this boils down to the observation
    \[
        \dirlimcommand{lim}_{f(\gamma) \to \gamma'} N(\Gamma /\gamma)_{n}       =
        N(f/\gamma')_{n}
        .
    \]
\end{proof}

The following lemma is inspired
by \textcite[Proposition~19.6.6]{hir}.
See also \textcite[Lemma~8.1.4]{riehl}.

\begin{lemmabreak}\label{res:change_of_diagrams}
    Suppose that \( \mathscr{C} \)
    is a complete category and that \( \Gamma \)
    and~\( \Gamma' \) are two categories
    with a functor~\( f \colon \Gamma \to \Gamma' \).
    Then
    we have
    \[
        \int_{\gamma \in \Gamma} F(f(\gamma))^{N(\Gamma /\gamma)}       =
        \int_{\gamma' \in \Gamma'} F(\gamma')^{N(f/\gamma')}    \]
    for~\( F \in \smash{(\mathscr{C}^{\mathbf{\Deltaup}^{\mathup{op}}})}^{\Gamma} \)
    (see the previous chapter for an explanation of the
    power notation).
\end{lemmabreak}

\begin{proof}
    For the purpose of the proof, we recall
    that the Kan extension formulas
    in~\eqref{eq:kan_extensions} may
    be equivalently written in terms of (co)ends:
    \[
        f_{!} F (\gamma')
        =
        \int^{\gamma \in \Gamma} \Gamma'(f(\gamma), \gamma') \times F(\gamma)       \qquad\text{and}\qquad
        f_{*} F (\gamma')
        =
        \int_{\gamma \in \Gamma} F(\gamma)^{\Gamma'(\gamma', f(\gamma))}        .
    \]
    Here we are using the natural copowering and powering of~\( \categoryformat{Set} \) on~\( \mathscr{C} \),
    given by~\( S \otimes c = \coprod_{S} c \)
    and~\( c^{S} = \prod_{S} c \)
    for~\( S \in \categoryformat{Set} \) and~\( c \in \mathscr{C} \),
    which make sense whenever \( \mathscr{C} \)
    is complete resp.~cocomplete.
    We shall furthermore make use of the
    so-called
    \enquote{co-Yoneda lemma} which says that
    \[
        G(f(\gamma))
        =
        \int_{\gamma' \in \Gamma'} G(\gamma')^{\Gamma'(f(\gamma), \gamma')}         \qquad
        \text{for all }
        G \in \mathscr{C}^{\Gamma'}
        .
    \]
    Finally, we use \enquote{Fubini's theorem} for ends,
    which says that ends, being limits, commute.
    This together yields
    \begin{align*}
        \int_{\gamma \in \Gamma} F(f(\gamma))^{N(\Gamma /\gamma)}       &=
        \int_{\gamma \in \Gamma} \int_{[n] \in \mathbf{\Deltaup}} (F(f(\gamma))_{n}^{N(\Gamma /\gamma)_{n}})    \\
        &=
        \int_{\gamma \in \Gamma} \int_{[n] \in \mathbf{\Deltaup}} \int_{\gamma' \in \Gamma'} (\bigl(F(\gamma')_{n}^{\Gamma'(f(\gamma), \gamma')} \bigr)^{N(\Gamma /\gamma)_{n}}) \\
        &=
        \int_{\gamma \in \Gamma} \int_{[n] \in \mathbf{\Deltaup}} \int_{\gamma' \in \Gamma'} (F(\gamma')_{n}^{\Gamma'(f(\gamma), \gamma') \times N(\Gamma /\gamma)_{n} }) \\
        &=
        \int_{[n] \in \mathbf{\Deltaup}} \int_{\gamma' \in \Gamma'} (F(\gamma')_{n}^{\int^{\gamma \in \Gamma} \Gamma'(f(\gamma), \gamma') \times N(\Gamma /\gamma)_{n} }) \\
        &=
            \int_{\gamma' \in \Gamma'} F(\gamma')^{f_{!} N(\Gamma /-) (\gamma') }       =
        \int_{\gamma' \in \Gamma'} F(\gamma')^{N(f/\gamma')}    \end{align*}
    where the last equality sign is due
    to \cref{res:kan_extension_nerve}.
\end{proof}

\begin{theorembreak}[{Theorem \parencite[Theorem~19.6.7]{hir}}]\label{res:homotopy_initial}
    Suppose \( \mathscr{C} \)~is a combinatorial model category
    and~\( \Gamma, \Gamma' \) two categories.
    If \( f \colon \Gamma \to \Gamma' \)~is
    homotopy-initial, then we have
    \[\textstyle
        \invlimcommand{holim}_{\Gamma'} F       =
        \invlimcommand{holim}_{\Gamma} f^{*} F  \]
    for all~\( F \in \mathscr{C}^{\Gamma'} \).
\end{theorembreak}

\begin{proof}
    \Cref{res:bousfield_kan} and equation~\eqref{eq:classical_bousfield_kan}
    show that
    \[
        {
            \textstyle
            \invlimcommand{holim}_{\Gamma} f^{*} F      }
        =
        \int_{\gamma' \in \Gamma'} R(F(\gamma'))^{N(f/\gamma')}         .
    \]
    Since \( N(f/\gamma') \)
    is contractible for all~\( \gamma'\),
    \( N(f/-) \)~is a projectively cofibrant
    resolution of the point
    by \cref{res:kan_extension_nerve}.
    Thus the right-hand side is
    exactly~\( \invlimcommand{holim}_{\Gamma'} F \)
    by~\cref{res:bousfield_kan}.
\end{proof}

\begin{examplebreak}[Example: Fat totalization formula]\label{ex:fat_totalization}
    Recall from \cref{ex:delta_reedy} that the simplex category~\( \mathbf{\Deltaup} \)
    is Reedy with~\( \mathbf{\Deltaup}_{+} \)
    being the subcategory containing only injective maps.
    The inclusion \(\smash{ \iota\colon \mathbf{\Deltaup}_{+}\into\mathbf{\Deltaup} }\) is
    homotopy-initial
    (\cite[see e.g.][Example~8.5.12]{riehl}
    or \cite[Example~21.2]{dugger}), hence
    \(\smash{
        \invlimcommand{holim}_{\mathbf{\Deltaup}} X^{\sbullet} 
        =
        \invlimcommand{holim}_{\mathbf{\Deltaup}_{+}} X^{\sbullet}  }\)
    for all~\( \smash{ X^{\sbullet} \in \mathscr{C}^{\mathbf{\Deltaup}} } \).
    As \( \mathbf{\Deltaup}_{+} \)~is a direct category, we obtain
    from~\cref{res:holim_direct_category} that we may
    calculate~\( \invlimcommand{holim}_{\mathbf{\Deltaup}} X^{\sbullet} \)
    as
    \[\textstyle
        \invlimcommand{holim}_{\mathbf{\Deltaup}} X^{\sbullet}      =
        \int_{\mathbf{\Deltaup}_{+}} R(X^{n})_{n}   \]
    for some functor
    \( \smash{
        R
        \colon
        \mathscr{C}
        \to
        \mathscr{C}^{\mathbf{\Deltaup}_{+}^{\mathup{op}}}
    } \)
    that takes~\( x \) to an injectively (i.e.~Reedy-) fibrant replacement of the constant diagram at~\( x \)
    (alternatively, this follows from \cref{res:bousfield_kan} using the well-known fact that the standard simplex~\( \Delta^{\sbullet} \) is projectively cofibrant over~\( \mathbf{\Deltaup}_{+} \),
    see e.g. \cite[Example~11.5.6]{riehl}).
    This is the so-called \textdef{fat totalization}
    formula for homotopy limits over~\( \mathbf{\Deltaup} \).
    The dual formula for homotopy colimits over~\( \mathbf{\Deltaup}^{\mathup{op}} \)
    is called the \textdef{fat geometric realization}
    formula.
\end{examplebreak}

The fat totalization formula is one of the main technical tools used in the companion paper to this one,
\textcite{comodules},
to develop a homological model for the dg-derived categories of quasi-coherent sheaves on a dg-scheme in terms of the dg-derived categories of quasi-coherent sheaves on a covering.
This solves the classical problem that \enquote{triangulated categories don't glue well} entirely using concrete homological constructions, unlike the existing \( \infty \)-categorical treatments which only give abstract constructions. Our construction makes it possible to directly apply classical, homological techniques like Koszul duality.

%\chapter*{Acknowledgements}
%
%We would like to thank Edouard Balzin, Marcel B\"okstedt, and Stefan Schwede for many fruitful discussions and for reading through a draft of this paper. Special thanks to Henning Haahr Andersen for many years of great discussions, help, and advice, and for making our cooperation possible in the first place. This paper was written mostly while the authors were visiting the Max Planck Institute for Mathematics in Bonn, Germany. We would like to express our gratitude to the institute for inviting us and for providing us with an excellent and stimulating working environment.

\newpage
\printbibliography

\end{document}

[Jazzpirate]

Hi @sorsted - first of all, congratulations on your new position :)

I downloaded your paper and can verify that I can compile both versions, so we're off to a good start! Apart from that, the CICM conference is in a week (https://cicm-conference.org/2022/cicm.php) which will keep me busy until the 26th or so, but seems to me that indeed, we should talk afterwards :)

By then we should also have proper releases for sTeX on CTAN again, of MMT, and I just published the sTeX-VSCode extension yesterday (although it will only be properly useful once the releases are done, unless one wants to build MMT from sources etc.).

tl;dr: let's talk after CICM, and by then everything should be ready for us to get started :)

[sorsted]

@Jazzpirate Sounds good. Meanwhile, I just added SemanTeX to GitHub, just in case something comes up that needs discussion. I doubt it’s going to be a very active git, though, as the main (and so far, probably only) serious user of SemanTeX is yours truly. ;-)

[Jazzpirate]

Hi @sorsted

So regarding a zoom-call: I'm pretty much open now (except for thursday/friday next week), but @kohlhase will be out of town and/or busy until ~ the 14th. That does not need to stop us though, we can already schedule something. Maybe we want to move that to email - you can find our addresses (in non-web-scrapable forms) at kwarc.info/people.

I've already started somewhat sTeX-ifying your paper, by going through the SemanTeX-version, which I find very informative - what I'm interested in is how you, as the author, think about the semantics of the document contents and your macros seem to show that quite well - which in turn shows us the kinds of mechanisms sTeX should offer. For example, I notice that you typeset the functor category \catGamma -> \catC as \catC[diag=\catGamma] - so it seems like you're thinking of the functor category as "a (unary) component of the category \catC", rather than an external (binary) operator taking two categories. To me, that is very interesting and lends evidence to #363 and in particular #346, which would allow us to provide the syntax \catC{diag}{\catGamma} to achieve the same thing, rather than having to do e.g. \funcat{\catGamma}{\catC}.

For now, I would replace the semanTeX macros by sTeX macros to see where the problems are, how far we can already go, and what we would need to fully annotate everything semantically. But once that works, it would be interesting to see whether and how we can "patch" the semanTeX macros to expand to the sTeX macros, so that we can combine the functionality of both packages - the "semantic syntax" of semanTeX and the formal semantic annotations of sTeX.

I'm hesitant pushing my "experiments" on your paper somewhere public without your permission, but a (public or private) repository would probably be a good thing. If it's alright with you, I would make a new public repository on gl.mathhub.info (where we store all of our sTeX content). Otherwise, I would ask you to make a new private repository there yourself and give me developer permissions, if that's alright with you?

[sorsted]

@Jazzpirate Good ideas! Yes, let us Zoom some time in the next couple of weeks. Let us wait until next week before we discuss the precise schedule of this, as I just started my new postdoc today and should make initial Zoom meetings with my two new hosts. So I’d better take care of those first.

And you have my permission to go ahead and create a depository. The only issue could be if the alternative version we create starts showing up at the top of Google searches for the paper. To avoid this, we should probably either make sure not to include a PDF version, or make the depository private. Both options are fine by me, what do you think? We can change it again later anyway.

It is true, in category theory, the category of functors into the category \catC is sometimes thought of as “diagrams” in \catC, hence the key name diag. The logic behind this becomes the most evident if you have a relatively “small” category. For instance, if you take \catGamma to be the category then a diagram in \catC of shape \catGamma is just a commutative diagram in \catC. So “diagrams” in \catC are really aspects of the category rather than something completely new.

When I type \catC[diag=\catGamma], I think of it as an annotation on \catC, a bit like, say, the dual vector space of a vector space \vectV, which I would type something like \vectV[dual] or \vectV[linear dual] (those keys are not defined above, though).

One of the most fundamental concepts you should always keep in mind with SemanTeX is the outputting system. The rule of thumb is: Whenever you “do” something to an object, it outputs, i.e. becomes a new object of the output class. In this case, the output class is \MyVar (“my variable”), which is just the standard class I use for variables. So once I’ve done \catC[diag=\catGamma], this thing is a new object of class \MyVar. So now I can do anything to this new object that I can do with any other object of \MyVar, e.g. \catC[diag=\catGamma][diag=\catDelta] or \catC[diag=\catGamma][op]. That last thing would be rendered as \mathscr{C}^{\Gamma\mathup{op}}, which looks stupid. This is why there is the key spar (“symbol parentheses”) which adds parentheses around the symbol. So I can do \catC[diag=\catGamma][spar,op] to get (\mathscr{C}^{\Gamma})^{\mathup{op}} instead.

BTW, I should make you aware that there is a new version of SemanTeX which was released a couple of days ago, version 0.521. You won’t notice much difference, but to be sure that we’re on the same page, I suggest you check that your version is up to date. You can run \SemantexVersion to check which version you have.

P.S. Some errors probably happened when I converted the paper from the old version of SemanTeX to the new one. For instance, I just noticed that the paper contained \alpha \colon \vF \to \vG rather than \valpha. I just corrected that.