5
$\begingroup$

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)

Improve this question
$\endgroup$
4
  • $\begingroup$ Is that functorial in the usual $(\infty,1)$-sense? $\endgroup$
    – David Roberts ♦
    Commented 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$
    – Mike Shulman
    Commented 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$
    – Guillaume Brunerie
    Commented 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$
    – The Amplitwist
    Commented Feb 5, 2023 at 6:51

2 Answers 2

Reset to default
5
$\begingroup$

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

Improve this answer
$\endgroup$
3
  • $\begingroup$ This is much nicer! Good to learn about that neat correspondence! $\endgroup$
    – Dylan Wilson
    Commented 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$
    – Guillaume Brunerie
    Commented 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 5.2.2.5). $\endgroup$
    – Rune Haugseng
    Commented Dec 6, 2011 at 5:33
3
$\begingroup$

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

Improve this answer
$\endgroup$
4
  • $\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$
    – Dylan Wilson
    Commented 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$
    – Dylan Wilson
    Commented Dec 4, 2011 at 22:38
  • 2
    $\begingroup$ Dylan, one word: nLab. $\endgroup$
    – David Roberts ♦
    Commented 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$
    – Guillaume Brunerie
    Commented Dec 5, 2011 at 22:11

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .