ScalingStacks

Proof. By symmetry, it is enough to prove (1). Observe that the prism $\Delta^{1}\times\Delta^{2}$ is a left cone on the simplicial set obtained by removing the initial vertex. Formally,

$$\Delta^{1}\times\Delta^{2}\simeq\left(\Delta^{2}\times\Delta^{\left\{1\right\}}\sqcup_{\Delta^{\left\{1,2\right\}}\times\Delta^{\left\{1\right\}}}\Delta^{\left\{1,2\right\}}\times\Delta^{1}\right)^{\triangleleft}.$$

We can therefore interpret the rectangle as a diagram in $\mathcal{C}_{A/}$ (and hence ignore $A$). Since the projection $\mathcal{C}_{A/}\to\mathcal{C}$ preserves and reflects limits (dual of T.1.2.13.8), the square $q_{r}$ is a pullback square in $\mathcal{C}_{A/}$. The universal property of the pullback implies that we have a homotopy Cartesian square

which in turn induces a homotopy equivalence of homotopy fibers of the vertical maps. Considering the given map $B\to Y$ as a point in $\operatorname{Map}_{\mathcal{C}_{A/}}\left(B,Y\right)$ and considering the induced equivalence on the homotopy fibers of the vertical maps, we obtain by T.5.5.5.12 an equivalence

$$\operatorname{Map}_{\mathcal{C}_{A//Y}}\left(\overline{B},\overline{X}\right)\overset{\sim}{\longrightarrow}\operatorname{Map}_{\mathcal{C}_{A//W}}\left(\overline{\overline{B}},\overline{\overline{Z}}\right),$$

where $\overline{B}$ and $\overline{X}$ are $A\to B\to Y$ and $A\to X\to Y$ viewed as objects of $\mathcal{C}_{A//Y}$ and $\overline{\overline{B}}$ and $\overline{\overline{Z}}$ are $A\to B\to W$ and $A\to Z\to W$ viewed as objects of $\mathcal{C}_{A//W}$. By the definition of the space of lifts, this is precisely the equivalence $L\left(q_{l}\right)\simeq L\left(q\right)$. ∎

Proof. Let $\mathcal{M}\to\Delta^{1}$ be the Cartesian-coCartesian fibration associated with the adjunction $F\dashv G$. Since $\mathcal{C}$ and $\mathcal{D}$ are full subcategories of $\mathcal{M}$ we can think of the square $q$ as taking values in $\mathcal{M}$ and it does not change the space of lifts. Consider the diagram in $\mathcal{M}$ given by

where in the left square $q_{l}$ the horizontal arrows are coCartesian and the rest of the data is given by the lifting property of coCartesian edges. Since the inclusion of the spine $\Lambda_{1}^{2}\hookrightarrow\Delta^{2}$ is inner anodyne, so is $\Delta^{1}\times\Lambda_{1}^{2}\hookrightarrow\Delta^{1}\times\Delta^{2}$ (by T.2.3.2.4) and since $\mathcal{M}\to\Delta^{1}$ is an inner fibration, the diagram can be extended to $\Delta^{1}\times\Delta^{2}\to\mathcal{M}$ and we can denote the outer square by $r\colon\Delta^{1}\times\Delta^{1}\to\mathcal{M}$. We now claim that $q_{l}$ is a pushout square in $\mathcal{M}$. For every $Z\in\mathcal{M}$, consider the induced diagram

If $Z\in\mathcal{M}_{0}\simeq\mathcal{C}$, then the spaces on both left corners are empty and if $Z\in\mathcal{M}_{1}\simeq\mathcal{D}$, then both horizontal arrows are equivalences. Either way, this is a pullback square and hence $q_{l}$ is a pushout square. By 4.1.3 we get $L\left(q\right)\simeq L\left(r\right)$.

We can now factor the outer square $r\colon\Delta^{1}\times\Delta^{1}\to\mathcal{M}$ as

where the left square is $p$ and in the right square $q_{r}$ the horizontal arrows are Cartesian and the square is determined by the lifting property of Cartesian edges. Repeating the argument in the dual form we get that $q_{r}$ is a pullback square and using 4.1.3 again we get $L\left(p\right)\simeq L\left(r\right)$ and therefore $L\left(p\right)\simeq L\left(q\right)$. ∎

Proof. For ease of notation, set $\mathcal{D}=\mathcal{C}_{A/}$. Recall that

$$L\left(q\right)=\operatorname{Map}_{\mathcal{D}_{/\overline{Y}}}\left(\overline{B},\overline{X}\right)$$

and therefore

$$L\left(q\right)\times L\left(q\right)=\operatorname{Map}_{\mathcal{D}_{/\overline{Y}}}\left(\overline{B},\overline{X}\right)\times\operatorname{Map}_{\mathcal{D}_{/\overline{Y}}}\left(\overline{B},\overline{X}\right)\simeq\operatorname{Map}_{\mathcal{D}_{/\overline{Y}}}\left(\overline{B},\overline{X}\times\overline{X}\right).$$

Products in the over-category are fibered products and products in the under-category are just ordinary products (dual of T.1.2.13.8). Hence, $\overline{X}\times\overline{X}$ is the diagram $A\to X\times_{Y}X\to Y$, which we denote by $\overline{X\times_{Y}X}$. Thus, a point $s=\left(s_{0},s_{1}\right)\in L\left(q\right)\times L\left(q\right)$ corresponds to a lift in the diagram

in the category $\mathcal{D}$. Furthermore, the diagonal map $\delta_{L\left(q\right)}\colon L\left(q\right)\to L\left(q\right)\times L\left(q\right)$ is induced from the diagonal map $\delta_{\overline{X}}\colon\overline{X}\to\overline{X}\times\overline{X}$. Namely, $\delta_{L\left(q\right)}=\left(\delta_{\overline{X}}\right)_{*}$. Our goal is therefore to compute the homotopy fiber of $\left(\delta_{\overline{X}}\right)_{*}$ over a given point

$$s=\left(s_{0},s_{1}\right)\simeq\operatorname{Map}_{\mathcal{D}_{/\overline{Y}}}\left(\overline{B},\overline{X}\times\overline{X}\right).$$

The projection $\mathcal{D}_{/\overline{Y}}\to\mathcal{D}$ induces an equivalence

$$\left(\mathcal{D}_{/\overline{Y}}\right)_{/\overline{X\times_{Y}X}}\simeq\mathcal{D}_{/\overline{X\times_{Y}X}}.$$

It follows that the fiber is the space of lifts in the diagram

in $\mathcal{D}$. By (the dual of) T.5.5.5.12, this space of lifts is homotopy equivalent to the mapping space $\operatorname{Map}_{\mathcal{D}_{/\overline{X\times_{Y}X}}}\left(\overline{B},\overline{X}\right)$. Recalling that $\mathcal{D}=\mathcal{C}_{A/}$, we see that this is none other than the space of lifts for $p$. ∎