Question: In a locally cartesian closed category $\mathcal C$, for every map $f:A\to B$, there is an associated pullback functor $f^\* : \mathcal C/B \to\mathcal C/A$. Moreover, if $g:B\to C$, the two functors $(g\circ f)^\*$ and $f^\*\circ g^\*$ are *canonically isomorphic*, but they have no reason to be "equal". Even in the category of sets, the usual choice of pullbacks is only functorial up to isomorphism (see [this paper of Hofmann](http://www.springerlink.com/content/5077x3h92151072u/fulltext.pdf))

This gives a pseudo functor from $\mathcal C^\mathrm{op}$ to $\mathcal{Cat}$. The fact that this is only a pseudo functor and not a functor causes some problems when trying to interpret dependent type theory in locally cartesian closed categories (see for example the previous paper of Hofmann, or [this paper of Curien](http://archive.numdam.org/ARCHIVE/DIA/DIA_1990__23_/DIA_1990__23__43_0/DIA_1990__23__43_0.pdf)).

I was wondering what happens when you pass to $(\infty,1)$-categories. Intuitively, the fact that pullback are only functorial up to isomorphism should not be a problem anymore, because $(\infty,1)$-functors are also only functorial up to isomorphism anyway.

So my question is, **if $\mathcal C$ is a [locally cartesian closed $(\infty,1)$-category](http://ncatlab.org/nlab/show/locally+cartesian+closed+%28infinity,1%29-category), does there always exists a functorial choice of pullbacks?** (by which I mean an $(\infty,1)$-functor from $\mathcal C^\mathrm{op}$ to $(\infty,1)\mathcal{Cat}$ sending objects to slice categories and morphisms to pullback functors)

Answer: 
The easiest thing to do is probably to appeal to the equivalence between functors $\mathcal{C}^{\text{op}} \to \text{Cat}\_{\infty}$ and Cartesian fibrations over $\mathcal{C}$. Roughly speaking, a Cartesian fibration $\mathcal{E} \to \mathcal{C}$ corresponds to a functor that sends $c \in \mathcal{C}$ to the fibre $\mathcal{E}\_{c}$ of the fibration at $c$ and a morphism $f \colon c \to d$ in $\mathcal{C}$ to a functor $f^\* \colon \mathcal{E}\_{d} \to \mathcal{E}\_{c}$ that takes an object $x$ in $\mathcal{E}\_{d}$ to the source of a Cartesian arrow over $f$ with target $x$. This functor is unique up to a contractible space of choices.

The "evaluation at 1" functor $\text{Fun}(\Delta^1, \mathcal{C}) \to \mathcal{C}$ is a Cartesian fibration precisely when $\mathcal{C}$ has pullbacks - a "Cartesian arrow" in $\text{Fun}(\Delta^1, \mathcal{C})$ is the same things as a pullback diagram - so the corresponding functor sends $c \in \mathcal{C}$ to the fibre $\mathcal{C}\_{/c}$ of this map and a morphism $f$ in $\mathcal{C}$ to "pullback by $f$".
Okay so I think the answer is that, yes, you can define such a functor. The main reasons are as follows:

1. Pullbacks themselves are only defined up to coherent homotopy equivalence.
2. Compositions in an infinity category (like $Cat\_\infty$) are only defined up to coherent equivalence.
3. Any two good choices of a "pullback functor" $f^\*: \mathcal{C}/A \rightarrow \mathcal{C}/B$ must be equivalent.

I'm sure there's some highly general proposition in HTT where Lurie proves something where this result is a special case, but I couldn't seem to find such a thing so I've written down some words that I think constitute a (rather messy) proof... I think a lot of what I say is probably unnecessary, so I'll try to clean it up a bit later:

[write up](http://washington.academia.edu/DylanWilson/Teaching/29740/Functoriality_of_pullbacks_in_infty-categories)

(also- it'd be really nice if I could actually just post documents here since I don't really have a webpage, I just sort of made one up on some site that I'm not even sure everyone can see...? Is there a way to do this?)