Let $\mathscr C$ be a cartesian category with subobject classifier $\Omega$ and generic subobject $\tau:I\to\Omega$. Consider the following pullback square:
$\require{AMScd} \begin{CD} P @>{\bar f}>> C\\ @V{\bar g}VV @V{g}VV \\ A @>{f}>> B \end{CD}$
I proved that for any $p:A\to\Omega$ the statement $\exists_{\bar f}(p\circ\bar g)\implies \exists_f(p)\circ g$ is true.
What about the converse: $\exists_f(p)\circ g\implies\exists_{\bar f}(p\circ\bar g)$?
My attempts to prove it in such a category fails. On the other hand, it seems to be intuitively true in a topos.
What assumptions are necessary in order to make it true?
Note that a similar question arises for the universal quantificator. In particular, $\forall_f(p)\circ g\implies\forall_{\bar f}(p\circ\bar g)$ is true. On the other hand, I found a proof for the converse $\forall_{\bar f}(p\circ\bar g)\implies \forall_f(p)\circ g$ when $g$ is monic.
The equivalence $\exists_{\bar f}(p\circ\bar g)\iff \exists_f(p)\circ g$ means that the pullback preserve images. Thus that equivalence holds if and only if the categor is regular.