Having used the symbols ∃ and ∀, we are obliged to justify them in terms of the rules of natural deduction, or at least their categorical interpretation [Tay99, §§9.3–4] as we don’t want to get too heavily involved in syntax. In particular, the ability to substitute under a quantifier is another consequence of insisting that the adjunctions be internal.
[The letter E is used in the following two results to suggest an existential quantifier, not a nucleus.]
Proposition 8.1
If Σ^{!}:Σ→Σ^{X} has a left (or right) adjoint
then Σ^{p1}:Σ^{Y}→Σ^{X× Y} also has one,
and this automatically satisfies the Beck–Chevalley condition,
the pullbacks in question being given by product projections
as shown on the left below.
Proof If E⊣Σ^{!} then F≡ E^{Y}⊣Σ^{p1} by Lemma 3.6.
Explicitly, for ω∈Σ^{X× Y}, put F(ω)≡ λ y.E(λ x.ω(x,y)); then for ψ∈Σ^{Y},
F(Σ^{ p1}(ψ))= λ y.E(λ x.ψ y)=λ y.EΣ^{!}(ψ y) ⊑λ y. ψ y = ψ, 
whilst ω(x,y)⇒Σ^{!} E(λ x′.ω(x′,y)) ⇔ F(Σ^{ p1}ω)(y).
The Beck–Chevalley condition is naturality of E^{(−)}:Σ^{X×(−)}→Σ^{(−)} with respect to f. Explicitly, ω↦λ z.E(λ x.ω(x, fz)) both ways round the square involving F and G≡ E^{Z}. ▫
The preceding proof only required Σ to be exponentiating: the Euclidean principle comes into the next result.
Proposition 8.2 For X overt,
every product projection p_{1}:X× Y→ Y is preopen, because
Proof
Definition 7.7 required E to be monotone, so F(σ)⇒ E(Σ^{!}σ)⇒ σ. Then
E(φ∧Σ^{!}σ)⇔ F(σ)⇔ F(σ)∧ σ⇔ F(⊤)∧ σ⇔ E(φ)∧ σ 
by the Euclidean principle.

▫
Proposition 8.3
By analogy with Proposition 6.11,
Proof [a] ∃_{1}≡ ∀_{1}≡ id_{Σ}. [b] ∃_{X× Y}≡ ∃_{X}·∃_{Y}^{X}≡ ∃_{Y}·∃_{X}^{Y}. [c,d] U↪ X→1 is a composite of open or proper maps. ▫
[Beware that the letter I in the following two results denotes an “indexing object” not a Σsplitting.]
Corollary 8.4 If the object I is overt then
every algebra (A≡ Σ^{X}) has internal Iindexed joins,
∧ distributes over them and they are preserved by homomorphisms.
Dually, if I is compact then algebras have and homomorphisms preserve Iindexed meets.
Proof These are restatements of the Frobenius and Beck–Chevalley conditions. ▫
Corollary 8.5
Now let’s think a bit about syntax, using [Tay99, §9.3].
Remark 8.6
Our category is a model of a fragment of predicate calculus
in which each object names a (nondependent) type, and contexts are products
(cf. Theorem 4.2).
Each open inclusion U↪ X is a predicate x:X⊢φ(x) prop,
though we prefer to regard φ(x) as a generalised element of Σ^{X},
rather than as a mono.
Thus we interpret

The effect of pullback Σ^{p0}≡ p_{0}^{*} along a product projection p_{0}:Γ× X→Γ is to add a variable x to the context (weakening, which is written x^{*} in [Tay99]):
If X is overt then this map Σ^{p0} has a left adjoint ∃_{X}:Σ^{X}→Σ or ∃_{p0}:Σ^{Γ× X}→Σ^{Γ}, which interprets existential quantification:
The Beck–Chevalley condition is needed to ensure that, for any function f:Γ→Δ between types, the bijective correspondence on the right is preserved by Σ^{f} (substitution or cut along f), whilst the Frobenius law provides in a similar way for additional predicates that may be present in the context.
Remark 8.7
In Section 10 we shall encounter expressions of the forms
∃_{i}· Σ^{i} · Σ^{p0}, ∃_{p1}·∃_{i}· Σ^{i} · Σ^{p1} and ∃_{p1}·∃_{i}· Σ^{i} · Σ^{p0} 
where i:R↪ X× Y is the inclusion of an open binary relation classified by ρ:X× Y→Σ. Recall from Section 3 that ∃_{i}· Σ^{i} ≡ρ∧(−), so it takes
Γ, x:X,y:Y⊢ψ(x,y) to Γ, x:X,y:Y⊢ρ(x,y)∧ψ(x,y) 
without changing the context. Hence the effect on Γ, x:X⊢φ(x) prop of

