Can we always make a strictly functorial choice of pullbacks/re-indexing?

$\newcommand{\C}{\mathbf{C}} \newcommand{\D}{\mathbf{D}}$ Let $\C$ be a category with pullbacks. Taking any choice of pullbacks gives us re-indexing functors $f^* \colon \C /Y \to \C/X$, and these will be functorial in $f$ up to natural isomorphism, in that $g^* \cdot f^* \cong (f \cdot g)^*$. However, these will usually not be strictly functorial in $f$; that is, $g^* \cdot f^*$ and $(f \cdot g)^*$ will not be literally equal. Strict functoriality also requires that $1_X^* = 1_{\C/X}$; while this typically does hold on the nose, it’s still not automatic.

My main question: Is there always some choice of pullbacks that make re-indexing strictly functorial? I believe the answer should be “no”, but I don’t know any counterexample. Even in the case of $\mathbf{Set}$, it’s not obvious whether there’s a choice that works.

An equivalent phrasing of the question is: can the codomain fibration $\mathrm{cod} \colon \C^\rightarrow \to \C$ be equipped with a splitting? It can always be replaced by an equivalent split fibration over $\C$; but splitting the codomain fibration itself seems hard.

• Just a rough idea (haven't check if it works): Define an element of $X \times_S Y$ to be a finite diagram of sets which "refines" $X \rightarrow S \leftarrow Y$ together with compatible elements in all the sets. – Martin Brandenburg Oct 11 '13 at 23:09
• You could rephrase this as asking whether any 2-functor C -> Cat is isomorphic to a strict 2-functor (that is, the components of the transformation are isos, not equivalences). This is already assuming enough Choice to get from a fibration to said 2-functor, and you may not want this. – David Roberts Oct 12 '13 at 0:04
• I'd say this is an undesirable property. Replacing isomorphisms with equalities is unnatural. – Fernando Muro Oct 12 '13 at 0:16
• @FernandoMuro Until you're doing type theory :-) – David Roberts Oct 12 '13 at 0:40
• @MartinBrandenburg: I don’t follow exactly what you’re suggesting, but the trouble I’ve had with constructions along those lines is that they don’t give $1^* = 1$, and if you modify them by making a special case for identities, then you lose $g^*f^*=(fg)^*$ in the case where $fg = 1$. – Peter LeFanu Lumsdaine Oct 12 '13 at 17:15

No, it is not always possible to make a strictly functorial choice of pullbacks. Four years later, I found a simple (if contrived) counterexample for this:

Let $\newcommand{\C}{\textbf{C}}\C$ be any full subcategory of $\textbf{FinSet}$ containing infinitely many sets of size 2, and at least one set of every finite size, but only one set of size 4. Certainly $\C$ has all pullbacks, since it is equivalent to $\textbf{FinSet}$.

Now pick specific 1- and 2-element sets $\newcommand{\one}{{1}}\newcommand{\two}{{2}}\one$, $\two$. Let $r : \two \to \one$ be the unique possible map, and $s : \one \to \two$ either of the two possible such maps. Then $s$, $r$ form a section-rectraction pair $\one \to \two \to \one$, with $rs = \newcommand{\id}{\mathrm{id}}\id_\one$.

If $\C$ had a strictly functorial choice of pullback functors, then the functors $r^* : \C/\one \to \C/\two$ and $s^* : \C/\two \to \C/\one$ would also be a (strict) section-retraction pair, with $s^* r^* = \id_{\C/\one}$. In particular, this would exhibit the subcategory of $\C/\one$ on 2-element sets (which is infinite) as a strict retract of the subcategory of $\C/\two$ on “maps into $\two$ where each fiber has size 2”, which has only 3 objects since $\C$ had only one object of size 4. But this is impossible: a finite category can’t be a strict retract of an infinite one.

• Note: This fully answers the question, but the counterexample is rather contrived. If, seeing this counterexample, someone can see how to improve it to an argument showing that some naturally-occurring category gives a counterexample, that would be a much better answer! So I will leave this answer un-accepted for a few days in case anyone can see that; otherwise I will accept this answer. – Peter LeFanu Lumsdaine Aug 30 '17 at 20:37

Many years ago, Peter Freyd published (I think he published it) a paper in which he showed that while it was possible to replace any category with products by a category with canonical products, the same could not be done for pullbacks. The only thing I remember about the paper was the use of the word "table" for some construction. If you can't find it, write to Peter directly.

• Thankyou very much! I’m having trouble finding the exact statement in his papers, so have written to him, and will report back when I have any more details. – Peter LeFanu Lumsdaine Oct 14 '13 at 20:27
• Did Theoretical Computer Science publish an unfinished paper by Peter Freyd, sciencedirect.com/science/article/pii/S0304397500003285 ? See Section 5, for example. And where are the references? – Andrej Bauer Oct 15 '13 at 7:04
• It's an invited talk at MFPS, so I guess it's allowed to be less formal than usual. – Tom Hirschowitz Oct 16 '13 at 13:29
• @TomHirschowitz: Perhaps, but unfinished sentences and missing LaTeX macros are a bit more informal than I’d expect! It looks very much as if they accidentally published an early draft instead of a final version. – Peter LeFanu Lumsdaine Oct 17 '13 at 17:29

Here's an argument (assuming global choice) that the codomain fibration will always be split in "natural" cases. Perhaps it's well-known, or perhaps it has an important shortcoming (such as the use of choice?). Or perhaps there's an error -- strictification is tricky!

Claim: Let $C$, $D$ be categories with pullbacks, and suppose there is a functor $p: C \to D$ with the following properties:

1. $p$ preserves pullbacks.

2. $p$ is an isofibration, and induces an isofibration on all slices (perhaps this is redundant?).

3. $p$ reflects identities (i.e. if $f: c \to c$ is an endomorphism in $C$, and $pf: pc \to pc$ is an identity, then so is $f$).

4. There is a cardinal $\kappa$ such that for every $f: x \to c \in C^{[1]}$, the isomorphism class $[f]$ of $f$ in the fiber category $p^{-1}(pf) \subseteq C/c$ has cardinality $\kappa$.

The claim is that if $D$ admits strict reindexing, then so does $C$, and $p$ preserves the strict reindexing.

Upshot: Most "natural" categories $C$ admit such a functor $p: C \to \mathsf{Set}$, with $\kappa$ being the cardinality of the universe (perhaps with an exception for objects over $\emptyset$, which often doesn't matter because there are few maps into $\emptyset$). I'm assuming that $\mathsf{Set}$ admits strict reindexing (right?). So most "natural" categories do as well.

EDIT: $\mathsf{Set}$ does indeed admit strict reindexing. To see this, as in the comment below, note that the fibration $\mathsf{Set}^{(-)} \to \mathsf{Set}$ admits a splitting, and the fibration $\mathsf{Set}/(-) \to \mathsf{Set}$ is isomorphic as a fibered caegory -- the fact that it's equivalent as a fibered category is standard, and each isomorphism class in each fiber category has the cardinality of the universe, in both fibrations, so an isomorphism of fibrations exists. So $\mathsf{Set}/(-) \to \mathsf{Set}$ also admits a splitting as desired.

So indeed, most "natural" categories admit a strict reindexing. Of course, it's completely undecideable to compute it because the choice function must solve the isomorphism problem!

Proof of Claim: Let $()^\ast$ be a system of strict reindexing in $D$. Fix enumerations of the isomorphism classes of the fibers of $p$ by $\kappa$ (using condition (4) and choice). Now, if $\gamma : c' \to c$ is a morphism in $C$ and $f: x \to c \in C/c$, take an arbitrary pullback of $f$ along $\gamma$. Because $p$ is an isofibration (condition (2))and $p$ preserves pullbacks (condition (1)), we can correct this choice to lie over the canonical pullback $(p\gamma)^\ast(pf)$. Moreover, we can choose a representative which has the same index under our enumeration as $f$ does; let's call it $\gamma^\ast(f)$. It remains only to nail down the lift of the other leg of the pullback square, but any two choices differ by an automorphism of $\gamma^\ast(f)$ which lies over the identity on $(p\gamma)^\ast(pf)$, so by condition (3) this choice is uniquely determined.

It's now obvious that the lifted operation $()^\ast$ is strictly functorial, because it preserves the indexing by our enumerations.

• Or maybe this is much ado about nothing -- assuming (4) with $D$ the terminal category should simply allow you to construct strict reindexing directly, so maybe I should infer that an assumption like (4) is not a reasonable assumption in the situations that Peter is thinking about... – Tim Campion Aug 31 '17 at 1:05
• I certainly agree with your claim — I’ve looked at similar approaches myself before, not to split the codomain fibration itself but to obtain well-behaved split fibrations equivalent to it, typically starting from the replacement of $\mathbf{Set}/-$ by $\mathbf{Set}^{(-)}$. However, for splitting the codomain fibration itself, it’s not so clear how to apply it. Taking $D$ to be the terminal category doesn’t work, since “reflects identities” won’t hold. And for taking $D$ to be $\mathbf{Set}$, first you’d have to find strict reindexing there, which might be possible but is far from obvious! – Peter LeFanu Lumsdaine Aug 31 '17 at 8:30
• But isn't $\mathsf{Set}^{(-)}$ isomorphic to $\mathsf{Set}/-$ as categories fibered over $\mathsf{Set}$? Not by the obvious functor, of course -- but they are equivalent as fibered categories and all nonempty isomorphism classes have the same cardinality in the two fibrations (the cardinality of the universe) ergo they are isomorphic as fibered categories, no? And therefore $\mathsf{Set}/-$ admits a splitting because $\mathsf{Set}^{(-)}$ does. – Tim Campion Aug 31 '17 at 12:44
• Ah, very nice! Yes, I absolutely agree. I think that would be worth adding to the answer, since it’s not obvious (except of course in hindsight). – Peter LeFanu Lumsdaine Aug 31 '17 at 14:09
• Actually, I don’t think one even does need any choice in order to construct the splitting on Sets, or transfer it to most natural categories. Let’s continue this discussion by email, to avoid cluttering comments here! – Peter LeFanu Lumsdaine Sep 1 '17 at 9:09