# Equivalence of definitions of cartesian morphisms

Let $p: C\to D$ be a functor, and let $f:y\to x$ be a morphism of $C$. We say that $f$ is cartesian if the canonical map $Q:(C\downarrow f) \to P:=(C\downarrow x)\times_{(D\downarrow p(x)} (D\downarrow p(f))$ is a surjective (on objects) equivalence of categories. However, if we write out what the (strict 2-) pullback means, the objects are precisely the pairs of morphisms $g: z\to x$ and $h:p(z)\to p(y)$ such that $p(g)=p(f) \circ h$. If we look at the fibres of $Q$ over objects of $A$, we see that that they are contractible groupoids.

Using the more common definition of a cartesian morphism, we must show that any pair of morphisms $(g, h)$ as above uniquely determines an arrow $\ell:z\to y$ such that $f\circ \ell= g$ and $p(\ell)=h$.

I see how the first definition implies the existence of such a map, but how does it determine the map's uniqueness (up to more than a contractible space of choices)?

-

The only morphisms in the fibers of $Q$ are identity maps, so it is actually an isomorphism of categories. To see this, suppose $\ell,\ell'\colon z\to y$ both induce $g\colon z\to y$. What would a morphism from $\ell$ to $\ell'$ in the fiber of $Q$ be? It would be a morphism $\varphi\colon z\to z$ over $y$ (the first $z$ is over $y$ via $\ell$ and the second via $\ell'$) which induces the identity morphism on $g$ in $(C\downarrow x)$. But $\varphi$ induces the morphism

    φ
z ----> z
\     /
g\   /g
v v
x


The only way this is the identity morphism of $g$ is if $\varphi=id_z$.

-
That's what I thought as well, but the nLab says that it only needs to be a surjective equivalence (a trivial fibration in the natural model structure). ncatlab.org/nlab/show/Cartesian+morphism . In fact, I asked a similar question earlier on the nForum where I raised the same issue math.ntnu.no/~stacey/Vanilla/nForum/… . I agree with you, but maybe someone can explain why the definition on the nForum is so strange? Does it give a good definition for weakly cartesian morphisms? – Harry Gindi Aug 29 '10 at 8:38
I think, as you say, the motivation for the strange phrasing is to weaken well. As Anton shows, the two versions are equivalent in this setting — “surjective equivalence” implies “isomorphism” — so just looking at this case, it'd seem more natural to use the simpler phrasing of “isomorphism”. But if in higher-dimensional/weakened generalisations the general concept needed is “trivial fibration”, that would be an argument for using it here, slightly harder to understand but more principled. – Peter LeFanu Lumsdaine Aug 29 '10 at 17:58