Composing duplication and projections

Question

Suppose I have a cartesian closed category $\mathcal{C}$ with projection $(\pi_1)_{A \times B} : A\times B \to A$, duplication $\delta_{A} : A \to A \times A$ and associator $\alpha_{A,B,C} : (A \times B) \times C \to A \times (B \times C)$.

Does the following commute ?

$$ \require{AMScd} \begin{CD} A \times B @>{\delta_A \times id_B }>> (A \times A) \times B \\ @V\delta_{A \times B}VV @VV{\alpha_{A,A,B}}V \\\ (A \times B) \times (A \times B) @>{(\pi_1)_{A\times B} \times id_{A \times B}}>> A \times (A \times B) \end{CD} $$

It seems to me obvious that it should, but I can't prove it!

Answer 1

You don't need closure, a cartesian category is fine.

The big hammer approach is to note that the internal language of cartesian categories looks and feels like (multi-sorted) Universal Algebra, i.e. an arrow $A\times B \times C \to D$ can be thought of as a term with three variables of sort $A$, $B$, and $C$. That is, you have terms like $x:A, y:B, z:C \vdash \mathtt{f}(\mathtt{g}(x,x,y),\mathtt{h}(z))$. An arrow $A\times B\times C \to D\times E$ is just a tuple of terms. The upshot is that you can use essentially "normal" mathematical notation, in normal ways, as long as you only use it in certain, fairly obvious ways, and what it says will correspond to statements that are true. If you insist on cartesian closure, you can further use the simply typed lambda calculus with products, making even more "normal" mathematical operations allowable, namely currying and passing functions as parameters.

Of course, if you wanted to prove the above statements you'd need to be able to handle situations like the one you are asking about. The trick here is that you are treating $\delta$ and $\alpha$ as primitives, but they are definable in terms of the projections and tupling which is $\langle -,=\rangle_{ABC} : \text{Hom}(A,B)\times\text{Hom}(A,C)\to\text{Hom}(A,B\times C)$. In particular, we have the universal property: $$\pi_i \circ \langle f_1,f_2\rangle = f_i \quad \text{and}\quad \langle\pi_1 \circ t,\pi_2\circ t\rangle = t$$ We can define $\delta \equiv \langle id,id\rangle$, $f\times g \equiv \langle f\circ\pi_1,g\circ\pi_2\rangle$, and $\alpha \equiv \langle id\times\pi_1,\pi_2\circ\pi_2\rangle$. You can now just expand the definitions and apply the equations provided by the universal property. To be systematic about it, to prove $h = k : A \to B\times C$, you simply need to prove $\pi_i \circ h = \pi_i \circ k$ for $i = 1,2$ (because then we can use the second equation in the universal property to show $h = k$). You can apply this multiple times until you get a collection of equations of the form $A \to B$ where $B$ is not a product. At this point you can systematically apply the first (pair of) equation(s) of the universal property until all uses of $\langle -,=\rangle$ are gone. The process is completely mechanical. If you're a programmer, you could make a little simplifier to do it for you. It would be a fairly straightforward exercise.

Answer 2

First, observe that $\alpha = \langle \pi_1 \circ \pi_1, \pi_2 \times \mathrm{id} \rangle$ and $\delta = \langle \mathrm{id}, \mathrm{id}\rangle$.

We have the following equalities:

1. $\langle f , g \rangle \circ h = \langle f \circ h , g \circ h \rangle$
2. $\pi_i \circ (f_1 \times f_2) = f_i \circ \pi_i$
3. $\pi_i \circ \langle f_1, f_2 \rangle = f_i$
4. $(f_1 \times f_2) \circ (g_1 \times g_2) = (f_1 \circ g_1) \times (f_2 \circ g_2)$

\begin{align*} \alpha \circ (\delta \times \mathrm{id}) &= \langle \pi_1 \circ \pi_1, \pi_2 \times \mathrm{id} \rangle \circ (\delta \times \mathrm{id}) \tag{Def .of $\alpha$}\\ &= \langle \pi_1 \circ \pi_1 \circ (\delta \times \mathrm{id}), (\pi_2 \times \mathrm{id})\circ (\delta \times \mathrm{id}) \rangle \tag{By 1.}\\ &= \langle \pi_1 \circ \pi_1 \circ (\langle \mathrm{id}, \mathrm{id}\rangle \times \mathrm{id}), (\pi_2 \times \mathrm{id})\circ (\langle \mathrm{id}, \mathrm{id}\rangle \times \mathrm{id}) \rangle \tag{Def. of $\delta$}\\ &= \langle \pi_1 \circ \langle \mathrm{id}, \mathrm{id}\rangle\circ \pi_1 , (\pi_2 \times \mathrm{id})\circ (\langle \mathrm{id}, \mathrm{id}\rangle \times \mathrm{id}) \rangle \tag{By 1.}\\ &= \langle \pi_1 \circ \langle \mathrm{id}, \mathrm{id}\rangle\circ \pi_1 , ((\pi_2 \circ \langle \mathrm{id}, \mathrm{id}\rangle) \times \mathrm{id}\rangle \tag{By 4.}\\ &= \langle \mathrm{id} \circ \pi_1 , \mathrm{id} \times \mathrm{id}\rangle \tag{By 3.}\\ &= \langle \pi_1 , \mathrm{id}\rangle\\ &= (\pi_1 \times \mathrm{id}) \circ \delta \end{align*}