1.7 Coproduct types

Given $A,B:\\mathcal{U}$ , we introduce their coproduct type $A+B:\\mathcal{U}$ .This corresponds to the disjoint union in set theory, and we may also use that name for it.In type theory, as was the case with functions and products, the coproduct must be a fundamental construction, since there is no previously given notion of “union of types”.We also introduce anullary version: the empty type $\\mathbf{0}:\\mathcal{U}$ .

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 needfunctions $g_{0}:A\\to C$ and $g_{1}:B\\to C$ . Then $f$ is definedvia 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$ withouthaving 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}$ , andrequire

	$\\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$ isconstant.

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 theempty type.