A question about fibrations of simplicial sets and their fibers

Question

I couldn't think of a title for this, but here we go:

Fix $p:S\rightarrow T$, a left fibration of simplicial sets, and an edge $f:\Delta^1 \rightarrow T$. Let $t$ be the first vertex of $f$, and $t'$ be the second vertex.
We name the induced map, $q: S^{\Delta^1}\rightarrow S^{\{1 \}}\times_{T^{\{1 \}}} T^{\Delta^1}$.

Now let $X$ be the simplicial set of sections of the projection $S\times_T \Delta^1\rightarrow \Delta^1$, where the pullback is taken with respect to the map $p:S\rightarrow T$ and the fixed edge $f:\Delta^1 \rightarrow T$.

More notation: We'll denote by $S_{t'}$ the fiber $S \times_T \Delta^0$ where $\Delta^0 \rightarrow T$ is given by the inclusion of the vertex $t'$ and $S\rightarrow T$ is given again by p. We give a fiber $q':X \rightarrow S_{t'}$ of $q$ over the edge $f$ (This is about where I stop understanding what's going on).

What we'd like to show is: $q$ and $q'$ have the same fibers over points of $S^{\{1 \}}\times_{T^{\{1 \}}} T^{\Delta^1}$ where the second projection is the edge f. Remember that exponentiation denotes the internal Hom.

The problem is this simplicial set of sections. What are its maps out, and why do they naturally go to $S_{t'}$ and agree with q? I feel like the key to this is understanding how the exponential is mapping into the pullback, but it's not really clear to me how that should work.

This fact is stated in HTT by Lurie in the proof of proposition 2.1.3.1, but I don't really see how it's obvious.

A link to the relevant proof/page: http://books.google.com/books?id=CTe68E8wK4QC&lpg=PP1&ots=o8qYDiX4mt&dq=lurie%20higher%20topos%20theory&pg=PA67#v=onepage&q=&f=false

Update: "Work" I've done thusfar: $$\ \ \matrix{&S^{\Delta^1}_f &\to & S^{\Delta^1}& \cr &\downarrow &Pb &\downarrow \cr S_{t'}\cong &L_f & \to & L & \to & S^{\{1\}} & \cr &\downarrow &Pb&\downarrow&Pb&\downarrow p \cr &\Delta^{0} & \to & T^{\Delta^1} & \to & T^{\{1\}} \cr &&f&&d_1}\ \ $$

Note that $d_1$ denotes the face map at the vertex 1. Also, $L:= S^{\{1 \}}\times_{T^{\{1 \}}} T^{\Delta^1}$, and The point here is that it should be "morally" the same to give a pullback of $\Delta^1\to T \leftarrow S$ as giving a pullback $\Delta^0\to T^{\Delta^1} \leftarrow S^{\Delta^1}$ with respect to the edge f. So we'd like to show that $X$, the simplicial set of sections of the projection noted before is somehow isomorphic to $S^{\Delta^1}_f$, since this shows that $q$ and $q'$ agree where they're needed to. So what I'm struggling with at this point is showing this last idea.

Answer 1

I've got to agree with you; it's not the best-written proof in HTT. Let me go through it glacially slowly (for my own sake!) to see if I can write something that will help clarify the role of $X$.

Let me write $Map(U,V)$ instead of $V^U$. I find it easier to parse on the internet.

First, what is our $X$? It's the simplicial set of sections of $S\times_T\Delta^1\to\Delta^1$, that is, it is the fiber product

$Map(\Delta^1,S\times_T\Delta^1)\times_{Map(\Delta^1,\Delta^1)}\Delta^0$, where $\Delta^0$ maps in by inculsion of $id$. So (since $Map(\Delta^1,-)$ is a right adjoint) we get: $$X=Map(\Delta^1,S\times_T\Delta^1)\times_{Map(\Delta^1,\Delta^1)}\Delta^0=Map(\Delta^1,S)\times_{Map(\Delta^1,T)}Map(\Delta^1,\Delta^1)\times_{Map(\Delta^1,\Delta^1)}\Delta^0$$ $$=Map(\Delta^1,S)\times_{Map(\Delta^1,T)}\Delta^0$$ where $\Delta^0$ is mapping in by inclusion $f$.

Now we've got our map $$q:Map(\Delta^1,S)\to Map(\{1\},S)\times_{Map(\{1\},T)}Map(\Delta^1,T),$$ whose fibers over $f$ we seek. That is, we just include $$S_{t'}=Map(\{1\},S)\times_{Map(\{1\},T)}\Delta^0\to Map(\{1\},S)\times_{Map(\{1\},T)}Map(\Delta^1,T)$$ (which is itself the pullback of $f:\Delta^0\to Map(\Delta^1,T)$ along the projection, of course) and we pull back to get $q'$.

So the result is a pullback of a pullback. (If I knew how, I'd draw the two pullback squares here.) The composite pullback is the pullback of $f:\Delta^0\to Map(\Delta^1,T)$ along $Map(\Delta^1,S)\to Map(\Delta^1,T)$. But this is what we called $X$. So our result is a map $q':X\to S_{t'}$, and its fiber over any vertex of $S_{t'}$ must coincide with the fiber over the corresponding vertex of $Map(\{1\},S)\times_{Map(\{1\},T)}Map(\Delta^1,T)$, since that will be a pullback of a pullback as well.

Edit (Harry): I typed up the final version of the diagram. If the letters aren't explained, you can deduce what they are just by either looking at Clark's argument or just tracing the pullbacks. Every square is a pullback, so everything is very easy to deal with. $$\ \ \matrix{ X&\cong&S^{\Delta^1}_f &\to &Y^{\Delta^1}&\to& S^{\Delta^1}& \cr &\searrow&\downarrow &Pb &\downarrow&Pb&\downarrow \cr L_f&\cong &S_{t'} & \to &L'&\to& L & \to & S^{\{1\}} & \cr &&\downarrow &Pb&\downarrow&Pb&\downarrow&Pb&\downarrow p \cr &&\Delta^{0} & \to &(\Delta^1)^{\Delta^1} &\to& T^{\Delta^1} & \to & T^{\{1\}} \cr &&&id&&(f)^{\Delta^1}&&d_1}\ \ $$