1.7 Coproduct types
Given , we introduce their coproduct type . 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 a nullary version: the empty type .
There are two ways to construct elements of , either as for , or as for . There are no ways to construct elements of the empty type.
To construct a non-dependent function , we need functions and . Then is defined via the defining equations
That is, the function is defined by case analysis. As before, we can derive the recursor:
with the defining equations
We can always construct a function without having to give any defining equations, because there are no elements of on which to define . Thus, the recursor for is
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 out of a coproduct, we assume as given the family , and require
This yields with the defining equations:
We package this scheme into the induction principle for coproducts:
As before, the recursor arises in the case that the family is constant.
The induction principle for the empty type
gives us a way to define a trivial dependent function out of the empty type.
|Title||1.7 Coproduct types|