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}$

• Disjunction $(-)\vee(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$

• Conjunction $(-)\wedge(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$

• Biconditional $(-)\iff(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$

• Conditional $(-)\implies(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$

Properties

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

It is also the homotopy pushout? $\mathbb{1} \sqcup_\emptyset \mathbb{1}$.

See also

• decidable setoid

• decidable universal quantifier

• decidable existential quantifier

• Sierpinski space

• decidable subtype?

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)