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 |
---|---|
\metatable |