Michael Shulman Beck-Chevalley condition > history

For any subobject $U$ of $B$, $g:C\to A$, $f:B\to A$, $q:C{\times}B\to A$ and $p:C{\times}B\to B$,

$g^{-1}\exists_{f}U=\exists_{q}p^{-1}U$

See Mac Lane and Moerdijk, section IV.9 (page 205).