booleans > history in Homotopy Type Theory

[[!redirects decidable subtype classifier]]

#Contents#
* table of contents
{:toc}

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

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

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

## See also ##

* [[Sierpinski space]]

* [[decidable subtype]]

## References ##

* Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013)