1.8 The type of booleans
The type of booleans is intended to have exactly two elements . It is clear that we could construct this type out of coproduct and unit types as . However, since it is used frequently, we give the explicit rules here. Indeed, we are going to observe that we can also go the other way and derive binary coproducts from -types and .
To derive a function we need and add the defining equations
The recursor corresponds to the if-then-else construct in functional programming:
with the defining equations
Given , to derive a dependent function we need and , in which case we can give the defining equations
We package this up into the induction principle
with the defining equations
As an example, using the induction principle we can prove that, as we expect, every element of is either or . As before, we use the equality types which we have not yet introduced, but we need only the fact that everything is equal to itself by .
We use the induction principle with . The two inputs are and . ∎
We have remarked that -types can be regarded as analogous to indexed disjoint unions, while coproducts are binary disjoint unions. It is natural to expect that a binary disjoint union could be constructed as an indexed one over the two-element type . For this we need a type family such that and . Indeed, we can obtain such a family precisely by the recursion principle for . (The ability to define type families by induction and recursion, using the fact that the universe is itself a type, is a subtle and important aspect of type theory.) Thus, we could have defined
We leave it as an exercise to derive the induction principle of a coproduct type from this definition. (See also PMlinkexternalExercise 1.5http://planetmath.org/node/87558,§5.2 (http://planetmath.org/52uniquenessofinductivetypes).)
We can apply the same idea to products and -types: we could have defined
Pairs could then be constructed using induction for :
while the projections are straightforward applications
The derivation of the induction principle for binary products defined in this way is a bit more involved, and requires function extensionality, which we will introduce in §2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom). Moreover, we do not get the same judgmental equalities; see http://planetmath.org/node/87559Exercise 1.6. This is a recurrent issue when encoding one type as another; we will return to it in §5.5 (http://planetmath.org/55homotopyinductivetypes).
We may occasionally refer to the elements and of as “false” and “true” respectively. However, note that unlike in classical mathematics, we do not use elements of as truth values or as propositions. (Instead we identify propositions with types; see §1.11 (http://planetmath.org/111propositionsastypes).) In particular, the type is not generally the power set of ; it represents only the “decidable” subsets of (see http://planetmath.org/node/87576Chapter 3).
|Title||1.8 The type of booleans|