Homotopy Type Theory booleans > history (Rev #1)

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

𝟚 P:𝒰isProp(P)×isDecidable(P)\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

References

Revision on March 12, 2022 at 17:52:58 by Anonymous?. See the history of this page for a list of all contributions to it.