In the definition of predicative topoi by van den Berg we encounter the following definition of a collection square, for an ambient category that is assumed to be locally cartesian closed, lextensive and regular:
$$ \require{AMScd} \begin{CD} D @>{q}>> B \\ @V{g}VV @VV{f}V \\ C @>>{p}> A \end{CD} $$ A square as the one above will be called a collection square, if the following statement holds in the internal logic: for every $c \in C$ and cover $e : E \twoheadrightarrow$ $D_c$ there is a $c' \in C$ with $p(c) = p(c')$ and a map $h : D_{c'} → D_{c}$ over $B$ which factors through $e$.
Given such an external square of four morphisms how can I state this statement externally?
This is my first foray into translating a statement in internal logic to external logic, so maybe there are simpler examples that could illustrate all the connectives and quantifiers within this statement.
The translation is: for every morphism $c : T \to C$ and every cover $e : E \twoheadrightarrow D_c$, there exist a cover $t : T' \twoheadrightarrow T$, a morphism $c' : T' \to C$, and a morphism $h : D_{c'} \to D_c$ factoring through $e : E \twoheadrightarrow D_c$, where $D_c$ and $D_{c'}$ are defined by the following pullback squares, $$\require{AMScd} \begin{CD} D_c @>{d}>> D \\ @V{g_c}VV @VV{g}V \\ T @>>{c}> C \end{CD} \qquad \begin{CD} D_{c'} @>{d'}>> D \\ @V{g_{c'}}VV @VV{g}V \\ T' @>>{c'}> C \end{CD} $$ such that $p \circ c \circ t = p \circ c'$ and $q \circ d \circ h = q \circ d'$.
Frankly, this is not an appropriate first exercise in interpreting internal logic. Even for experts it is a bit tricky.