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)

  • $\begingroup$ Is that functorial in the usual $(\infty,1)$-sense? $\endgroup$
    – David Roberts
    Dec 4, 2011 at 20:59
  • 1
    $\begingroup$ Up until the final parenthetical, I thought this question was asking for a strictly functorial 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$ Dec 5, 2011 at 8:25
  • $\begingroup$ @Mike If we want to model (homotopy) type theory in weak $(\infty,1)$-categories, we will have to deal with weak functors somehow. I agree that the usual models of type theory use strict functoriality, but perhaps that there will be someday a notion of model in a weak $(\infty,1)$-category where strict does not mean anything. $\endgroup$ Dec 5, 2011 at 21:52
  • $\begingroup$ The link to springerlink.com is broken. I'm also unable to find any copy saved on the Wayback Machine. $\endgroup$ Feb 5 at 6:51

2 Answers 2


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

  • $\begingroup$ This is much nicer! Good to learn about that neat correspondence! $\endgroup$ Dec 5, 2011 at 0:10
  • $\begingroup$ Thanks! Does this also proves that when the $(\infty,1)$-category is locally cartesian closed, there is an $(\infty,1)$-functorial choice of right adjoints to the pullback functor? $\endgroup$ Dec 5, 2011 at 21:54
  • $\begingroup$ A map $\mathcal{E} \to \mathcal{C}$ that's both a Cartesian and a coCartesian fibration corresponds to $F \colon \mathcal{C} \to \text{Cat}_{\infty}$ and $G \colon \mathcal{C}^{\text{op}} \to \text{Cat}_{\infty}$ such that $F(f)$ is left adjoint to $G(f)$ for all $f$ in $\mathcal{C}$. For right adjoints to pullbacks we can consider the opposite of the evaluation functor, $\text{Fun}(\Delta^1, \mathcal{C})^{\text{op}} \to \mathcal{C}^{\text{op}}$. This is coCartesian if $\mathcal{C}$ has finite limits, and Cartesian iff each pullback functor has a right adjoint (Higher Topos Theory $\endgroup$ Dec 6, 2011 at 5:33

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

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

  • $\begingroup$ Also: the document probably needs proofreading, and I'm certain there were various places where I needed to put an "op" and didn't... Maybe I should have just done it for pushouts instead. $\endgroup$ Dec 4, 2011 at 22:23
  • $\begingroup$ Also! Why did you need locally Cartesian closed? It seems like existence of finite limits is all you need... $\endgroup$ Dec 4, 2011 at 22:38
  • 2
    $\begingroup$ Dylan, one word: nLab. $\endgroup$
    – David Roberts
    Dec 4, 2011 at 23:54
  • $\begingroup$ Indeed, I only needed the existence of finite limits for this question. In semantics of type theory, local cartesian closedness is used for interpreting dependent products. $\endgroup$ Dec 5, 2011 at 22:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.