[[!redirects decidable subtype classifier]] [[!redirects decidable subset classifier]] #Contents# * table of contents {:toc} ## 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}$ $$\neg 0 \coloneqq 1$$ $$\neg 1 \coloneqq 0$$ * Disjunction $(-)\vee(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$ $$0 \vee 0 \coloneqq 0$$ $$0 \vee 1 \coloneqq 1$$ $$1 \vee 0 \coloneqq 1$$ $$1 \vee 1 \coloneqq 1$$ * Conjunction $(-)\wedge(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$ $$0 \wedge 0 \coloneqq 0$$ $$0 \wedge 1 \coloneqq 0$$ $$1 \wedge 0 \coloneqq 0$$ $$1 \wedge 1 \coloneqq 1$$ * Biconditional $(-)\iff(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$ $$0 \iff 0 \coloneqq 1$$ $$0 \iff 1 \coloneqq 0$$ $$1 \iff 0 \coloneqq 0$$ $$1 \iff 1 \coloneqq 1$$ * Conditional $(-)\implies(-):\mathbb{2} \times \mathbb{2} \to \mathbb{2}$ $$0 \implies 0 \coloneqq 1$$ $$0 \implies 1 \coloneqq 1$$ $$1 \implies 0 \coloneqq 0$$ $$1 \implies 1 \coloneqq 1$$ ## 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)$$ ## See also ## * [[decidable setoid]] * [[decidable universal quantifier]] * [[decidable existential quantifier]] ## References ## * Univalent Foundations Project, [[HoTT book|Homotopy Type Theory – Univalent Foundations of Mathematics]] (2013) category: not redirected to nlab yet