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.

  • $\begingroup$ For the sake of completeness, did you check reference [8] mentioned in the paper? $\endgroup$ Jan 16, 2023 at 18:32
  • $\begingroup$ 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? $\endgroup$
    – Nico
    Jan 16, 2023 at 19:07
  • $\begingroup$ @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. $\endgroup$
    – Ilk
    Jan 16, 2023 at 19:20
  • $\begingroup$ @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. $\endgroup$
    – Ilk
    Jan 16, 2023 at 19:23
  • $\begingroup$ 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. $\endgroup$ Jan 21, 2023 at 16:20

1 Answer 1


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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .