# How to translate a statement from internal to external logic?

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.

• For the sake of completeness, did you check reference [8] mentioned in the paper? Jan 16, 2023 at 18:32
• the statement seems to contain some dependent type theory (looking at the fiber over c :C), and it seems to quantify over types (the E). what does "cover" mean internally in that context?
– Nico
Jan 16, 2023 at 19:07
• @MartinBrandenburg in [8] there is a similar definition 2.3 but in category of sets, I should probably edit that in the paper i am talking about, the ambient category is assumed to be lcc, lextensive and regular.
– Ilk
Jan 16, 2023 at 19:20
• @Nico That's confusing me too as before that there is a definition 3.1 of a covering square, but as far as i can tell it uses external logic to define what it means.
– Ilk
Jan 16, 2023 at 19:23
• I believe that Table 4.2 in these notes of mine might be useful. It spells out a fragment of the internal language in the special case of sheaf toposes over topological spaces. The case of arbitrary Grothendieck toposes is very similar. Jan 21, 2023 at 16:20

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'$$.