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

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

2011-12-03T20:23:33Z

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)

Answer by Dylan Wilson for Functorial choice of pullbacks in a locally cartesian closed $(\infty,1)$-category

2011-12-04T22:20:27Z

Okay so I think the answer is that, yes, you can define such a functor. The main reasons are as follows:

Pullbacks themselves are only defined up to coherent homotopy equivalence.
Compositions in an infinity category (like $Cat_\infty$) are only defined up to coherent equivalence.
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

(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?)

Answer by Rune Haugseng for Functorial choice of pullbacks in a locally cartesian closed $(\infty,1)$-category

2011-12-04T23:30:04Z

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$".