Contents

Definition

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

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

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

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

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)