1.8 The type of booleans

The type of booleans 𝟐:𝒰 is intended to have exactly two elements 0𝟐,1𝟐:𝟐. It is clear that we could construct this type out of coproductMathworldPlanetmath 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 f:πŸβ†’C we need c0,c1:C and add the defining equations

f⁒(0𝟐) :≑c0,
f⁒(1𝟐) :≑c1.

The recursor corresponds to the if-then-else construct in functional programming:


with the defining equations

π—‹π–Ύπ–ΌπŸβ’(C,c0,c1,0𝟐) :≑c0,
π—‹π–Ύπ–ΌπŸβ’(C,c0,c1,1𝟐) :≑c1.

Given C:πŸβ†’π’°, to derive a dependent function f:∏(x:𝟐)C⁒(x) we need c0:C⁒(0𝟐) and c1:C⁒(1𝟐), in which case we can give the defining equations

f⁒(0𝟐) :≑c0,
f⁒(1𝟐) :≑c1.

We package this up into the inductionMathworldPlanetmath principle


with the defining equations

π—‚π—‡π–½πŸβ’(C,c0,c1,0𝟐) :≑c0,
π—‚π—‡π–½πŸβ’(C,c0,c1,1𝟐) :≑c1.

As an example, using the induction principle we can prove that, as we expect, every element of 𝟐 is either 1𝟐 or 0𝟐. 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 𝗋𝖾𝖿𝗅x:x=x.

Theorem 1.8.1.

We have


We use the induction principle with C(x):≑(x=0𝟐)+(x=1𝟐). The two inputs are 𝗂𝗇𝗅⁒(𝗋𝖾𝖿𝗅0𝟐):C⁒(0𝟐) and 𝗂𝗇𝗋⁒(𝗋𝖾𝖿𝗅1𝟐):C⁒(1𝟐). ∎

We have remarked that Ξ£-types can be regarded as analogous to indexed disjoint unionsMathworldPlanetmathPlanetmath, while coproducts are binary disjoint unions. It is natural to expect that a binary disjoint union A+B could be constructed as an indexed one over the two-element type 𝟐. For this we need a type family P:πŸβ†’π’° such that P⁒(0𝟐)≑A and P⁒(1𝟐)≑B. 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 universePlanetmathPlanetmath 𝒰 is itself a type, is a subtle and important aspect of type theoryPlanetmathPlanetmath.) Thus, we could have defined



𝗂𝗇𝗅⁒(a) :≑(0𝟐,a),
𝗂𝗇𝗋⁒(b) :≑(1𝟐,b).

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 productsPlanetmathPlanetmathPlanetmath and Ξ -types: we could have defined


Pairs could then be constructed using induction for 𝟐:


while the projections are straightforward applications

𝗉𝗋1⁒(p) :≑p(0𝟐),
𝗉𝗋2⁒(p) :≑p(1𝟐).

The derivationPlanetmathPlanetmath 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 0𝟐 and 1𝟐 of 𝟐 as β€œfalse” and β€œtrue” respectively. However, note that unlike in classical mathematics, we do not use elements of 𝟐 as truth values or as propositionsPlanetmathPlanetmath. (Instead we identify propositions with types; see Β§1.11 (http://planetmath.org/111propositionsastypes).) In particular, the type Aβ†’πŸ is not generally the power setMathworldPlanetmath of A; it represents only the β€œdecidable” subsets of A (see http://planetmath.org/node/87576Chapter 3).

Title 1.8 The type of booleans