I am having trouble understanding this part in Lurie's Higher Topos Theory. This can be found in section right after Lemma

Lemma Let $p : \mathcal{C} \rightarrow \mathcal{D}$ be an inner fibration of $\infty$-categories and let $X, Y \in \mathcal{C}$. The induced map $$\phi : Hom^R_{\mathcal{C}}(X,Y) \rightarrow Hom^R_{\mathcal{C}}(p(X),p(Y))$$ is a Kan fibration.


Suppose the conditions of Lemma are satisfied. Let us consider the problem of computing the fiber of $\phi$ over a vertex $\overline{e} : p(X) \rightarrow p(Y)$ of $Hom^R_{\mathcal{C}}(p(X), p(Y))$. Suppose that there is a $p$-Cartesian edge $e : X' \rightarrow Y$ lifting $\overline{e}$. By definition, we have a trivial fibration

$$\psi : \mathcal{C}_{/e} \rightarrow \mathcal{C}_{/y} \times_{}\mathcal{D}_{/p(y)} \mathcal{D}_{/\overline{e}}.$$

Consider the $2$-simplex $\sigma = s_1(\overline{e})$ regarded as a vertex of $\mathcal{D}_{/\overline{e}}$. Passing to the fiber, we obtain a trivial fibration

$$ F \rightarrow \phi^{-1}(\overline{e}),$$ where $F$ denotes the fiber of $\mathcal{C}_{/e} \rightarrow \mathcal{D}_{/\overline{e}} \times_{\mathcal{D}} \mathcal{C}$ over the point $(\sigma, x)$.

I am not understanding exactly what he means by "taking fibers". I see that both $F$ and $\phi^{-1}(\overline{e})$ are fibers, but I don't know how he obtains the trivial fibration between them. I was thinking that both those fibers are defined by pullbacks which are actually homotopy pullbacks and maybe we can find a map of diagram in which all component are weak equivalences to have that those two fibers are weakly equivalent. However I can't find those map and it would not show the that this map is a fibration.

  • $\begingroup$ Oscar I see you edited. Do you not understand my answer? You also left in the typo. $\endgroup$ Jan 12, 2019 at 10:06
  • $\begingroup$ I just corrected a random typo before reading your answer. I will edit once more with the typo you mentionned in your answer. I am still trying to fully understand your answer tho. $\endgroup$
    – Oscar P.
    Jan 12, 2019 at 10:19
  • $\begingroup$ I added more detail. $\endgroup$ Jan 12, 2019 at 10:30

1 Answer 1


The version that you've given has a typo. In the latest version of HTT from Lurie's website, it instead defines $F$ as the fibre of $\mathcal{C}_{/e}\to \mathcal{D}_{/\bar{e}}\times_{\mathcal{D}} \mathcal{C}$ over the point $(\sigma, x)$.

The comparison map that you want now is to show that actually $\phi^{-1}(\bar{e})$ is exactly the fibre of $$\mathcal{D}_{/\bar{e}}\times_{\mathcal{D}_{/py}} \mathcal{C}_{/y}\to \mathcal{D}_{/\bar{e}}\times_{\mathcal{D}} \mathcal{C}$$

over $(\sigma,x)$.

This is a routine calculation just drawing out all of the pullback cubes, specifically notice that the fibre of the map between pullbacks is exactly the pullback of the fibres, which gives you exactly the formula you want.

Consider this diagram in sSet

$$\begin{matrix} \mathcal{D}_{/\bar{e}} &\rightarrow &\mathcal{D}_{/py}&\leftarrow&\mathcal{C}_{/y} \\ \downarrow^{\operatorname{id}}&&\downarrow^{\pi^\prime} &&\downarrow^\pi\\ \mathcal{D}_{/\bar{e}} &\rightarrow& \mathcal{D}& \leftarrow& \mathcal{C}\\ \uparrow^\sigma &&\uparrow^{px} &&\uparrow^x\\ \Delta^0 &\rightarrow & \Delta^0 &\leftarrow &\Delta^0 \end{matrix}$$

If you take the pullbacks vertically, you get the diagram

$$\Delta^0 \to \operatorname{Hom}_\mathcal{D}^R(px,py) \leftarrow \operatorname{Hom}_\mathcal{C}^R(x,y) \qquad (1)$$

Taking pullbacks first horizontally, you get

$$\Delta^0 \to \mathcal{D}_{/\bar{e}}\times_{\mathcal{D}} \mathcal{C} \leftarrow \mathcal{D}_{/\bar{e}}\times_{\mathcal{D}_{/py}}\mathcal{C}_{/y} \qquad(2),$$

so by commutation of limits, these both have the same limit, which demonstrates that the fibre product of $(2)$ is exactly the fibre product of $(1)$, as claimed above.

From this, we see that the comparison map is actually a pullback of the map we originally demonstrated was a trivial fibration (by the pasting law for pullback squares).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.