MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
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

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.

share|cite|improve this answer
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, ? 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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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