I've often seen Lurie's *Higher Topos Theory* praised as the next "great" mathematical book. As someone who isn't particularly up-to-date on the state of modern homotopy theory, the book seems like a lot of abstract nonsense and the initial developments unmotivated. I'm interested in what the tools developed concretely allow us to do.


**What does HTT let us do that we previously were unable to?**


Please note that I'm looking for concrete examples or theorems that can be expressed in terms of math that one doesn't need higher topos theory to understand. I'd also be interested in ways that the book has changed pre-existing perspectives on homotopy theory.



Higher Topos Theory- what's the moral?
It seems there are really two questions here:


1. Why higher category theory? What questions can you pose without the language of higher category theory which are best answered using higher category theory?
2. Why does Lurie's work specifically set the standard for the foundations of higher category theory?


These are really distinct questions. I'll leave it to others to address (1), and focus on (2). For this, I will refer back to an [old answer of mine](https://mathoverflow.net/questions/311158/what-parts-of-the-theory-of-quasicategories-have-been-simplified-since-the-publi/311273#311273) for a summary of some of the contents of HTT and HA. There, I said:



> 
> In *Higher Topos Theory*, Lurie accomplishes many things. Let me highlight a few:
> 
> 
> * A study of the Joyal model structure and comparison to the Bergner model structure.
> * A study of cartesian fibrations and straightening / unstraightening, the $\infty$-categorical analog of the Grothendieck construction. This is often viewed as the technical heart of Lurie's theory, since cartesian fibrations are used systematically to avoid writing down all the higher coherence data involved in $qCat$-valued functors.
> * A development of the fundamental notions of category theory -- (co)limits, Kan extensions, cofinality, etc, allowing one to "do category theory" in the $\infty$-categorical setting.
> * A development of the theory of presentable $\infty$-categories. The point here is to get access to (the most important instances of) Freyd's adjoint functor theorem in the $\infty$-categorical setting, and in particular the theory of localizations.
> * The theory of (Grothendieck) $\infty$-toposes.
> 
> 
> In the context of foundations, maybe it's worth also mentioning some of the contents of *Higher Algebra*:
> 
> 
> * The Barr-Beck monadicity theorem. I tend to think of this, along with the adjoint functor theorem as "the only real theorems" of basic ordinary category theory.
> * A theory of operads, allowing one to "do algebra" $\infty$-categorically.
> * The theory of stable $\infty$-categories, playing roughly the roles of abelian categories and triangulated categories in the $\infty$-categorical setting.
> 
> 
> 


So the reason that HTT and HA set the standard for the foundations of category theory is pretty self-evident. Nowhere else can one find such a comprehensive treatment! The 2500 pages in these books are there for a reason. Some pieces of HTT/HA were previously available in various sources, but some were not, and moreover HTT/HA synthesize them in coherent account. So you don't have to spend as much time as you otherwise would have to patching together results proven in slightly different frameworks using model-comparison results.


