I’ve recently learned about the curry howard isomorphism for dependent type theory, and I’m now interested in learning about how to capture this in category theory.
I believe that I understand how to frame propositional logic in category theory: Every proposition is an object, and a proof of a proposition is a morphism from $T$ to that object, and we assume the category is cartesian closed. $A$ implies $B$ is assumed as an axiom by positing a morphism from $T$ to the exponential object $B^A$. A conjunction between $A$ and $B$ is true if there is a morphism from $T$ to $A\times B$, and to the coproduct for a disjunction. A negation of a proposition $A$ is represented by a morphism from $A$ to type “bottom” which is uninhabited.
But I’m not sure how to represent universal quantifiers and existential quantifiers, and I couldn’t really understand the texts I found online.
Best Answer
Assuming you are interested only in the Curry-Howard-Lambek type of interpretations of logic in categories then in order to interpret first-order logic in a category cartesian closed categories are not sufficient.
The problem lies in the fact that you need a category whose objects represents not only propositions, i.e. closed formulas, but predicates as well (i.e. formulas with variables).
In order to do this one needs some sort of fibered categories (or indexed ones if you prefer).
We assume we have a logic signature made of an algebraic signature $\Sigma$, containing the operation symbols, and predicate signature $\Pi$, containing the predicate symbols.
For start one consider the category $T(\Sigma)$ whose objects sets of free variables and for every pair of such sets $X$ and $Y$ we have $$T(\Sigma)[X,Y]=\mathbf{Set}[X,T_\Sigma(Y)]$$ where $T_\Sigma(Y)$ is the set of terms with variables in $Y$. So morphisms of this category are substitutions for the logic signature considered.
To each $X \in T(\Sigma)$ we can associate the poset $P(X)$ of formulas with free variables in $X$, with order relations given by $\varphi \leq \psi$ iff $\varphi \vdash \psi$.
Also for every morphism/substitution $\sigma \in T(\Sigma)[X,Y]$ we have a monotone map $$P(\sigma)\colon P(X) \to P(Y)$$ defined as $P(\sigma)(\varphi)=\sigma(\varphi)$, that is the formula obtained by applying the substitution $\sigma$ to the formula $\varphi$.
These assignment define a functor $P\colon T(\Sigma) \to \mathbf{Cat}$, where we regard posets as categories and monotone functions as functors.
In this set up we can characterize quantifiers as adjoint functors, let see how.
For every $X$ set of variables and a new variable $x$ we have a morphisms $\pi_x^X \in T(\Sigma)[X,X\cup\{x\}]$ given by the substitution $$\pi_x^X \colon X \longrightarrow X\cup\{x\}$$ $$\pi_x^X(x)=x$$ for every $x \in X$.
The induced functor/monotone map $P(\pi_x^X)$ sends every proposition of $P(X)$ into itself seen as a member of $P(X\cup\{x\})$.
A left adjoint to $P(\pi_x^X)$ would be a functor $L_x^X \colon P(X \cup\{x\}) \to P(X)$, that takes formulas with free variables in $X\cup\{x\}$ and sends them in formulas with free variables in $X$ (pretty much as the quantifiers that eliminate free variables).
For $L_x^X$ to be an adjoint we need to have a natural isomorphism $$P(X)[L_x^X(\varphi),\psi]\cong P(X\cup\{x\})[\varphi,P(\pi_x^X)(\psi)]$$ and since we are dealing with posets this amounts to require that $$L_x^X(\varphi) \leq \psi \iff \varphi \leq P(\pi_x^X)(\psi)=\psi$$
This is equivalent to require that $L_x^X(\varphi)$ is a proposition whose logical consequences $\psi$ with free variables in $X$ are exactly those formulas that are implied by $\varphi$ in the extended context of $P(X\cup\{x\})$.
With a little effort one can show that such $L_x^X(\varphi)$ must be $\exists x \varphi$.
Similarly a right adjoining $R_x^X \colon P(X\cup\{x\}) \to P(X)$ would be a functor such that there is a natural isomorphism $$P(X\cup\{x\})[P(\pi_x^X)(\varphi),\psi]\cong P(X)[\varphi,R_x^X(\psi)]$$ Again, since we are dealing with posets, this amounts to require that $R_x^X(\psi)$ is the formula such that $\varphi \leq R_x^X(\psi)$ iff and only if $\varphi \leq \psi$, that is $R_x^X(\psi)$ is a logical consequence of $\varphi$ if and only if $\psi$ is a logical consequence of $\varphi$.
By playing a little bit with logic one can show that the only possibility is for $R_x^X(\psi)$ to be $\forall x \psi$.
If you are interested to some pointers I suggest to read Bart Jacobs' "Categorical Type Theory" that deals in details with these subject.
Note: usually authors use a different notation form the one I used here, for instance they usually deal with the category $T(\Sigma)$, nevertheless if you got the general idea I think you can easily fix the difference in notations.
I hope I was able to give you the raw idea, in case you needed any additional clarification please ask.