[proofplan]
We construct $[f,g]$ by the nondependent coproduct eliminator, using $f$ on the left summand and $g$ on the right summand. The coproduct beta laws immediately give the two required branch equations. For uniqueness, we compare any other function $h:A+B\to C$ satisfying the same branch equations with $[f,g]$ pointwise, using coproduct eta, and then apply function extensionality to upgrade pointwise equality to equality of functions.
[/proofplan]
[step:Construct the map from the coproduct eliminator]
Fix functions
\begin{align*}
f:A\to C
\end{align*}
and
\begin{align*}
g:B\to C.
\end{align*}
By the nondependent eliminator for the coproduct $A+B$, define the function
\begin{align*}
[f,g]:A+B\to C
\end{align*}
to be the map obtained by case analysis with left branch $f$ and right branch $g$. Thus, for an input $x:A+B$, the definition of $[f,g](x)$ is by cases on whether $x$ is introduced as $\iota_1(a)$ for some $a:A$ or as $\iota_2(b)$ for some $b:B$.
[guided]
We begin with the data that must determine a function out of a sum type. A function
\begin{align*}
f:A\to C
\end{align*}
specifies what should happen to inputs coming from the left summand, and a function
\begin{align*}
g:B\to C
\end{align*}
specifies what should happen to inputs coming from the right summand.
The nondependent eliminator for coproducts is precisely the rule that allows these two pieces of data to define a single function on $A+B$. Applying that eliminator to the codomain $C$, the left branch $f$, and the right branch $g$, we obtain a function
\begin{align*}
[f,g]:A+B\to C.
\end{align*}
This notation records the construction: $[f,g]$ is the map defined by case analysis, using $f$ after the left injection and using $g$ after the right injection.
[/guided]
[/step]
[step:Use the coproduct beta laws to prove the two branch equations]
Let $a:A$. Since $[f,g]$ was defined by the coproduct eliminator with left branch $f$, the left coproduct beta law gives
\begin{align*}
[f,g](\iota_1(a))=f(a).
\end{align*}
Let $b:B$. Since $[f,g]$ was defined by the coproduct eliminator with right branch $g$, the right coproduct beta law gives
\begin{align*}
[f,g](\iota_2(b))=g(b).
\end{align*}
Thus $[f,g]$ satisfies the required two computation equations.
[/step]
[step:Compare any other compatible map pointwise by coproduct eta]
Let
\begin{align*}
h:A+B\to C
\end{align*}
be a function satisfying the same branch equations, meaning that for every $a:A$ and every $b:B$ there are equalities
\begin{align*}
h(\iota_1(a))=f(a)
\end{align*}
and
\begin{align*}
h(\iota_2(b))=g(b).
\end{align*}
We prove that $h(x)=[f,g](x)$ for every $x:A+B$.
We use the coproduct eta principle in its pointwise comparison form for the two functions $h,[f,g]:A+B\to C$. It suffices to verify equality after precomposition with each coproduct injection. In the left branch, let $a:A$. Then
\begin{align*}
h(\iota_1(a))=f(a)
\end{align*}
by the assumed left branch equation for $h$, while
\begin{align*}
[f,g](\iota_1(a))=f(a)
\end{align*}
by the left beta law for $[f,g]$. Hence $h(\iota_1(a))=[f,g](\iota_1(a))$.
In the right branch, let $b:B$. Then
\begin{align*}
h(\iota_2(b))=g(b)
\end{align*}
by the assumed right branch equation for $h$, while
\begin{align*}
[f,g](\iota_2(b))=g(b)
\end{align*}
by the right beta law for $[f,g]$. Hence $h(\iota_2(b))=[f,g](\iota_2(b))$.
Therefore, by coproduct eta, there is a pointwise equality
\begin{align*}
\prod_{x:A+B} h(x)=[f,g](x).
\end{align*}
[guided]
Now suppose another function
\begin{align*}
h:A+B\to C
\end{align*}
has the same behaviour on both summands. This means that for every $a:A$ and every $b:B$ we are given equalities
\begin{align*}
h(\iota_1(a))=f(a)
\end{align*}
and
\begin{align*}
h(\iota_2(b))=g(b).
\end{align*}
To show that $h$ is the same function as $[f,g]$, the first task is to show that they agree at every input $x:A+B$.
The coproduct eta principle being used here is the pointwise comparison form: to prove that two functions $u,v:A+B\to C$ agree at every input, it is enough to prove $u(\iota_1(a))=v(\iota_1(a))$ for every $a:A$ and $u(\iota_2(b))=v(\iota_2(b))$ for every $b:B$. We apply this principle to the functions $u:=h$ and $v:=[f,g]$.
For the left branch, let $a:A$. The hypothesis on $h$ gives
\begin{align*}
h(\iota_1(a))=f(a).
\end{align*}
The construction of $[f,g]$ and the left coproduct beta law give
\begin{align*}
[f,g](\iota_1(a))=f(a).
\end{align*}
Composing the path $h(\iota_1(a))=f(a)$ with the inverse of the path $[f,g](\iota_1(a))=f(a)$ gives
\begin{align*}
h(\iota_1(a))=[f,g](\iota_1(a)).
\end{align*}
For the right branch, let $b:B$. The hypothesis on $h$ gives
\begin{align*}
h(\iota_2(b))=g(b).
\end{align*}
The construction of $[f,g]$ and the right coproduct beta law give
\begin{align*}
[f,g](\iota_2(b))=g(b).
\end{align*}
Composing the path $h(\iota_2(b))=g(b)$ with the inverse of the path $[f,g](\iota_2(b))=g(b)$ gives
\begin{align*}
h(\iota_2(b))=[f,g](\iota_2(b)).
\end{align*}
The eta principle combines these two casewise equalities into the pointwise statement
\begin{align*}
\prod_{x:A+B} h(x)=[f,g](x).
\end{align*}
This is exactly the information needed before invoking function extensionality: we have not merely compared the two functions on the generators informally, but have produced equality at every input of their common domain.
[/guided]
[/step]
[step:Apply function extensionality to obtain uniqueness of the function]
The functions $h$ and $[f,g]$ have the same domain $A+B$ and codomain $C$. From the previous step we have a pointwise equality
\begin{align*}
\prod_{x:A+B} h(x)=[f,g](x).
\end{align*}
By the [function extensionality principle](/theorems/9638) assumed in the theorem statement, this pointwise equality induces an equality of functions
\begin{align*}
h=[f,g].
\end{align*}
Hence every function $h:A+B\to C$ satisfying the two branch equations is equal to $[f,g]$. Since $[f,g]$ exists and satisfies those equations, it is the unique such function.
[guided]
At this point we know more than agreement on the two constructors: the previous step produced a pointwise equality
\begin{align*}
\prod_{x:A+B} h(x)=[f,g](x).
\end{align*}
The remaining gap is that uniqueness in the theorem is uniqueness as a function, not merely a family of pointwise equalities. Function extensionality, in the form assumed in the theorem statement, applies to the common domain $A+B$, the codomain $C$, and the two functions $h,[f,g]:A+B\to C$. Its hypothesis is precisely the displayed pointwise equality, so it yields an equality in the function type:
\begin{align*}
h=[f,g].
\end{align*}
Therefore any function $h:A+B\to C$ satisfying the same left and right branch equations is propositionally equal to the constructed function $[f,g]$. Since the earlier steps constructed $[f,g]$ and proved that it satisfies those two branch equations, this proves existence and propositional uniqueness of the required function.
[/guided]
[/step]
