# Codomain fibration.

It is known that the codomain fibration is given by a functor in the form $\mathcal{C}^{\rightarrow}\longrightarrow\mathcal{C}$ where $\mathcal{C}$ is a category having pullbacks and $\mathcal{C}^{\rightarrow}$ is the arrow category. It is also known (see B. Jacobs, Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, North Holland, Elsevier, 1999. ISBN 0-444-50170-3) that the condition of $\mathcal{C}$ having pullbacks is necessary and sufficient.

In the same book can also be found the definition of a chain of fibrations in the form $\mathcal{C}^{\rightarrow\rightarrow}\longrightarrow\mathcal{C}^{\rightarrow}\longrightarrow\mathcal{C}$ etc and that it depends again on the condition of $\mathcal{C}$ having pullbacks.

My question is: could this sequence be defined as a fibration when $\mathcal{C}$ is just a cartesian category? Would the fibers be the same (that is: the slices over an object in $\mathcal{C}$)?

-

I assume, like Finn, that by "cartesian" you mean "having finite products". It's not really clear to me what you're looking for, since you said yourself that a necessary and sufficient condition for the codomain functor to be a fibration is that $\mathbf{C}$ have pullbacks.

There is however a vaguely "codomain-like" fibration $\mathbf{C}^{pr} \to \mathbf{C}$ for a category $\mathbf{C}$ with finite products, where $\mathbf{C}^{pr}$ is the full subcategory of $\mathbf{C}^{\to}$ whose objects are first projections out of cartesian products $A\times B\to A$. This is a fibration since the pullback of such a projection along any map $f\colon A'\to A$ always exists in a category with products (it is $A'\times B$).

The fiber of this fibration over $A$ is, of course, the full subcategory of the slice category over $A$ consisting of first projections out of cartesian products. That's equivalent to a category whose objects are those of $\mathbf{C}$ and whose morphisms from $B$ to $B'$ are morphisms $A\times B \to B'$, i.e. the co-Kleisli category of the comonad $(A\times -)$ on $\mathbf{C}$.

We could also iterate this to obtain another fibration $\mathbf{C}^{pr^2}\to \mathbf{C}^{pr}$, where $\mathbf{C}^{pr^2}$ is the full subcategory of $\mathbf{C}^{\to\to}$ on projection sequences such as $A\times B\times C \to A\times B\to A$.

I don't know whether these things have a standard name, but I think I have heard them associated with the adjective "simple".

-
'Simple' is the term that Jacobs uses in his book -- he writes s(C) for your $C^{pr}$. –  Finn Lawler Jan 13 '12 at 18:40
Mh...that is not the simple fibration but a particular case of it (according to Jacobs). It is interesting for me anyway, it gives me some suggestions to work with. I was looking, however, for a fibration like this without pullbacks and it seems to be no possible. $C^{pr}$ has pullbacks as you say. Thank you anyway. –  Doctor Gibarian Jan 16 '12 at 16:13

I assume that by 'cartesian' you mean 'having cartesian products'. In that case the answer is no. You've more or less said this yourself: for $C^{\mathbf{3}} \to C^{\mathbf{2}}$ or the composite $C^{\mathbf{3}} \to C$ to be fibrations it is again necessary and sufficient that C have pullbacks.

The sequence makes perfect sense as a functor, of course, and the fibres are the same no matter what C looks like: an object over c is a composable pair of morphisms $\bullet \to \bullet \to c$ and a morphism is a 'square on top of a triangle'.

-