1.8 The type of booleans

The type of booleans $\mathrm{𝟐}:𝒰$ is intended to have exactly two elements$0_{\mathrm{𝟐}},1_{\mathrm{𝟐}}:\mathrm{𝟐}$. It is clear that we could construct thistype out of coproductand unit types as $\mathrm{𝟏}+\mathrm{𝟏}$. 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 wayand derive binary coproducts from $\mathrm{\Sigma }$-types and $\mathrm{𝟐}$.

To derive a function $f:\mathrm{𝟐}\to C$ we need $c_0,c_1:C$ andadd the defining equations

$f(0_{\mathrm{𝟐}})$$:\equiv c_0,$

$f(1_{\mathrm{𝟐}})$$:\equiv c_1.$

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

$${\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}:\prod _{C:𝒰}C\to C\to \mathrm{𝟐}\to C$$

with the defining equations

${\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(C,c_0,c_1,0_{\mathrm{𝟐}})$$:\equiv c_0,$

${\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(C,c_0,c_1,1_{\mathrm{𝟐}})$$:\equiv c_1.$

Given $C:\mathrm{𝟐}\to 𝒰$, to derive a dependent function$f:{\prod }_{(x:\mathrm{𝟐})}C(x)$ we need $c_0:C(0_{\mathrm{𝟐}})$ and $c_1:C(1_{\mathrm{𝟐}})$, in which case we can give the defining equations

$f(0_{\mathrm{𝟐}})$$:\equiv c_0,$

$f(1_{\mathrm{𝟐}})$$:\equiv c_1.$

We package this up into the induction principle

$${\mathrm{𝗂𝗇𝖽}}_{\mathrm{𝟐}}:\prod _{(C:\mathrm{𝟐}\to 𝒰)}C(0_{\mathrm{𝟐}})\to C(1_{\mathrm{𝟐}})\to {\prod }_{(x:\mathrm{𝟐})}C(x)$$

with the defining equations

${\mathrm{𝗂𝗇𝖽}}_{\mathrm{𝟐}}(C,c_0,c_1,0_{\mathrm{𝟐}})$$:\equiv c_0,$

${\mathrm{𝗂𝗇𝖽}}_{\mathrm{𝟐}}(C,c_0,c_1,1_{\mathrm{𝟐}})$$:\equiv c_1.$

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

Theorem 1.8.1.

We have

$$\prod _{x:\mathrm{𝟐}}(x=0_{\mathrm{𝟐}})+(x=1_{\mathrm{𝟐}}).$$

Proof.

We use the induction principle with $C(x):\equiv (x=0_{\mathrm{𝟐}})+(x=1_{\mathrm{𝟐}})$.The two inputs are $\mathrm{𝗂𝗇𝗅}({\mathrm{𝗋𝖾𝖿𝗅}}_{0_{\mathrm{𝟐}}}):C(0_{\mathrm{𝟐}})$ and $\mathrm{𝗂𝗇𝗋}({\mathrm{𝗋𝖾𝖿𝗅}}_{1_{\mathrm{𝟐}}}):C(1_{\mathrm{𝟐}})$.∎

We have remarked that $\mathrm{\Sigma }$-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 $A+B$ could be constructed as an indexed one over the two-element type $\mathrm{𝟐}$.For this we need a type family $P:\mathrm{𝟐}\to 𝒰$ such that $P(0_{\mathrm{𝟐}})\equiv A$ and $P(1_{\mathrm{𝟐}})\equiv B$.Indeed, we can obtain such a family precisely by the recursion principle for $\mathrm{𝟐}$.(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

$$A+B:\equiv \sum _{x:\mathrm{𝟐}}{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,A,B,x).$$

with

$\mathrm{𝗂𝗇𝗅}(a)$$:\equiv (0_{\mathrm{𝟐}},a),$

$\mathrm{𝗂𝗇𝗋}(b)$$:\equiv (1_{\mathrm{𝟐}},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 products and $\mathrm{\Pi }$-types: we could have defined

$$A\times B:\equiv \prod _{x:\mathrm{𝟐}}{\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,A,B,x)$$

Pairs could then be constructed using induction for $\mathrm{𝟐}$:

$$(a,b):\equiv {\mathrm{𝗂𝗇𝖽}}_{\mathrm{𝟐}}({\mathrm{𝗋𝖾𝖼}}_{\mathrm{𝟐}}(𝒰,A,B),a,b)$$

while the projections are straightforward applications

${\mathrm{𝗉𝗋}}_1(p)$$:\equiv p(0_{\mathrm{𝟐}}),$

${\mathrm{𝗉𝗋}}_2(p)$$:\equiv p(1_{\mathrm{𝟐}}).$

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 $0_{\mathrm{𝟐}}$ and $1_{\mathrm{𝟐}}$ of $\mathrm{𝟐}$ as “false” and “true” respectively.However, note that unlike in classical mathematics, we do not use elements of $\mathrm{𝟐}$ as truth valuesor as propositions.(Instead we identify propositions with types; see §1.11 (http://planetmath.org/111propositionsastypes).)In particular, the type $A\to \mathrm{𝟐}$ is not generally the power set of $A$; it represents only the “decidable” subsets of $A$ (see http://planetmath.org/node/87576Chapter 3).