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)

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).

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, 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)

strictlyfunctorial choice of pullbacks, not an "(infinity,1)-functorial" choice. The example cited of the 1-categorical case is about strict functoriality, with pseudo (2-)functoriality being automatic. Strict functoriality is also what's necessary for modeling type theory. I think (infinity,1)-functoriality of pullbacks is analogous to pseudofunctoriality, not to strict functoriality, and isn't good enough for modeling type theory. $\endgroup$`springerlink.com`

is broken. I'm also unable to find any copy saved on the Wayback Machine. $\endgroup$