categorical interpretation of quantification
There are two concepts in category theory that correspond to $\land$ and $\lor$:
- (Binary) categorical products and coproducts, as you mention.
- Meets and joins as operations on the subobjects of a given object (satisfying the Beck-Chevalley condition).
Similarly, there are two ways to express logical quantifiers as categorical notions. In the following I assume a category $\mathcal{C}$ which has whatever structure is necessary to make sense of what I am saying (I can be more precise if needed).
For every arrow $f : A \to B$ there is a pullback functor $f^{*} : \mathcal{C}/B \to \mathcal{C}/A$ which takes an arrow $g : D \to B$ to its pullback $f^{*}(g) : f^{*}(D) \to A$ along $f$. Here $\mathcal{C}/X$ is the slice category over $X$. There is another functor $\Sigma_f : \mathcal{C}/A \to \mathcal{C}/B$ defined on an object $h : E \to A$ as $\Sigma_f(h) = f \circ h$. Then $\Sigma_f$ is left adjoint to $f^{*}$. Sometimes $\mathcal{C}$ is such that $f^{*}$ also has a right adjoint $\Pi_f$ of $f^{*}$. When such structure exists, $\mathcal{C}$ is said to be locally cartesian closed. The existential quantifier corresponds to $\Sigma_f$ and the universal one to $\Pi_f$. More precisely, universal quantification $\forall x \in X . \phi(x, y)$ corresponds to $\Pi_{\pi_1}(\phi)$ where $\pi_1 : X \times Y \to Y$ is the first projection and $\phi : Z \to X \times Y$.
There is a subobject functor $\mathsf{Sub} : \mathcal{C}^{\mathrm{op}} \to \mathsf{Poset}$ which takes an object $A$ to the poset of its subobjects and an arrow $f : A \to B$ to the monotone map $f^{*} : \mathsf{Sub}(B) \to \mathsf{Sub}(A)$ which takes a subobject represented by a mono $m : X \to B$ to the subobject represented by $f^{*}(m) : f^{*}(X) \to A$, the pullback of $m$ along $f$. When the posets $\mathsf{Sub}(A)$ are (distributive) lattices, we can interpret $\land$ and $\lor$ as meets and joins. To interpret the quantifiers we again ask for the left and right adjoints of $f^{*}$. The left adjoints exist when $\mathcal{C}$ has stable image factorizations, and these give the existential quantifiers. The right adjoints give the universal quantifiers. There is a little detail called the Beck-Chevalley condition which requires that the adjoints are stable under pullbacks. (In logic the condition corresponds to the fact that substitution commutes with quantifiers.)
We can also express the inference rules for quantifiers in a form that makes it obvious that they are adjoints. Consider the following rule: $$\frac{x : X, y : Y \mid \phi \vdash \psi}{y : Y \mid \phi \vdash \forall x : X . \psi}$$ This says: "if $\phi$ entails $\psi$, where $x$ and $y$ are free variables of type $X$ and $Y$ respectively, then $\phi$ entails $\forall x : X . \psi$ with free variable $y : Y$." (Note that $x$ cannot occur free in $\phi$ because $\phi$ appears on the bottom line in a context where only the free variable $y$ is allowed.) This is the introduction rule for $\forall$. But we can turn it around to get the elimination rule: $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi}{x : X, y : Y \mid \phi \vdash \psi}$$ This is not the elimination rule as usually stated, which is $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi \qquad a : X}{y : Y \mid \phi \vdash \psi[a/x]},$$ but we can obtain this one from ours by using the rule of substitution: from $\forall x : X . \psi$ first derive $\psi$, and then substiute $a$ for $x$.
Now to be completely precise, we should consider $\phi$ above the line to be different from the one below the line because one appears in the context with variables $x : X$ and $y : Y$, and the other in the context with just $y : Y$. So let us write $[x]^{*}(\phi)$ for the formula $\phi$ considered in the context with the variable $x$ added to it (this is known as weakening in logic, although here we are adding stuff to the typing context, whereas in logic there is also weakening that adds hypotheses). With this notation our rules read as $$\frac{x : X, y : Y \mid [x]^{*}(\phi) \vdash \psi}{y : Y \mid \phi \vdash \forall x : X . \psi}$$ and $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi}{x : X, y : Y \mid [x]^{*}(\phi) \vdash \psi}.$$ But this has the form of an adjunction between $[x]^{*}$ and $\forall x : X$! We also see the correspondence between logic and categories clearly now: weakening $[x]^{*}$ corresponds to pullback along the projection $\pi_1 : X \times Y \to X$, and $\forall x : X$ corresponds the functor $\Pi_{\pi_1}$.
I leave it as an exercise for you to figure out how the existential is a left adjoint to weakening. So the moral of the story is that universal and existential quantifiers are rigth and left adjoints of weakening.
References:
- Steve Awodey: Category theory, Oxford University Press. This has a nice and easy explanation of what I wrote above.
- Bart Jacobs: Categorical Logic and Type Theory. This is nuclear weapons, it contains everything and more about the subject, including generalizations that unify the above two views.
The analogue of existential quantification is the dependent sum, and the analogue of universal quantification is the dependent product. The analogy itself passes through the Curry-Howard correspondence.
A simple categorical description of quantification is the following. In a category with pullbacks, any morphism $f : x \to y$ induces a functor $f^{\ast} : \text{Sub}(y) \to \text{Sub}(x)$ from the category of subobjects of $y$ to the category of subobjects of $x$ by taking pullbacks. In a category with finite products, and when they exist, the existential quantifier is the left adjoint to the functor $\text{Sub}(x) \to \text{Sub}(x \times y)$ induced by a projection map $\pi_x : x \times y \to x$, and the universal quantifier is the right adjoint, thinking of $\text{Sub}(x)$ as being described by predicates over $x$ (although strictly speaking we need a subobject classifier to do this).
See also Heyting category and dependent type theory.
Here's a simple-minded version of the basic point here, put in terms of Galois connections.
Let $L$ be a first-order language, and $\mathit{Form}(\vec{x})$ be the set of $L$-wffs with at most the variables $\vec{x}$ free.
Write $\phi(\vec{x})$ for a formula in $Form(\vec{x})$, $|\phi(\vec{x})|$ for the class of formulae logically interderivable with $\phi(\vec{x})$, and $E_{\vec{x}}$ for the set of such equivalence classes of formulae from $\mathit{Form}(\vec{x})$.
Put $|\phi(\vec{x})| \Rightarrow |\psi(\vec{x})|$ iff $|\phi(\vec{x})| \vdash |\psi(\vec{x})|$. Then $\Rightarrow$ is a partial order on $E_{\vec{x}}$.
Now we'll consider two maps between the posets $(E_{\vec{x}}, \Rightarrow)$ and $(E_{\vec{x}, y}, \Rightarrow)$. In other words, we are going to be moving between (classes of) formulae with at most $\vec{x}$ free, and formulae with at most $\vec{x}, y$ free (where $y$ isn't among the $\vec{x}$).
First, since every wff with at most the variables $\vec{x}$ free also has at most the variables $\vec{x}, y$ free, there is a trivial map $f_*$ that sends $|\phi(\vec{x})| \in E_{\vec{x}}$ to the same element $|\phi(\vec{x})| \in E_{\vec{x}, y}$.
Second, we define the companion map $f^*$ that sends $|\phi(\vec{x}, y)| \in E_{\vec{x}, y}$ to $|\forall y\,\phi(\vec{x}, y)| \in E_{\vec{x}}$.
Then $(f_*, f^*)$ is a Galois connection between $E_{\vec{x}}$ and $E_{\vec{x}, y}$. That is to say
$f_*(|\phi(\vec{x})|) = |\psi(\vec{x},y)|\quad$ if and only if $\quad|\,\phi(\vec{x})\,| = f^*(|\psi(\vec{x},y)|)$
For that just restates the familiar logical rule
$\phi(\vec{x}) \vdash \psi(\vec{x},y)\quad$ iff $\quad\phi(\vec{x}) \vdash \forall y\,\psi(\vec{x},y)$
Hence universal quantification is right-adjoint to a certain quite trivial operation. (There's an analogous result for existentials.)
I've accepted Andrej Bauer's answer as it is the most thorough, provides references, and, especially with the explanations in the comments, has made this topic much clearer. Different references have been provided in the various answers, and in case future users have additional references, I though it would be useful add a community wiki answer listing the various references.
- Steve Awodey: Category theory, Oxford University Press. This has a nice and easy explanation of the material in Andrej Bauer's answer.
- Bart Jacobs: Categorical Logic and Type Theory. This is nuclear weapons, it contains everything and more about the subject, including generalizations that unify the above two views.
- Goldblatt, R. (2006). Topoi: the categorial analysis of logic (Vol. 98). Courier Dover Publications. Goldblatt approaches category theory from the standpoint of logic, so those more acquainted with logic than category theory may appreciate this text. (Additionally, the same might do well to read Peter Smith's answer before reading Andrej Bauer's answer; it will provide some intuition for the categorical generalization.)