# 1.7 Coproduct types

There are two ways to construct elements of $A+B$, either as ${\mathsf{inl}}(a):A+B$ for $a:A$, or as ${\mathsf{inr}}(b):A+B$ for $b:B$. There are no ways to construct elements of the empty type.

To construct a non-dependent function $f:A+B\to C$, we need functions $g_{0}:A\to C$ and $g_{1}:B\to C$. Then $f$ is defined via the defining equations

 $\displaystyle f({\mathsf{inl}}(a))$ $\displaystyle:\!\!\equiv g_{0}(a),$ $\displaystyle f({\mathsf{inr}}(b))$ $\displaystyle:\!\!\equiv g_{1}(b).$

That is, the function $f$ is defined by case analysis. As before, we can derive the recursor:

 $\mathsf{rec}_{A+B}:\prod_{(C:\mathcal{U})}\,(A\to C)\to(B\to C)\to A+B\to C$

with the defining equations

 $\displaystyle\mathsf{rec}_{A+B}(C,g_{0},g_{1},{\mathsf{inl}}(a))$ $\displaystyle:\!\!\equiv g_{0}(a),$ $\displaystyle\mathsf{rec}_{A+B}(C,g_{0},g_{1},{\mathsf{inr}}(b))$ $\displaystyle:\!\!\equiv g_{1}(b).$

We can always construct a function $f:\mathbf{0}\to C$ without having to give any defining equations, because there are no elements of $\mathbf{0}$ on which to define $f$. Thus, the recursor for $\mathbf{0}$ is

 $\mathsf{rec}_{\mathbf{0}}:\mathchoice{{\textstyle\prod_{(C:\mathcal{U})}}}{% \prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}% \mathbf{0}\to C,$

which constructs the canonical function from the empty type to any other type. Logically, it corresponds to the principle ex falso quodlibet.

To construct a dependent function $f:\mathchoice{\prod_{x:A+B}\,}{\mathchoice{{\textstyle\prod_{(x:A+B)}}}{\prod_% {(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{\textstyle\prod_{(x% :A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}}{\mathchoice{{% \textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}% }C(x)$ out of a coproduct, we assume as given the family $C:(A+B)\to\mathcal{U}$, and require

 $\displaystyle g_{0}$ $\displaystyle:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{% (a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}C({\mathsf{inl}}(% a)),$ $\displaystyle g_{1}$ $\displaystyle:\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}% }{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{% (b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle% \prod_{(b:B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}C({\mathsf{inr}}(% b)).$

This yields $f$ with the defining equations:

 $\displaystyle f({\mathsf{inl}}(a))$ $\displaystyle:\!\!\equiv g_{0}(a),$ $\displaystyle f({\mathsf{inr}}(b))$ $\displaystyle:\!\!\equiv g_{1}(b).$

We package this scheme into the induction  principle for coproducts:

 $\mathsf{ind}_{A+B}:\prod_{(C:(A+B)\to\mathcal{U})}\,\Bigl{(}\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}C({% \mathsf{inl}}(a))\Bigr{)}\to\Bigl{(}\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}C({\mathsf{inr}}(b))\Bigr{)}\to% \mathchoice{{\textstyle\prod_{(x:A+B)}}}{\prod_{(x:A+B)}}{\prod_{(x:A+B)}}{% \prod_{(x:A+B)}}C(x).$

As before, the recursor arises in the case that the family $C$ is constant.

The induction principle for the empty type

 $\mathsf{ind}_{\mathbf{0}}:\mathchoice{\prod_{(C:\mathbf{0}\to\mathcal{U})}\,}{% \mathchoice{{\textstyle\prod_{(C:\mathbf{0}\to\mathcal{U})}}}{\prod_{(C:% \mathbf{0}\to\mathcal{U})}}{\prod_{(C:\mathbf{0}\to\mathcal{U})}}{\prod_{(C:% \mathbf{0}\to\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:\mathbf{0}\to% \mathcal{U})}}}{\prod_{(C:\mathbf{0}\to\mathcal{U})}}{\prod_{(C:\mathbf{0}\to% \mathcal{U})}}{\prod_{(C:\mathbf{0}\to\mathcal{U})}}}{\mathchoice{{\textstyle% \prod_{(C:\mathbf{0}\to\mathcal{U})}}}{\prod_{(C:\mathbf{0}\to\mathcal{U})}}{% \prod_{(C:\mathbf{0}\to\mathcal{U})}}{\prod_{(C:\mathbf{0}\to\mathcal{U})}}}% \mathchoice{\prod_{(z:\mathbf{0})}\,}{\mathchoice{{\textstyle\prod_{(z:\mathbf% {0})}}}{\prod_{(z:\mathbf{0})}}{\prod_{(z:\mathbf{0})}}{\prod_{(z:\mathbf{0})}% }}{\mathchoice{{\textstyle\prod_{(z:\mathbf{0})}}}{\prod_{(z:\mathbf{0})}}{% \prod_{(z:\mathbf{0})}}{\prod_{(z:\mathbf{0})}}}{\mathchoice{{\textstyle\prod_% {(z:\mathbf{0})}}}{\prod_{(z:\mathbf{0})}}{\prod_{(z:\mathbf{0})}}{\prod_{(z:% \mathbf{0})}}}C(z)$

gives us a way to define a trivial dependent function out of the empty type.

Title 1.7 Coproduct types
\metatable