1.7 Coproduct types

Given A,B:𝒰, we introduce their coproductMathworldPlanetmath type A+B:𝒰. This corresponds to the disjoint unionMathworldPlanetmathPlanetmath in set theoryMathworldPlanetmath, and we may also use that name for it. In type theoryPlanetmathPlanetmath, as was the case with functions and productsPlanetmathPlanetmathPlanetmath, 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 𝟎:U.

There are two ways to construct elements of A+B, either as 𝗂𝗇𝗅⁒(a):A+B for a:A, or as 𝗂𝗇𝗋⁒(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→C, we need functions g0:A→C and g1:B→C. Then f is defined via the defining equations

f⁒(𝗂𝗇𝗅⁒(a)) :≑g0(a),
f⁒(𝗂𝗇𝗋⁒(b)) :≑g1(b).

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


with the defining equations

𝗋𝖾𝖼A+B⁒(C,g0,g1,𝗂𝗇𝗅⁒(a)) :≑g0(a),
𝗋𝖾𝖼A+B⁒(C,g0,g1,𝗂𝗇𝗋⁒(b)) :≑g1(b).

We can always construct a function f:πŸŽβ†’C without having to give any defining equations, because there are no elements of 𝟎 on which to define f. 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 f:∏(x:A+B)C⁒(x) out of a coproduct, we assume as given the family C:(A+B)→𝒰, and require

g0 :∏a:AC⁒(𝗂𝗇𝗅⁒(a)),
g1 :∏b:BC⁒(𝗂𝗇𝗋⁒(b)).

This yields f with the defining equations:

f⁒(𝗂𝗇𝗅⁒(a)) :≑g0(a),
f⁒(𝗂𝗇𝗋⁒(b)) :≑g1(b).

We package this scheme into the inductionMathworldPlanetmath principle for coproducts:


As before, the recursor arises in the case that the family C 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