How are existential quantifiers present in the internal logic of regular categories?

Question

Intuitively speaking, how do existential quantifiers appear?

I'm just starting to get familiar with these definitions.

Top and conjunctions appear because of finite products. (Plus, I assume, something that makes them work nicely with the existential quantifiers.)

But my understanding of existential quantifiers in categorical terms is by way of them being left adjoint to weakening.

Answer 1

The internal logic of a regular category is talking about the logic of its subobject fibration, $p : \mathsf{Sub}_C → C$. I think for later purposes, it's easiest to think about this case using two related structures:

1. The codomain fibration on $C$ is the functor $\mathsf{cod} : C^→ → C$ mapping each arrow to its codomain
2. The subobject fibration is equivalent to the subfibration of $\mathsf{cod}$ containing only monomorphisms in the 'over' category

For both of these, given the projection map $π : Γ×A → Γ$, there is a weakening functor $π^*$ (given by pullback), with a type like $C/Γ → C/Γ×A$ or $\mathsf{Sub}_C(Γ) → \mathsf{Sub}_C(Γ×A)$, and we want to interpret existential quantifiers as left adjoints to this.

I think it's easiest to see what the regular structure does in two steps. If we start with a monomorphism $s : S \hookrightarrow Γ×A$, we can consider it as an object of the codomain fibration. Then the left adjoint to weakening is the disjoint union functor, given by the postcomposition $π \circ s : S → Γ$.

However, this is generally no longer a monomorphism/subobject. If you imagine there are 'elements' involved, then the fiber over $γ : Γ$ has all the elements that were originally over $(γ,a) : Γ×A$. There can be only one element for each $a$, but if $A$ has multiple elements there can be multiple elements over $γ$.

So, to get a subobject we need to crush the $π \circ s$ family down to a monomorphism, and this is done by factoring through the image in the regular category $C$. The factorization looks like:

$$S \twoheadrightarrow T \hookrightarrow Γ$$

And then the monomorphism $T \hookrightarrow Γ$ gives the subobject of $Γ$ corresponding to the existential. The regular category structure comes in because the image is the coequalizer of the kernel pair (if you're defining them like the nlab does).

The last rule of a regular category ensures that these existential quantifiers satisfy the Beck-Chevalley condition, so they are stable under substitution in the internal logic (pullback/reindexing of the fibration).