I've been looking at various general strategies for proving that some category is triangulated, and Lurie manages to prove that a huge class of interesting examples of categories that we know about are triangulated in his book *Higher Algebra* (formerly DAG I-IV and VI).(EDIT: here's a link to the [book](http://www.math.harvard.edu/~lurie/papers/higheralgebra.pdf)) The trouble is that I am *very* new to this language, and so what he calls $\infty$-categorical notions that are basic and easily motivated' I see as foreign and unfamiliar. 


The part I'm really interested in is the proof of the octahedral axiom on page 24 of *Higher Algebra*. He builds a diagram using a proposition from *Higher Topos Theory* that seems completely out of context (to me!). The proposition says:


``Suppose we are given a diagram of $\infty$-categories $\mathcal{C} \rightarrow \mathcal{D}' \leftarrow \mathcal{D}:p$, where $p$ is a categorical fibration. Let $\mathcal{C}^0$ be a full subcategory of $\mathcal{C}$. Let $\mathcal{K} \subset Map\_{\mathcal{D}'}(\mathcal{C}, \mathcal{D})$ be the full subcategory spanned by those functors $F: \mathcal{C} \rightarrow \mathcal{D}$ which are $p$-left Kan extensions of $F\vert\mathcal{C}^0$. Let $\mathcal{K}'\subset \text{Map}\_{\mathcal{D}'}(\mathcal{C}^0, \mathcal{D})$ be the full subcategory spanned by those functors $F\_0: \mathcal{C}^0 \rightarrow \mathcal{D}$ with the property that, for each object $C \in \mathcal{C}$, the induced diagram $\mathcal{C}^0\_{/C} \rightarrow \mathcal{D}$ has a $p$-colimit. Then the restriction functor $\mathcal{K} \rightarrow \mathcal{K}'$ is a trivial fibration of simplicial sets.''


And Lurie says that, in order to prove (TR4), we use this ``repeatedly to construct a map from the nerve of the appropriate partially ordered set into $\mathcal{C}$.'' (See Lurie's book available for download on his webpage.)


Now, obviously this must be some sort of standard use of the proposition, but I would very much like to understand this one proof without reading all of *Higher Topos Theory*, so we have my question:


1. Is there possibly a more easy-going reference for this proof?
or
2. If it doesn't require too much effort, would someone be willing to explain how the cited proposition applies in this instance?
or
3. Do I really just have to read *Higher Topos Theory* up through Chapter 4?



Proof that the homotopy category of a stable $\infty$-category is triangulated
Alright, here's a proof and construction: Suppose we're given a $2$-simplex $X\to Y\to Z$ in $\mathcal{C}$. We have a lemma: 


Every $2$-simplex in $\Delta^2\to \mathcal{C}$ can be (right Kan-)extended by zeroes via the map $\Delta^2\hookrightarrow \Delta^1\vee \Delta^3$, which gives diagrams of the form:


$$0\leftarrow X\to Y\to Z\to 0.$$ It is an easy computation to show that right Kan extensions relative to the inclusion of a full and faithful subcategory that is also a *sieve* are extensions by zero. 


Let $\mathfrak{A}\subseteq Fun(\Delta^1\vee \Delta^3,\mathcal{C})$ be the full subcategory spanned by objects whose "first and last" vertices are zero. Then the induced map $\mathfrak{A}\to Fun(\Delta^2, \mathcal{C})$ is a trivial fibration by the theorem. 


Then consider the inclusion $$\Delta^1\vee \Delta^3 \cong \Delta^1\times \{0\}\coprod\_{\{0\}\times\{0\}} \{0\}\times \Delta^3\hookrightarrow \Delta^1\times \Delta^3$$


Let $\mathfrak{B}$ be the full subcategory of $Fun(\Delta^1\times \Delta^3,\mathcal{C})$ spanned by diagrams that look like the top row in Lurie's diagram. We can now do another right Kan extension by zero. 


Things are getting a bit more complicated, so we will consider the diagrams as subcomplexes of $\Delta^2\times \Delta^4$. We may identify our $\Delta^1\times \Delta^3$ with the subcomplex spanned by the set of vertices $P\_0:=\{(x,y): x\in \{0,1\}, y\in \{0,1,2\}\}$. Let $P\_1=P\_0\cup \{(2,1),(1,3)\}$. Let $H$ be the subcomplex of $\Delta^2\times \Delta^4$ spanned by $P\_1$. Let $\Delta^1\times \Delta^3\hookrightarrow H$. Taking a right Kan extension, we have extended the diagrams by zero, and then taking the left Kan extension along the inclusion $H\hookrightarrow J$, where $J$ is the subcomplex of $\Delta^2\times \Delta^4$ spanned by the set of vertices $(\Delta^2\times \Delta^4)\_0 -\{(2,0), (0,4)\}$, we get a diagram like Lurie's, and also with the property that the canonical map from the category of such diagrams induced by the projection $Fun(\Delta^2\times \Delta^4,\mathcal{C})\to Fun(\{0\}\times \Delta^2,\mathcal{C})$ is a trivial fibration. 


Since each stage is built up from cokernels, everything that we claimed exists does exist (the verification is a matter of looking at the definition.) Finally, to deduce that every square is in fact a pushout, we apply the pasting law for pushouts in an $\infty$-category a bunch of times.. With that information in hand, we're done, by Lurie's statement. 


