Contents

Definition

The booleans $\mathbb{2}$ are inductively generated by

• a term $0:\mathbb{2}$

• a term $1:\mathbb{2}$

$\mathbb{2}$ is also called the decidable subtype classifier.

Boolean functions

The following functions could be inductively defined on the booleans:

• Negation $\neg:\mathbb{2} \to \mathbb{2}$
$\neg 0 \coloneqq 1$
$\neg 1 \coloneqq 0$
• Disjunction $(-)\vee(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$
$0 \vee 0 \coloneqq 0$
$0 \vee 1 \coloneqq 1$
$1 \vee 0 \coloneqq 1$
$1 \vee 1 \coloneqq 1$
• Conjunction $(-)\wedge(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$
$0 \wedge 0 \coloneqq 0$
$0 \wedge 1 \coloneqq 0$
$1 \wedge 0 \coloneqq 0$
$1 \wedge 1 \coloneqq 1$
• Biconditional $(-)\iff(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$
$0 \iff 0 \coloneqq 1$
$0 \iff 1 \coloneqq 0$
$1 \iff 0 \coloneqq 0$
$1 \iff 1 \coloneqq 1$
• Conditional $(-)\implies(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$
$0 \implies 0 \coloneqq 1$
$0 \implies 1 \coloneqq 1$
$1 \implies 0 \coloneqq 0$
$1 \implies 1 \coloneqq 1$

Properties

The booleans are homotopy-equivalent to the type of decidable propositions in a universe $\mathcal{U}$.

$\mathbb{2} \cong \sum_{P:\mathcal{U}} isProp(P) \times isDecidable(P)$

References

Revision on June 15, 2022 at 22:29:31 by Anonymous?. See the history of this page for a list of all contributions to it.