▫
This brief discussion of the rules of natural deduction and Corollary 10.11 about the direct image show logicians and categorists respectively that we are using the existential quantifier in the usual way. However, the dual of the Euclidean principle implies the dual Frobenius law for ∀_{X}, which is something extra on top of the standard rules for the universal quantifier [Tay99, §9.4], namely that Σ^{!}⊣∀_{X} with the Beck–Chevalley condition.
Remark 8.8
Let φ∈Σ^{X} be a decidable predicate on any overt compact object,
so ∀ x.(φ(x)∨ψ(x)), where ψ≡ ¬φ∈Σ^{X}.
Then we have ∀ x.(φ(x)∨∃ y.ψ(y)),
which is equivalent by the dual Frobenius law to
(∀ x.φ(x))∨(∃ y.ψ(y)).
For decidable predicates on ℕ, this property is well known in recursion theory as the Markov principle [Mar47] [Ros86, §5.1].
For us it is not legitimate to write “∀ n:ℕ.φ(n)” because ℕ is not compact in topology or recursion (Remark 7.11). But consider its onepoint compactification, ℕ_{∞}; both ℕ and ℕ_{∞} are (intended to be) overt, and the inclusion i:ℕ↪ℕ_{∞} is dense in the sense that (∃ x:ℕ_{∞}.ψ(x))⇔ (∃ n:ℕ.ψ(i n)). Although ℕ is not compact, if ⊤⇔ ∀ x:ℕ_{∞}.φ(x)∈Σ then Σ^{i}φ=⊤∈Σ^{ℕ}. Conversely, we may transfer Σpredicates from ℕ to ℕ_{∞}, but we cannot, unfortunately, do the same with decidable ones without prejudging the question for the extra point ∞∈ X. ▫
We have a more encouraging result when we compare our universal quantifier for closed subsets with the standard one for all subsets in a topos. The following situation arises in synthetic domain theory (Remark 2.13), for the sheaves for a Lawvere–Tierney topology (Σ≡ Ω_{j} in Example 2), and also for Ω↠Υ in Example 6.14 since this map is actually also mono.
[Eduardo Dubuc and Jacques Penon [DP86] called an object K of a topos compact if its universal quantifier ∀_{K} satisfies the dual Frobenius law.]
Proposition 8.9
Suppose that Σ is an object that satisfies the Euclidean principle
in a topos, so Σ classifies certain open subsets,
whilst Ω classifies all subsets.
If the object X is compact with respect to Σ then
the interpretations of ∀_{X} with respect to Σ and Ω agree,
in the sense that the bottom face of the cube commutes:
Proof To prove that the two routes Σ^{X}→Ω are equal, it is enough to show that they both classify the Ωsubobject {λ x.⊤}⊂Σ^{X}. The front and back faces of the cube are pullbacks by Proposition 7.10, as is the right face because Σ→Ω is mono by Remark 2.13. To show that the left face is also a pullback, consider any test Γ; the two routes Γ⇉Ω^{X} are equal iff the square on the right commutes, which it does iff ∼φ=λ x.⊤, as required. ▫
Remark 8.10 Of the other meanings that we might attribute to saying that
the two notions of ∀ agree,
one is trivially true in that Σ^{X}≅Σ^{X},
where X is the replete reflection of X,
and another is trivially false in that every object is compact with respect
to Ω, but not necessarily with respect to Σ.
Remark 8.11
It is not possible to adapt this argument to ∃ and ⊥
because, without excluded middle,
characteristic maps with respect to ⊥:1→Ω in a topos
need not be unique.
An analogous result can nevertheless be achieved
by imposing the open cover Lawvere–Tierney topology on the topos,
but discussion of this relies on sheaftheoretic methods,
which are inappropriate for this paper.