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



Equivalence of definitions of cartesian morphisms
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$.


