The Stacks project

It took me a little long to parse this proof so I will spell out the details for everyone's convenience: Suppose $\psi_1,\psi_2:x\rightrightarrows x'$ are morphisms in $\mathcal{X}_U$ such that $\rho=F_U\psi_1=F_U\psi_2:F_Ux\to F_Ux'$ in $\mathcal{Y}_U$. Write $y=Fx$ and let $\phi:\operatorname{id}_U^*y\to Fx$ be the induced strongly cartesian morphism (it lives in $\mathcal{Y}_U$). The object $y\in\mathcal{Y}_U$ induces a morphism $\mathcal{C}/U\to\mathcal{Y}$ of fibered categories over $\mathcal{C}$. Write $\phi'=\rho\circ\phi$. Then $\psi_1,\psi_2:(x,\phi)\rightrightarrows(x',\phi')$ are parallel morphisms in the fiber category of $(\mathcal{C}/U)\times_\mathcal{Y}\mathcal{X}$ over the object $\operatorname{id}_U$ of $\mathcal{C}/U$ (Lemma 4.42.1). But this fiber category is a setoid (Lemma 4.40.2), hence $\psi_1=\psi_2$.

The previous comment has an enhancement.

Lemma. Let $F:\mathcal{X}\to\mathcal{Y}$ be a $1$-morphism of categories fibred in groupoids over $\mathcal{C}$. The following are equivalent:

1. For every object $U$ in $\mathcal{C}$ and every $1$-morphism $\mathcal{C}/U\to\mathcal{Y}$ over $\mathcal{C}$, the category $\mathcal{X}\times_\mathcal{Y}\mathcal{C}/U$ is fibred in setoids over $\mathcal{C}/U$.

2. The functor $F_U:\mathcal{X}_U\to\mathcal{Y}_U$ is faithful for every object $U$ in $\mathcal{C}$.

Proof. 1$\Rightarrow$2. The proof is as in #11416.

2$\Rightarrow$1. In any case, we have that $\mathcal{X}\times_\mathcal{Y}\mathcal{C}/U$ is fibred in groupoids over $\mathcal{C}/U$ by Lemma 4.42.2. It is left to verify that the fibre category of $\mathcal{X}\times_\mathcal{Y}\mathcal{C}/U$ over an object $f:V\to U$ of $\mathcal{C}/U$ is thin (i.e., there is at most one morphism between any two given objects). Suppose then $\psi_1,\psi_2:(x,\phi)\rightrightarrows(x',\phi')$ are parallel morphisms in the fiber category of $(\mathcal{C}/U)\times_\mathcal{Y}\mathcal{X}$ over the object $f:V\to U$ of $\mathcal{C}/U$. Then $F(\psi_1)=\phi'\circ\phi^{-1}=F(\psi_2)$. Since $\psi_i$ belongs to $\mathcal{X}_V$, faithfulness of $F_V$ gives $\psi_1=\psi_2$. $\square$

Leaving as is.