[proofplan]
We construct the mediating map by sending each $c:C$ to the ordered pair $(f(c),g(c))$. The product beta laws show, pointwise, that its two projection composites are $f$ and $g$; function extensionality upgrades these pointwise equalities to equalities of functions when needed. For uniqueness, any other map $h:C\to A\times B$ with the same projections is pointwise equal to the constructed pairing by the product eta principle and the assumed projection equalities. A final use of function extensionality gives equality of the two maps.
[/proofplan]
[step:Construct the pairing map from the two component maps]
Let $f:C\to A$ and $g:C\to B$ be functions. Define the function
\begin{align*}
\langle f,g\rangle:C\to A\times B
\end{align*}
by the rule
\begin{align*}
\langle f,g\rangle(c)=(f(c),g(c))
\end{align*}
for each $c:C$.
For every $c:C$, the first product beta law gives
\begin{align*}
(\pi_1\circ\langle f,g\rangle)(c)=\pi_1((f(c),g(c)))=f(c).
\end{align*}
Thus $\pi_1\circ\langle f,g\rangle$ and $f$ are pointwise equal. By the assumed [function extensionality principle](/theorems/9638), if equality of functions is propositional, this pointwise equality induces
\begin{align*}
\pi_1\circ\langle f,g\rangle=f.
\end{align*}
Similarly, for every $c:C$, the second product beta law gives
\begin{align*}
(\pi_2\circ\langle f,g\rangle)(c)=\pi_2((f(c),g(c)))=g(c).
\end{align*}
By function extensionality, this pointwise equality induces
\begin{align*}
\pi_2\circ\langle f,g\rangle=g.
\end{align*}
Therefore $\langle f,g\rangle$ is a function with the required two projection composites.
[/step]
[step:Show that any map with the same projections is pointwise equal to the pairing]
Let $h:C\to A\times B$ be a function such that
\begin{align*}
\pi_1\circ h=f
\end{align*}
and
\begin{align*}
\pi_2\circ h=g.
\end{align*}
Fix $c:C$. The product eta principle applied to the element $h(c):A\times B$ gives
\begin{align*}
h(c)=(\pi_1(h(c)),\pi_2(h(c))).
\end{align*}
Applying the equality $\pi_1\circ h=f$ at the argument $c$ gives
\begin{align*}
\pi_1(h(c))=f(c).
\end{align*}
Applying the equality $\pi_2\circ h=g$ at the argument $c$ gives
\begin{align*}
\pi_2(h(c))=g(c).
\end{align*}
Substituting these two equalities into the eta equality yields
\begin{align*}
h(c)=(f(c),g(c)).
\end{align*}
By the definition of $\langle f,g\rangle$, this is
\begin{align*}
h(c)=\langle f,g\rangle(c).
\end{align*}
[guided]
We now prove uniqueness at a single input $c:C$, because equality of functions will later be obtained from pointwise equality by function extensionality. Let $h:C\to A\times B$ be another candidate map, and suppose it has the same two components as the constructed pairing:
\begin{align*}
\pi_1\circ h=f
\end{align*}
and
\begin{align*}
\pi_2\circ h=g.
\end{align*}
The reason products are unique is the eta principle: an element of a product is determined by its two projections. Applying product eta to the particular element $h(c):A\times B$ gives
\begin{align*}
h(c)=(\pi_1(h(c)),\pi_2(h(c))).
\end{align*}
The assumptions on $h$ identify these two projections. Evaluating the equality $\pi_1\circ h=f$ at $c$ gives
\begin{align*}
\pi_1(h(c))=f(c).
\end{align*}
Evaluating the equality $\pi_2\circ h=g$ at $c$ gives
\begin{align*}
\pi_2(h(c))=g(c).
\end{align*}
Substituting these component equalities into the eta expansion of $h(c)$ gives
\begin{align*}
h(c)=(f(c),g(c)).
\end{align*}
But the constructed map $\langle f,g\rangle:C\to A\times B$ was defined by
\begin{align*}
\langle f,g\rangle(c)=(f(c),g(c)).
\end{align*}
Therefore
\begin{align*}
h(c)=\langle f,g\rangle(c).
\end{align*}
This proves pointwise equality of $h$ and $\langle f,g\rangle$ at the arbitrary input $c:C$.
[/guided]
[/step]
[step:Apply function extensionality to obtain uniqueness of the mediating map]
The previous step proves that for every $c:C$,
\begin{align*}
h(c)=\langle f,g\rangle(c).
\end{align*}
By the assumed function extensionality principle for functions from $C$ to $A\times B$, this pointwise equality induces
\begin{align*}
h=\langle f,g\rangle.
\end{align*}
Thus every function $h:C\to A\times B$ with projection composites $f$ and $g$ is equal to the constructed map $\langle f,g\rangle$. Hence $\langle f,g\rangle$ exists and is unique with the stated projection properties.
[/step]
