Homotopy Type Theory booleans > history (Rev #4, changes)

Showing changes from revision #3 to #4: Added | Removed | Changed

Contents

Definition

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

  • a term 0:𝟚 \bot:\mathbb{2} 0:\mathbb{2}

  • a term 1:𝟚 \top:\mathbb{2} 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}
¬01\neg 0 \coloneqq 1
¬10\neg 1 \coloneqq 0
  • Disjunction ()():𝟚×𝟚𝟚(-)\vee(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}
0000 \vee 0 \coloneqq 0
0110 \vee 1 \coloneqq 1
1011 \vee 0 \coloneqq 1
1111 \vee 1 \coloneqq 1
  • Conjunction ()():𝟚×𝟚𝟚(-)\wedge(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}
0000 \wedge 0 \coloneqq 0
0100 \wedge 1 \coloneqq 0
1001 \wedge 0 \coloneqq 0
1111 \wedge 1 \coloneqq 1
  • Biconditional ()():𝟚×𝟚𝟚(-)\iff(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}
0010 \iff 0 \coloneqq 1
0100 \iff 1 \coloneqq 0
1001 \iff 0 \coloneqq 0
1111 \iff 1 \coloneqq 1
  • Conditional ()():𝟚×𝟚𝟚(-)\implies(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}
0010 \implies 0 \coloneqq 1
0110 \implies 1 \coloneqq 1
1001 \implies 0 \coloneqq 0
1111 \implies 1 \coloneqq 1

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 April 28, 2022 at 02:54:52 by Anonymous?. See the history of this page for a list of all contributions to it.