In his paper: "Calculate Categorically", Maarten Fokkinga invites readers to compare algebraic calculations with the usual pictorial proofs of category theory.
I would like to do just that, using "Elementary Categories, Elementary Toposes" (Colin McClarty) as the "usual" text.
McClarty presents Theorem 2.1 as: If P, $p_1$, $p_2$ is a product diagram for A and B, and there is an iso $f:Q \rightarrow P$, then Q, $p_1 \circ f$, $p_2 \circ f$ is also a product diagram for A and B.
My formulation of that theorem began by establishing the truth of Fokkinga's $(\vartriangle-TYPE)$, the instance of which for theorem 2.1 is:
$f;p_1:Q \rightarrow A \wedge f;p_2:Q \rightarrow B \Rightarrow f;p_1 \vartriangle f ; p_2 : Q \rightarrow A \times B $
But now I don't know what to do. Does establishing $(\vartriangle-TYPE)$ do enough to show that we have constructed a product for A and B? Studying McClarty's proof suggests that I need to do more, but I'm not sure what's next.
That you don't use the fact that $f$ is an isomorphism at all should be a strong indicator that you aren't finished. I think you might be misunderstanding what the theorem is saying. You already know there's a product, namely $A\times B$, for $A$ and $B$. What you want to show is that if $Q \cong A\times B$ then $Q$ is a product. For all of the constructs in "Calculate Categorically", the only result you need to establish is the CHARN (characterization) one. So, all you need to do is concretely define a $\vartriangle_Q$ which will produce an arrow into $Q$, and you need to show $\vartriangle$-CHARN with that $\vartriangle_Q$ and $exl = f;p_1$ and $exr = f;p_2$. That is you need to show: $$x;f;p_1 = h\ \land\ x;f;p_2 = k\ \iff\ x = h\vartriangle_Q k $$ To give you a start, the definition of $\vartriangle_Q$ is $$h \vartriangle_Q k \equiv h\vartriangle k;f^{-1}$$