I added this, with a tiny bit of further details, to model structure for left fibrations– Properties – Weak equivalences.

]]>Thanks! The trick I was missing was that since we’re gluing the cone over the horn back to S, we can take the original simplex as a face of the higher dimensional horn. That is, I was having a hard time seeing what the map

$\Lambda^{n+1}_{i+1}\to (\Lambda^n_i)^{\triangleleft} \coprod_{\Lambda^n_i} S$was.

I was about to ask how to construct all of this formally, but a quick second with a pencil and paper made it clear.

Thanks so much, I really appreciate it!

The key point here is that

$\Lambda^{n+1}_{i+1}\cong (\Lambda^n_i)^{\triangleleft} \coprod_{\Lambda^n_i} \Delta^n$in a compatible way.

]]>(HTT, lemma 2.1.4.6)

The input data is a morphism $\sigma : \Delta^n \to S$.

The pushout diagram in question is

$\array{ \Lambda^{n+1}_{i+1} &\to& (\Lambda^n_i)^{\triangleleft} \coprod_{\Lambda^n_i} S \\ \downarrow && \downarrow \\ \Delta^{n+1} &\to& (\Delta^n)^{\triangleleft} \coprod_{\Delta^n} S } \,.$Writing out the cells here is, as usual, obvious but tedious. Think about it in low dimensions, where you can visualize the simplices:

Set $n = 2$. Start with a 2-simplex $\sigma$ in $S$. Then $(\Delta^2)^{\triangleleft} \coprod_{\Delta^2} S$ is the original simplicial set $S$ together with a tetrahedron $\Delta^3$ built over $\sigma$. One face of the tetrahedron is the original 2-simplex $\sigma$ in $S$, the three others “stick out” of $S$:

The simplicial set $(\Lambda^2_1)^{\triangleleft} \coprod_{\Lambda^2_1} S$ is accordingly the simplicial set $S$ with only two of the three faces of this tetrahedron over $\sigma$ erected.

The map $(\Lambda^3_2) \to (\Delta^2)^{\triangleleft} \coprod_{\Delta^2} S$ identifies the horn of this tetrahedron given by these two new faces and the original face $\sigma$.

The pushout therefore glues in the remaining face of the tetrahedron and fills it with a 3-cell.

]]>Also, I’m not sure if the pushout is in the category of arrows or not, or if it means that it’s a pushout by some morphism (although the second one sounds more plausible).

]]>The LeftCone(X) is the join $\Delta^0\star X$. Also, that definitely won’t work, since if we replace n+1 and j+1 by n and j, we don’t get an inner anodyne map when i=0.

]]>A pushout in the category of arrows? Can we replace $n+1$ and $j+1$ by $n$ and $j$ in the bold statement?

]]>Lemma: Any left anodyne map in SSet/S is a covariant equivalence.

Proof: We can consider the case of a left horn inclusion, since these generate all left anodyne maps.

Then we must show that any map

$i: LeftCone(\Lambda^n_j) \coprod_{\Lambda^n_j} S \to LeftCone(\Delta^n) \coprod_{\Delta^n} S$is a categorical equivalence. **However, $i$ is a pushout of of the map $\Lambda^{n+1}_{j+1} \to \Delta^{n+1}$, which is inner anodyne, so we’re done.**

Questions:

How do we show that $i$ is a pushout as described in the bolded sentence?

]]>