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$ 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$C^\mathrm{op}$ to $(\infty,1)\mathcal{Cat}$ sending objects to slice categories and morphisms to pullback functors)

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$ 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$ to $(\infty,1)\mathcal{Cat}$ sending objects to slice categories and morphisms to pullback functors)

1

# Functorial choice of pullbacks in a locally cartesian closed $(\infty,1)$-category

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$ 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$ to $(\infty,1)\mathcal{Cat}$ sending objects to slice categories and morphisms to pullback functors)