# Bootstrapping the Product Category

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?

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}