Vrftjkry

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 $Atimes 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.

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 vatiables).

In order to do this one needs some sort of fibered categories (or indexed ones if you prefer).

The basic idea is the following: instead of having a category of propositions you have for any set of variables $X$, a category of formulas with free variables in $X$, and for every term substitution $sigma colon X to T_Sigma(Y)$ (where by $T_Sigma(Y)$ I mean the set of terms in a signature $Sigma$ and with variables in $Y$) we have a substitution functor between the categories indexed by $X$ and $Y$.

These data are required to satisfy some additional conditions that are needed to make all work out.

Without dealing with the details I can tell you this,
you clearly have and obvious substitution $X to X amalg {bullet}$ which adds a new variable to $X$, this substitution induces a functor between the categories associated to $X$ and $Xamalg{bullet}$ (which I remind are made of formulas with the appropriate variables). This functor basically send every formula with variables in $X$ in the same formula seen as a formula with variables in $X amalg {bullet}$.

This functor has both a left and right adjoint which are respectively the universal and existential quatifier: these adjoint functors take formulas in $X amalg{bullet}$-variables and give back formulas in $X$-variables.

Again the details require to know fibered or indexed categories at least, so I am not sure that a full answer can be given here.

If you are interested to some pointers I suggest to read Bart Jacobs' "Categorical Type Theory" that deals in details with these subject.

I hope I was able to give you the raw idea, in case you needed any additional clarification please ask.