It's my understanding that category theory can be used as a foundation of mathematics, and that it is not dependent on set theory in that respect. My question is about exactly how products come about.

The "universal" definition of products says that for $a,b \in C$, they have a product $a\times b$ if there's two arrows $\pi_1: a\times b \to a,\ \pi_2: a\times b \to b$ such that for any object $c$ with arrows $f: c\to a, g : c\to b$ there's a unique arrow $h: d\to a\times b$ making everything commute.

The formal basis for universal constructions like this is the definition of a functor and a limit. Specifically we take an index category $J = \cdot \leftarrow \cdot \rightarrow \cdot$ and let the limit be the right adjoint of the generalized diagonal functor $\Delta : C \to C^J $. In other words, we use exponentiation of a category to define products. But the category exponent requires category products first.

So... we need to define categories on the higher-level abstraction before we define them on the lower level. But then where does "product" come from? Is it just some meta-concept, or is there a more minimal way to develop it?


The typical way to set up a "foundation" is via an axiomatic approach, the most famous example, of course, being ZFC. For a variety of philosophical and technical reasons, this will usually be a axiomatization in (some variant of) first-order logic.

While many categorical approaches to characterizing concepts are not presented in a first-order manner, it's not unusual that they can be presented in a first-order manner. So the characterization of categorical products in terms of representability is not patently first-order but the characterization of categorical products in terms of universal arrows ("universal properties") is given a fairly standard axiomatization of the notion of a category. So you simply take the universal properties as axioms. This nLab page describes an axiomatization of ETCS (the elementary theory of the category of sets) which includes axiomatizing categorical products, or in this particular axiomatizations case, pullbacks and a terminal object.

Simplifying the axioms there for pullbacks to products (which are just pullbacks along arrows into the terminal object) and using their notation and conventions produces (if I didn't make a mistake): $$\begin{align}a=s(a),b=s(b)\vdash\exists_h\exists_k\forall_{h'}\forall_{k'}&((t(h')=a\land t(k')=b \land s(h')=s(k'))\\&\Rightarrow \exists!_j(c(h,j,h')\land c(k,j,k')))\end{align}$$ The postulated $h$ and $k$ correspond to the categorical product, in particular to the projection $\pi_1$ and $\pi_2$. This particular axiomatization uses an arrows-only formulation of category theory so there is no product object, instead the identity arrow $s(h) = s(k)$, corresponding to the source of $h$ and $k$, represents the object.

In something like FOLDS, you would have an axiom like: $$\begin{align}A,B:\mathsf{Ob}\vdash\ &\exists P:\mathsf{Ob}.\exists h:\mathsf{Hom}(P,A).\exists k:\mathsf{Hom}(P,B).\\&\forall X:\mathsf{Ob}.\forall h':\mathsf{Hom}(X,A).\forall k':\mathsf{Hom}(X,B).\\&\exists!j:\mathsf{Hom}(X,P).h'=h\circ j \land k' = k\circ j\end{align}$$

See the ETCC nLab page for references to similar approaches for axiomatizing the category of categories or the 2-category of categories. These have been less influential than ETCS which itself is not that influential.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.