1.8 The type of booleans

The type of booleans $\mathbf{2}:\mathcal{U}$ is intended to have exactly two elements ${0_{\mathbf{2}}},{1_{\mathbf{2}}}:\mathbf{2}$ . It is clear that we could construct this type out of coproduct and unit types as $\mathbf{1}+\mathbf{1}$ . 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 $\Sigma$ -types and $\mathbf{2}$ .

To derive a function $f:\mathbf{2}\to C$ we need $c_{0},c_{1}:C$ and add the defining equations

	$\displaystyle f({0_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle f({1_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{1}.$

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

$\mathsf{rec}_{\mathbf{2}}:\mathchoice{\prod_{C:\mathcal{U}}\,}{\mathchoice{{% \textstyle\prod_{(C:\mathcal{U})}}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:% \mathcal{U})}}{\prod_{(C:\mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:% \mathcal{U})}}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:% \mathcal{U})}}}{\mathchoice{{\textstyle\prod_{(C:\mathcal{U})}}}{\prod_{(C:% \mathcal{U})}}{\prod_{(C:\mathcal{U})}}{\prod_{(C:\mathcal{U})}}}C\to C\to% \mathbf{2}\to C$

with the defining equations

	$\displaystyle\mathsf{rec}_{\mathbf{2}}(C,c_{0},c_{1},{0_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle\mathsf{rec}_{\mathbf{2}}(C,c_{0},c_{1},{1_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{1}.$

Given $C:\mathbf{2}\to\mathcal{U}$ , to derive a dependent function $f:\mathchoice{\prod_{x:\mathbf{2}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbf% {2})}}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}% }}{\mathchoice{{\textstyle\prod_{(x:\mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{% \prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}}{\mathchoice{{\textstyle\prod_% {(x:\mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:% \mathbf{2})}}}C(x)$ we need $c_{0}:C({0_{\mathbf{2}}})$ and $c_{1}:C({1_{\mathbf{2}}})$ , in which case we can give the defining equations

	$\displaystyle f({0_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle f({1_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{1}.$

We package this up into the induction principle

$\mathsf{ind}_{\mathbf{2}}:\prod_{(C:\mathbf{2}\to\mathcal{U})}\,C({0_{\mathbf{% 2}}})\to C({1_{\mathbf{2}}})\to\mathchoice{{\textstyle\prod_{(x:\mathbf{2})}}}% {\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}C(x)$

with the defining equations

	$\displaystyle\mathsf{ind}_{\mathbf{2}}(C,c_{0},c_{1},{0_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{0},$
	$\displaystyle\mathsf{ind}_{\mathbf{2}}(C,c_{0},c_{1},{1_{\mathbf{2}}})$	$\displaystyle:\!\!\equiv c_{1}.$

As an example, using the induction principle we can prove that, as we expect, every element of $\mathbf{2}$ is either ${1_{\mathbf{2}}}$ or ${0_{\mathbf{2}}}$ . 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 $\mathsf{refl}_{x}:x=x$ .

Theorem 1.8.1.

We have

$\mathchoice{\prod_{x:\mathbf{2}}\,}{\mathchoice{{\textstyle\prod_{(x:\mathbf{2% })}}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}}% {\mathchoice{{\textstyle\prod_{(x:\mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{\prod% _{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}}{\mathchoice{{\textstyle\prod_{(x:% \mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:% \mathbf{2})}}}(x={0_{\mathbf{2}}})+(x={1_{\mathbf{2}}}).$

Proof.

We use the induction principle with $C(x):\!\!\equiv(x={0_{\mathbf{2}}})+(x={1_{\mathbf{2}}})$ . The two inputs are ${\mathsf{inl}}(\mathsf{refl}_{{0_{\mathbf{2}}}}):C({0_{\mathbf{2}}})$ and ${\mathsf{inr}}(\mathsf{refl}_{{1_{\mathbf{2}}}}):C({1_{\mathbf{2}}})$ . ∎

We have remarked that $\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 $\mathbf{2}$ . For this we need a type family $P:\mathbf{2}\to\mathcal{U}$ such that $P({0_{\mathbf{2}}})\equiv A$ and $P({1_{\mathbf{2}}})\equiv B$ . Indeed, we can obtain such a family precisely by the recursion principle for $\mathbf{2}$ . (The ability to define type families by induction and recursion, using the fact that the universe $\mathcal{U}$ is itself a type, is a subtle and important aspect of type theory.) Thus, we could have defined

$A+B:\!\!\equiv\mathchoice{\sum_{x:\mathbf{2}}\,}{\mathchoice{{\textstyle\sum_{% (x:\mathbf{2})}}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:% \mathbf{2})}}}{\mathchoice{{\textstyle\sum_{(x:\mathbf{2})}}}{\sum_{(x:\mathbf% {2})}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:\mathbf{2})}}}{\mathchoice{{\textstyle% \sum_{(x:\mathbf{2})}}}{\sum_{(x:\mathbf{2})}}{\sum_{(x:\mathbf{2})}}{\sum_{(x% :\mathbf{2})}}}\mathsf{rec}_{\mathbf{2}}(\mathcal{U},A,B,x).$

with

	$\displaystyle{\mathsf{inl}}(a)$	$\displaystyle:\!\!\equiv({0_{\mathbf{2}}},a),$
	$\displaystyle{\mathsf{inr}}(b)$	$\displaystyle:\!\!\equiv({1_{\mathbf{2}}},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 $\Pi$ -types: we could have defined

$A\times B:\!\!\equiv\mathchoice{\prod_{x:\mathbf{2}}\,}{\mathchoice{{% \textstyle\prod_{(x:\mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2% })}}{\prod_{(x:\mathbf{2})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbf{2})}}}{% \prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}}{% \mathchoice{{\textstyle\prod_{(x:\mathbf{2})}}}{\prod_{(x:\mathbf{2})}}{\prod_% {(x:\mathbf{2})}}{\prod_{(x:\mathbf{2})}}}\mathsf{rec}_{\mathbf{2}}(\mathcal{U% },A,B,x)$

Pairs could then be constructed using induction for $\mathbf{2}$ :

$(a,b):\!\!\equiv\mathsf{ind}_{\mathbf{2}}(\mathsf{rec}_{\mathbf{2}}(\mathcal{U% },A,B),a,b)$

while the projections are straightforward applications

	$\displaystyle\mathsf{pr}_{1}(p)$	$\displaystyle:\!\!\equiv p({0_{\mathbf{2}}}),$
	$\displaystyle\mathsf{pr}_{2}(p)$	$\displaystyle:\!\!\equiv p({1_{\mathbf{2}}}).$

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

Title	1.8 The type of booleans
\metatable