This is particularly striking from a historical perspective: in the days when HTT first appeared (almost 10 years ago now -- to call it "the next great mathematical book" is already a little behind the times I think: it's a *current* great mathematical book!), all of this was a dream. Lurie made it a reality.


I'll add on a personal note that my own most common mode of doing higher category theory is to pretend that everything is an ordinary category and freely use all the tools available there, until I've worked out a complete argument. After that I go through the process of looking up $\infty$-categorical analogs of each of the 1-categorical tools I've used in my argument. This works better than one might expect, because it's reasonable today to trust that most of these tools will indeed be available in the literature. That's thanks in large part to Lurie's work. Before Lurie, you could do something like this, but only if you were content to end up with incomplete arguments contingent on the dream of higher category theory working out. Today, I'd argue that higher category theory, among various mathematical disciplines, actually has a relatively *high* standard of rigor. That's thanks in part to Lurie's work setting the standard.




---


Let me close by sharing a sort of testimonial from Clark Barwick ([originally from the homotopy theory chat room](https://chat.stackexchange.com/transcript/message/41977621#41977621) here on MO, in the context of [another MO question](https://mathoverflow.net/questions/289259/the-derived-drift-is-pretty-unsatisfying-and-dangerous-to-category-theory-or)). Thanks to user1092847 for digging this up in the [comments](https://mathoverflow.net/questions/433554/higher-topos-theory-whats-the-moral/433590#comment1116677_433590) below!


**Clark Barwick on Lurie's impact with HTT:**



> 
> ... I feel a need to defend Jacob Lurie's writing. Let me take a rather selfish perspective, because I grew up alongside higher categories in some sense. I read preprints and papers of Rezk, Hirschowitz-Simpson, Simpson, Tamsamani, Toen, Joyal, Jacob's HTT-prototype on the arXiv, and others as a grad student (2001-05).
> 
> 
> All of these works had the same feature: they were all organised around a specific goal, leaving the more serious work of a complete theory for a later time. There were all sorts of homotopy coherence issues that were left hanging.
> 
> 
> So I developed my own point of view about these things and started writing a manuscript, the first little bit of which was my thesis.
> By the time I was halfway through my first postdoc, I'd written a pile of 'prenotes' that did enough foundational work to ensure, e.g., that there was no confusion over 'how unique' an adjoint between ∞-categories is, how to prove the existence of all colimits in an ∞-category from, say, geometric realisations and coproducts, a theory of what we now call ∞-operads, etc., etc.
> 
> 
> It all involved layer upon layer of giant combinatorial gadgets, and they were often fragile enough that I wasn't sure I had them layered correctly.
> 
> 
> At around that time I met Jacob at a conference, and he mentioned that he'd revised the text he put on the arXiv to add a little more detail. I said that I'd love to see it. He sent me a PDF of 600 pages or so of HTT.
> 
> 
> To my surprise and horror, he'd done everything I'd done, but more of it and far far better. He'd understood issues like cofinality in a way I didn't have access to with the models I was using. In his text, the proofs worked because of some very compact, very robust models he chose early on, following Joyal.
> 
> 
> Those models required him to do a lot of pretty tedious technical labour in the first few sections, but it ensured that if something existed up to homotopy, it 'really' existed. (This always came down to selecting a section of a trivial fibration.) This meant that it was genuinely easy to understand the arguments.
> 
> 
> When you look at a proof in HTT or HA or SAG, it's all there. He doesn't tell you that you 'can' find the argument – he gives you the argument! That's the real advantage of Jacob's arguments (and Joyal's before him) – they're completely convincing. You can actually check (and in rare cases, yes, correct) his proofs, because every individual object is so concrete. (Cf. claims about $A\_{\infty}$-categories like the Fukaya category.)
> 
> 
> After a few sleepless nights, I just gave up on what I was trying to develop. I was not going to try to compete. On the other hand, I didn't feel comfortable enough in the Joyal/Lurie perspective to really use their model, so I tried to do things in a model-independent way, as Rune suggests.
> 
> 
> But even simple things, like constructing a symmetric monoidal functor between two symmetric monoidal ∞-categories when there isn't one for formal reasons, is very difficult from that perspective: the only path I saw was to check an infinite hierarchy of coherences.
> It took me a long time to realise that the fibrational perspective was exactly designed to make it easy (or at least convincing) to write these things down. Jacob is actually providing you with the tools to perform explicit, nontrivial, non-formal constructions with higher categories in a precise, legible, and convincing way. That's what results like HTT.3.2.2.13 are all about.
> 
> 
> Jacob's done this continually: at every turn, he's done an incredible service to the community by carving out not just a narrow path to a desired application, but an expansive tunnel through which a lot of us can travel. He offers incredibly refined, interlinking technologies that are ideal for people like me, at least. I'm in a particularly good position to appreciate that kind of labour, because I attempted it and failed where he succeeded.
> 
> 
> Does he solve every problem or define every conceivable object? No, of course not. (And if it's tough to read now, what would it be like if he did? (However, I will point out that he does deal with general pro-objects in SAG.E.2.)) Is it possible to sharpen his results or use little techniques to get improvements on his results? Sure. But overall, I think that the precision, clarity, and thoroughness of Jacob's writing is something to which homotopy theory should aspire.
> 
> 
> 


