202503272203

Sum Types

Given types $A, B : U$ we introduce the type $A + B$ which is the disjoint union in set theory. This must be a fundamental construct because there is no notion of union of types in type theory. We also define a unit type for this operation that we will call $0 : U$ , the empty type.

There are 2 constructors of the type $A + B$ :

$inl : A \to A + B$
$inr : B \to A + B$ These are called “left injection” and “right injection”.

There are no ways to construct elements of the empty type.

Recursion Principle

To construct a non-dependent function $f : A + B \to C$ one needs 1 functions of type $g_{0} : A \to C$ and $g_{1} : B \to C$ respectively, now we can define $f$ as:
$f (inl (a)) f (inr (b)) :\equiv g_{0} (a) :\equiv g_{1} (b)$
That is, the function is defined by case-analysis and the recursor has the type:
$rec_{A + B} : C : U \prod (A \to C) \to (B \to C) \to A + B \to C$
with defining equation
$rec_{A + B} (C, g_{0}, g_{1}, inl (a)) :\equiv g_{0} (a) rec_{A + B} (C, g_{0}, g_{1}, inr (b)) :\equiv g_{1} (b)$
The recursor for $0$ will have the type:
$rec_{0} : C : U \prod 0 \to C$
This can be constructed without giving any definition as $0$ does not have any elements.

Induction Principle

To construct a dependent function out of a sum type, we assume we are given the family $C : A + B \to U$ , then we require 2 functions:

$g_{0} : \prod_{a : A} C (inl (a))$

$g_{1} : \prod_{b : B} C (inr (b))$ this gives the following definition for $f$ :

$f (inl (a)) :\equiv g_{0} (a) f (inr (b)) :\equiv g_{1} (b)$
Packaging the above construction into the induction operator we get
$ind_{A + B} : C : A + B \to U \prod (a : A \prod C (inl (a))) \to (b : B \prod C (inr (b))) \to x : A + B \prod C (x)$
And there is also an induction operator on the emtpy that has the type:
$ind_{0} : C : 0 \to U \prod z : 0 \prod C (z)$

References

Coproducts in Category Theory Dependent Pair Types

🏠 No Place Like ~

Explorer

Sum Types

References

Graph View

Table of Contents

Backlinks