nLab boolean domain

Redirected from "type of booleans".
Contents

Context

Universes

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

The boolean domain or boolean field (often just: BoolBool) is a 22-element set, say 𝔹={0,1}\mathbb{B} = \{ 0, 1 \} (β€œbits”) or 𝔹={βŠ₯,⊀}\mathbb{B} = \{ \bot, \top \} (β€œbottom”, β€œtop”), whose elements may be interpreted as truth values.

Note that 𝔹\mathbb{B} is the set of all truth values in classical logic, but this cannot be assumed in non-classical logic such as intuitionistic logic.

The Boolean domain plays the role of the subobject classifier in the Boolean topos of Sets.

If we think of the classical 𝔹\mathbb{B} as a pointed set equipped with the true element, then there is an effectively unique boolean domain.

A boolean variable xx is a variable that takes its value in a boolean domain, as xβˆˆπ”Ήx \in \mathbb{B}. If this variable depends on parameters, then it is (or defines) a Boolean-valued function, that is a function whose target is 𝔹\mathbb{B}.

An element of 𝔹\mathbb{B} is a binary digit, or bit.

The boolean domain is the initial set with two elements. It is also the initial set with an element and an involution. It is also the tensor unit for the smash product in the monoidal category of pointed sets.

Remark

(relation to boolean algebra)
The term β€˜boolean field’ (or just β€˜field’, depending on the context) is sometimes used more generally for any boolean algebra. In fact, the boolean domain is the initial boolean algebra. If we interpret a boolean algebra as a boolean ring, then the boolean domain is the finite field with 22 elements.

Definition

In type theory

As an inductive type, the boolean domain is given by

Inductive Bool : Type
  | zero : Bool
  | one : Bool

This says that the type is inductively constructed from two terms in the type Bool, whose interpretation is as the two points of the type.

As a positive type

Assuming that identification types and dependent product types exist in the type theory, the boolean domain is the inductive type generated by two elements, and is defined by the following inference rules:

type formation rules for the boolean domain

Ξ“ctxΞ“βŠ’Booltype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Bool} \; \mathrm{type}}


term introduction rules for the boolean domain:

Ξ“ctx⊒0:BoolΞ“ctxΞ“βŠ’1:Bool\frac{\Gamma \; \mathrm{ctx}}{\vdash 0:\mathrm{Bool}} \qquad \frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash 1:\mathrm{Bool}}


term elimination rules for the boolean domain:

Ξ“,x:Bool⊒C(x)typeΞ“,c 0:C(0),c 1:C(1),p:Bool⊒ind Bool C(c 0,c 1,p):C(p)\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1), p:\mathrm{Bool} \vdash \mathrm{ind}_\mathrm{Bool}^C(c_0, c_1, p):C(p)}


computation rules for the boolean domain:

  • judgmental computation rules

    Ξ“,x:Bool⊒C(x)typeΞ“,c 0:C(0),c 1:C(1)⊒ind Bool C(c 0,c 1,0)≑c 0:C(0)\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \mathrm{ind}_\mathrm{Bool}^C(c_0, c_1, 0) \equiv c_0:C(0)}
    Ξ“,x:Bool⊒C(x)typeΞ“,c 0:C(0),c 1:C(1)⊒ind Bool C(c 0,c 1,1)≑c 1:C(1)\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \mathrm{ind}_\mathrm{Bool}^C(c_0, c_1, 1) \equiv c_1:C(1)}
  • typal computation rules

    Ξ“,x:Bool⊒C(x)typeΞ“,c 0:C(0),c 1:C(1)⊒β Bool 0(c 0,c 1):Id C(0)(ind Bool C(c 0,c 1,0),c 0)\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \beta_\mathrm{Bool}^0(c_0, c_1):\mathrm{Id}_{C(0)}(\mathrm{ind}_\mathrm{Bool}^C(c_0, c_1, 0), c_0)}
    Ξ“,x:Bool⊒C(x)typeΞ“,c 0:C(0),c 1:C(1)⊒β Bool 1(c 0,c 1,1):Id C(1)(ind Bool C(c 0,c 1,1),c 1)\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1) \vdash \beta_\mathrm{Bool}^1(c_0, c_1, 1):\mathrm{Id}_{C(1)}(\mathrm{ind}_\mathrm{Bool}^C(c_0, c_1, 1), c_1)}


uniqueness rules for the boolean domain:

  • judgmental uniqueness rules
    Ξ“,x:Bool⊒C(x)typeΞ“,c:∏ x:BoolC(x),p:Bool⊒ind Bool C(c(0),c(1),p)≑c(p):C(p)\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c:\prod_{x:\mathrm{Bool}} C(x), p:\mathrm{Bool} \vdash \mathrm{ind}_\mathrm{Bool}^C(c(0), c(1), p) \equiv c(p):C(p)}
  • typal uniqueness rules
    Ξ“,x:Bool⊒C(x)typeΞ“,c:∏ x:BoolC(x),p:Bool⊒η Bool(c,p):Id C(p)(ind Bool C(c(0),c(1),p),c(p))\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c:\prod_{x:\mathrm{Bool}} C(x), p:\mathrm{Bool} \vdash \eta_\mathrm{Bool}(c, p):\mathrm{Id}_{C(p)}(\mathrm{ind}_\mathrm{Bool}^C(c(0), c(1), p), c(p))}


The elimination, typal computation, and typal uniqueness rules for the boolean domain state that the boolean domain satisfies the dependent universal property of the boolean domain. If the dependent type theory also has dependent sum types and product types, allowing one to define the uniqueness quantifier, the dependent universal property of the boolean domain can be simplified to the following rule:

Ξ“,x:Bool⊒C(x)typeΞ“,c 0:C(0),c 1:C(1)⊒up Bool C(c 0,c 1):βˆƒ!c:∏ x:BoolC(x).Id C(0)(c(0),c 0)Γ—Id C(1)(c(1),c 1)\frac{\Gamma, x:\mathrm{Bool} \vdash C(x) \; \mathrm{type}}{\Gamma, c_0:C(0), c_1:C(1)\vdash \mathrm{up}_\mathrm{Bool}^C(c_0, c_1):\exists!c:\prod_{x:\mathrm{Bool}} C(x).\mathrm{Id}_{C(0)}(c(0), c_0) \times \mathrm{Id}_{C(1)}(c(1), c_1)}

The judgmental computation and uniqueness rules imply the typal computation and uniqueness rules and thus imply the dependent universal property of the boolean domain.

In type theories with a separate type judgment where not all types are elements of universes, one has to additionally add the following elimination and computation rules:

Elimination rules:

Ξ“βŠ’AtypeΞ“βŠ’BtypeΞ“,x:Bool⊒typerec Bool A,B(x)type\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma, x:\mathrm{Bool} \vdash \mathrm{typerec}_{\mathrm{Bool}}^{A, B}(x) \; \mathrm{type}}

Computation rules:

  • judgmental computation rules
Ξ“βŠ’AtypeΞ“βŠ’BtypeΞ“βŠ’typerec Bool A,B(0)≑Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{typerec}_{\mathrm{Bool}}^{A, B}(0) \equiv A \; \mathrm{type}}
Ξ“βŠ’AtypeΞ“βŠ’BtypeΞ“βŠ’typerec Bool A,B(1)≑Btype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \mathrm{typerec}_{\mathrm{Bool}}^{A, B}(1) \equiv B \; \mathrm{type}}
  • typal computation rules
Ξ“βŠ’AtypeΞ“βŠ’BtypeΞ“βŠ’Ξ² Bool 0,A,B:typerec Bool A,B(0)≃A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \beta_{\mathrm{Bool}}^{0, A, B}:\mathrm{typerec}_{\mathrm{Bool}}^{A, B}(0) \simeq A}
Ξ“βŠ’AtypeΞ“βŠ’BtypeΞ“βŠ’Ξ² Bool 1,A,B:typerec Bool A,B(1)≃B\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash B \; \mathrm{type}}{\Gamma \vdash \beta_{\mathrm{Bool}}^{1, A, B}:\mathrm{typerec}_{\mathrm{Bool}}^{A, B}(1) \simeq B}

As the type of decidable propositions

The boolean domain can also be defined as the type of decidable propositions. Suppose that we have a type of propositions Prop\mathrm{Prop}. Then, the type of booleans is defined as

Boolβ‰‘βˆ‘ P:PropP∨¬P\mathrm{Bool} \equiv \sum_{P:\mathrm{Prop}} P \vee \neg P

where A∨BA \vee B is the disjunction of two types AA and BB and Β¬A≑Aβ†’βˆ…\neg A \equiv A \to \emptyset is the negation of the type AA. Both disjunctions and the empty set can be directly defined from Prop\mathrm{Prop}, dependent function types, and product types.

One can also define directly the boolean domain as the type of all decidable propositions, provided one already has disjunctions defined in the type theory. Similarly to the type of all propositions, the boolean domain can be presented either as a Russell universe or a Tarski universe. The difference between the two is that in the former, every decidable proposition in the type theory is literally an element of the boolean domain, while in the latter, elements of Bool\mathrm{Bool} are only indices of a (-1)-truncated type family El\mathrm{El}; every decidable proposition in the type theory is only essentially Bool \mathrm{Bool} -small for weak Tarski universes or judgmentally equal to an El(P)\mathrm{El}(P) for P:BoolP:\mathrm{Bool} for strict Tarski universes.

As a strict Tarski universe

As a strict Tarski universe, the boolean domain is given by the following natural deduction inference rules:

Formation rules for the boolean domain:

Ξ“ctxΞ“βŠ’Booltype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Bool} \; \mathrm{type}}

Introduction rules for the boolean domain:

Ξ“βŠ’AtypeΞ“βŠ’toBool A:isProp(A)β†’(A∨¬A)β†’Bool\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toBool}_A:\mathrm{isProp}(A) \to (A \vee \neg A) \to \mathrm{Bool}}

Elimination rules for the boolean domain:

Ξ“βŠ’A:BoolΞ“βŠ’El(A)typeΞ“βŠ’A:BoolΞ“βŠ’proptrunc(A):isProp(El(A))Ξ“βŠ’A:BoolΞ“βŠ’lem(A):El(A)∨¬El(A)\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{proptrunc}(A):\mathrm{isProp}(\mathrm{El}(A))} \qquad \frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{lem}(A):\mathrm{El}(A) \vee \neg \mathrm{El}(A)}

Computation rules for the boolean domain:

Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’El(toBool A(p)(q))≑Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{El}(\mathrm{toBool}_A(p)(q)) \equiv A \; \mathrm{type}}
  • Judgmental computation rules:
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’proptrunc(toBool A(p)(q))≑p:isProp(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{proptrunc}(\mathrm{toBool}_A(p)(q)) \equiv p:\mathrm{isProp}(A)}
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’lem(toBool A(p)(q))≑q:A∨¬A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{lem}(\mathrm{toBool}_A(p)(q)) \equiv q:A \vee \neg A}
  • Typal computation rules:
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’Ξ² Bool proptrunc,A(p,q):Id isProp(A)(proptrunc(toBool A(p)(q)),p)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \beta_{\mathrm{Bool}}^{\mathrm{proptrunc}, A}(p, q):\mathrm{Id}_{\mathrm{isProp}(A)}(\mathrm{proptrunc}(\mathrm{toBool}_A(p)(q)), p)}
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’Ξ² Bool lem,A(p,q):Id A∨¬A(lem(toBool A(p)(q)),q)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \beta_{\mathrm{Bool}}^{\mathrm{lem}, A}(p, q):\mathrm{Id}_{A \vee \neg A}(\mathrm{lem}(\mathrm{toBool}_A(p)(q)), q)}

Uniqueness rules for the boolean domain:

  • Judgmental computation rules:

    Ξ“βŠ’A:BoolΞ“βŠ’toBool El(A)(proptrunc(A))(lem(A))≑A:Bool\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{toBool}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A))(\mathrm{lem}(A)) \equiv A:\mathrm{Bool}}
  • Typal computation rules:

    Ξ“βŠ’A:BoolΞ“βŠ’Ξ· Bool(A):Id Bool(toProp El(A)(proptrunc(A))(lem(A)),A)\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \eta_{\mathrm{Bool}}(A):\mathrm{Id}_{\mathrm{Bool}}(\mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A))(\mathrm{lem}(A)), A)}

Extensionality principle for the boolean domain:

Ξ“βŠ’A:BoolΞ“βŠ’B:BoolΞ“βŠ’ext Bool(A,B):isEquiv(transport El(A,B))\frac{\Gamma \vdash A:\mathrm{Bool} \quad \Gamma \vdash B:\mathrm{Bool}} {\Gamma \vdash \mathrm{ext}_\mathrm{Bool}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}
As a weak Tarski universe

As a weak Tarski universe, the boolean domain is given by the following natural deduction inference rules:

Formation rules for the boolean domain:

Ξ“ctxΞ“βŠ’Booltype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Bool} \; \mathrm{type}}

Introduction rules for the boolean domain:

Ξ“βŠ’AtypeΞ“βŠ’toBool A:isProp(A)β†’(A∨¬A)β†’Bool\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toBool}_A:\mathrm{isProp}(A) \to (A \vee \neg A) \to \mathrm{Bool}}

Elimination rules for the boolean domain:

Ξ“βŠ’A:BoolΞ“βŠ’El(A)typeΞ“βŠ’A:BoolΞ“βŠ’proptrunc(A):isProp(El(A))Ξ“βŠ’A:BoolΞ“βŠ’lem(A):El(A)∨¬El(A)\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{El}(A) \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{proptrunc}(A):\mathrm{isProp}(\mathrm{El}(A))} \qquad \frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{lem}(A):\mathrm{El}(A) \vee \neg \mathrm{El}(A)}

Computation rules for the boolean domain:

Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’Ξ² Bool El,A(p,q):El(toBool A(p)(q))≃A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \beta_\mathrm{Bool}^{\mathrm{El}, A}(p, q):\mathrm{El}(\mathrm{toBool}_A(p)(q)) \simeq A}
  • Judgmental computation rules:
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’congform isProp(Ξ² Bool El,A(p,q))(proptrunc(toBool A(p)(q)))≑p:isProp(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Bool}^{\mathrm{El}, A}(p, q))(\mathrm{proptrunc}(\mathrm{toBool}_A(p)(q))) \equiv p:\mathrm{isProp}(A)}
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’congform (βˆ’)∨¬(βˆ’)(Ξ² Bool El,A(p,q))(lem(toBool A(p)(q)))≑q:A∨¬A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{congform}_{(-) \vee \neg (-)}(\beta_\mathrm{Bool}^{\mathrm{El}, A}(p, q))(\mathrm{lem}(\mathrm{toBool}_A(p)(q))) \equiv q:A \vee \neg A}
  • Typal computation rules:
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’Ξ² Bool proptrunc,A(p,q):Id isProp(A)(congform isProp(Ξ² Bool El,A(p,q))(proptrunc(toBool A(p)(q))),p)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \beta_{\mathrm{Bool}}^{\mathrm{proptrunc}, A}(p, q):\mathrm{Id}_{\mathrm{isProp}(A)}(\mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Bool}^{\mathrm{El}, A}(p, q))(\mathrm{proptrunc}(\mathrm{toBool}_A(p)(q))), p)}
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’Ξ² Bool proptrunc,A(p,q):Id A∨¬A(congform (βˆ’)∨¬(βˆ’)(Ξ² Bool El,A(p,q))(lem(toBool A(p)(q))),q)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \beta_{\mathrm{Bool}}^{\mathrm{proptrunc}, A}(p, q):\mathrm{Id}_{A \vee \neg A}(\mathrm{congform}_{(-) \vee \neg (-)}(\beta_\mathrm{Bool}^{\mathrm{El}, A}(p, q))(\mathrm{lem}(\mathrm{toBool}_A(p)(q))), q)}

where the equivalences

congform isProp(Ξ² Bool El,A(p,q)):isProp(El(toProp A(p)(q)))≃isProp(A)\mathrm{congform}_\mathrm{isProp}(\beta_\mathrm{Bool}^{\mathrm{El}, A}(p, q)):\mathrm{isProp}(\mathrm{El}(\mathrm{toProp}_A(p)(q))) \simeq \mathrm{isProp}(A)
congform (βˆ’)∨¬(βˆ’)(Ξ² Bool El,A(p,q)):(El(toProp A(p)(q))∨¬El(toProp A(p)(q)))≃(A∨¬A)\mathrm{congform}_{(-) \vee \neg (-)}(\beta_\mathrm{Bool}^{\mathrm{El}, A}(p, q)):(\mathrm{El}(\mathrm{toProp}_A(p)(q)) \vee \neg \mathrm{El}(\mathrm{toProp}_A(p)(q))) \simeq (A \vee \neg A)

can always be constructed in a type theory with dependent product types, dependent sum types, identity types, disjunctions, and negations, as given types AA and BB and an equivalence e:A≃Be:A \simeq B, it is possible to form the equivalences

congform isProp(e):isProp(A)≃isProp(B)\mathrm{congform}_\mathrm{isProp}(e):\mathrm{isProp}(A) \simeq \mathrm{isProp}(B)
congform (βˆ’)∨¬(βˆ’)(e):(A∨¬A)≃(B∨¬B)\mathrm{congform}_{(-) \vee \neg (-)}(e):(A \vee \neg A) \simeq (B \vee \neg B)

through application of equivalences to identifications and the typal congruence rules of function types, dependent product types, product types, dependent sum types, disjunctions, and negations.

Uniqueness rules for the boolean domain:

  • Judgmental computation rules:

    Ξ“βŠ’A:BoolΞ“βŠ’toBool El(A)(proptrunc(A))(lem(A))≑A:Bool\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash\mathrm{toBool}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A))(\mathrm{lem}(A)) \equiv A:\mathrm{Bool}}
  • Typal computation rules:

    Ξ“βŠ’A:BoolΞ“βŠ’Ξ· Bool(A):Id Bool(toProp El(A)(proptrunc(A))(lem(A)),A)\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \eta_{\mathrm{Bool}}(A):\mathrm{Id}_{\mathrm{Bool}}(\mathrm{toProp}_{\mathrm{El}(A)}(\mathrm{proptrunc}(A))(\mathrm{lem}(A)), A)}

Extensionality principle for the boolean domain:

Ξ“βŠ’A:BoolΞ“βŠ’B:BoolΞ“βŠ’ext Bool(A,B):isEquiv(transport El(A,B))\frac{\Gamma \vdash A:\mathrm{Bool} \quad \Gamma \vdash B:\mathrm{Bool}} {\Gamma \vdash \mathrm{ext}_\mathrm{Bool}(A, B):\mathrm{isEquiv}(\mathrm{transport}^\mathrm{El}(A, B))}
As a Russell universe

As a Russell universe, the boolean domain is given by the following natural deduction inference rules:

Formation rules for the boolean domain:

Ξ“ctxΞ“βŠ’Booltype\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{Bool} \; \mathrm{type}}

Introduction rules for the boolean domain:

Ξ“βŠ’AtypeΞ“βŠ’toBool A:isProp(A)β†’(A∨¬A)β†’Bool\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash \mathrm{toBool}_A:\mathrm{isProp}(A) \to (A \vee \neg A) \to \mathrm{Bool}}

Elimination rules for the boolean domain:

Ξ“βŠ’A:BoolΞ“βŠ’AtypeΞ“βŠ’A:BoolΞ“βŠ’proptrunc(A):isProp(A)Ξ“βŠ’A:BoolΞ“βŠ’lem(A):A∨¬A\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash A \; \mathrm{type}} \qquad \frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{proptrunc}(A):\mathrm{isProp}(A)} \qquad \frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{lem}(A):A \vee \neg A}

Computation rules for the boolean domain:

Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’toBool A(p)(q)≑Atype\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{toBool}_A(p)(q) \equiv A \; \mathrm{type}}
  • Judgmental computation rules:
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’proptrunc(toBool A(p)(q))≑p:isProp(A)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{proptrunc}(\mathrm{toBool}_A(p)(q)) \equiv p:\mathrm{isProp}(A)}
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’lem(toBool A(p)(q))≑q:A∨¬A\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \mathrm{lem}(\mathrm{toBool}_A(p)(q)) \equiv q:A \vee \neg A}
  • Typal computation rules:
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’Ξ² Bool proptrunc,A:Id isProp(A)(proptrunc(toBool A(p)(q)),p)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \beta_{\mathrm{Bool}}^{\mathrm{proptrunc}, A}:\mathrm{Id}_{\mathrm{isProp}(A)}(\mathrm{proptrunc}(\mathrm{toBool}_A(p)(q)), p)}
Ξ“βŠ’AtypeΞ“βŠ’p:isProp(A)Ξ“βŠ’q:A∨¬AΞ“βŠ’Ξ² Bool lem,A:Id A∨¬A(lem(toBool A(p)(q)),q)\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash p:\mathrm{isProp}(A) \quad \Gamma \vdash q:A \vee \neg A}{\Gamma \vdash \beta_{\mathrm{Bool}}^{\mathrm{lem}, A}:\mathrm{Id}_{A \vee \neg A}(\mathrm{lem}(\mathrm{toBool}_A(p)(q)), q)}

Uniqueness rules for the boolean domain:

  • Judgmental computation rules:

    Ξ“βŠ’A:BoolΞ“βŠ’toBool A(proptrunc(A))(lem(A))≑A:Bool\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \mathrm{toBool}_{A}(\mathrm{proptrunc}(A))(\mathrm{lem}(A)) \equiv A:\mathrm{Bool}}
  • Typal computation rules:

    Ξ“βŠ’A:BoolΞ“βŠ’Ξ· Bool(A):Id Bool(toBool A(proptrunc(A))(lem(A)),A)\frac{\Gamma \vdash A:\mathrm{Bool}}{\Gamma \vdash \eta_{\mathrm{Bool}}(A):\mathrm{Id}_{\mathrm{Bool}}(\mathrm{toBool}_{A}(\mathrm{proptrunc}(A))(\mathrm{lem}(A)), A)}

Extensionality principle for the boolean domain:

Ξ“βŠ’A:BoolΞ“βŠ’B:BoolΞ“βŠ’ext Bool(A,B):isEquiv(idToEquiv(A,B))\frac{\Gamma \vdash A:\mathrm{Bool} \quad \Gamma \vdash B:\mathrm{Bool}} {\Gamma \vdash \mathrm{ext}_\mathrm{Bool}(A, B):\mathrm{isEquiv}(\mathrm{idToEquiv}(A, B))}

In homotopy type theory

In homotopy type theory the type of booleans / bits looks as above (using judgemental equality, propositional equality, or typal equality for the computation rule and uniqueness rule) but now it may equivalently be thought of as the sphere type of the 0-sphere and as such as the beginning of the suspension type-tower of types of β€œhigher homotopy bits” β€” the n n -sphere types:


Properties

Descent and large elimination

The descent for the boolean domain states that given any types AA and BB one can construct a type family x:𝟚⊒descFam 𝟚 A,B(x)x:\mathbb{2} \vdash \mathrm{descFam}_\mathbb{2}^{A, B}(x) with equivalences of types

descEquiv A:descFam 𝟚 A,B(0)≃AanddescEquiv B:descFam 𝟚 A,B(1)≃B\mathrm{descEquiv}_A:\mathrm{descFam}_\mathbb{2}^{A, B}(0) \simeq A \quad \mathrm{and} \quad \mathrm{descEquiv}_B:\mathrm{descFam}_\mathbb{2}^{A, B}(1) \simeq B

Large elimination for the boolean domain strengthens the equivalences of types in descent to judgmental equality of types

descFam 𝟚 A,B(0)≑AanddescFam 𝟚 A,B(1)≑B\mathrm{descFam}_\mathbb{2}^{A, B}(0) \equiv A \quad \mathrm{and} \quad \mathrm{descFam}_\mathbb{2}^{A, B}(1) \equiv B

Extensionality principle of the boolean domain

The elements of the boolean domain represent certain truth values or propositions, namely, true and false. By the principle of propositions as some types, truth values or propositions are represented as certain types: specifically, true or 11 is represented by the unit type πŸ™\mathbb{1}, and false or 00 is represented by the empty type 𝟘\mathbb{0}. The boolean domain is a Tarski universe through the following type family:

x:Bool⊒El(x)≔(x= Bool1)Γ—Β¬(x= Bool0)x:\mathrm{Bool} \vdash \mathrm{El}(x) \coloneqq (x =_\mathrm{Bool} 1) \times \neg (x =_\mathrm{Bool} 0)

The extensionality principle of the boolean domain is then given by the univalence axiom:

Ξ“ctxΞ“,x:Bool,y:Bool⊒ua(x,y):Id Bool(x,y)≃(El(x)≃El(y))\frac{\Gamma \; \mathrm{ctx}}{\Gamma, x:\mathrm{Bool}, y:\mathrm{Bool} \vdash \mathrm{ua}(x, y):\mathrm{Id}_\mathrm{Bool}(x, y) \simeq (\mathrm{El}(x) \simeq \mathrm{El}(y))}

Since the empty type is not equivalent to the unit type, this automatically implies that 00 is not equal to 11. The extensionality principle of the boolean domain can be proven from descent of the boolean domain, see Sattler 2023 for a proof.

Relation to sum types

The sum types can be defined in terms of the boolean domain and the dependent sum type. Given types AA and BB, the sum type A+BA + B is defined as

A+Bβ‰”βˆ‘ x:Bool((x= Bool1)β†’A)Γ—((x= Bool0)β†’B)A + B \coloneqq \sum_{x:\mathrm{Bool}} ((x =_\mathrm{Bool} 1) \to A) \times ((x =_\mathrm{Bool} 0) \to B)

Boolean logic

One could recursively define the logical functions on Bool\mathrm{Bool} as follows

  • For negation Β¬\neg
    • Β¬0:=1\neg 0 := 1
    • Β¬1:=0\neg 1 := 0
  • For conjunction ∧\wedge
    • 0∧a:=00 \wedge a := 0
    • 1∧a:=a1 \wedge a := a
  • For disjunction ∨\vee
    • 0∨a:=a0 \vee a := a
    • 1∨a:=11 \vee a := 1
  • For implication β‡’\implies
    • 0β‡’a:=10 \implies a := 1
    • 1β‡’a:=a1 \implies a := a
  • For the biconditional ⇔\iff
    • 0⇔a:=Β¬a0 \iff a := \neg a
    • 1⇔a:=a1 \iff a := a

One could prove that (Bool,0,1,Β¬,∧,∨,β‡’)(\mathrm{Bool}, 0, 1, \neg, \wedge, \vee, \implies) form a Boolean algebra. The poset structure is given by implication.

One could also inductively define observational equality on the booleans Eq Bool(x,y)\mathrm{Eq}_\mathrm{Bool}(x, y) as an indexed inductive type on the boolean type Bool\mathrm{Bool} with the following constructors

eq 0:Eq 𝟚(0,0)\mathrm{eq}_0: \mathrm{Eq}_\mathbb{2}(0, 0)
eq 1:Eq 𝟚(1,1)\mathrm{eq}_1: \mathrm{Eq}_\mathbb{2}(1, 1)

A boolean predicate valued in a type TT is a function P:T→BoolP: T \rightarrow \mathrm{Bool}, and the type T→BoolT \to \mathrm{Bool} is a boolean function algebra for finite types TT, and if path types exist, for all types TT. Thus the functor F:U→BoolAlgF: U \to BoolAlg, F(T)=T→BoolF(T) = T \to \mathrm{Bool} for a type universe UU is a Boolean hyperdoctrine, and one could do classical first-order logic inside UU if Bool\mathrm{Bool} and path types exist in UU.

In fact, just with dependent sum types, dependent product types, empty type, unit type, and the two-valued type in a type universe UU, any two-valued logic could be done inside UU. Furthermore, since binary disjoint coproducts exist when Bool\mathrm{Bool} exists, all finite types exist in UU, and any finitely-valued logic?, such as the internal logic of a finite cartesian power of Set, could be done inside UU.

For finite types, one could also inductively define specific functions

βˆ€a∈A.(βˆ’)(a):(Aβ†’Bool)β†’Bool\forall a \in A.(-)(a):(A \to \mathrm{Bool}) \to \mathrm{Bool}
βˆƒa∈A.(βˆ’)(a):(Aβ†’2)β†’Bool\exists a \in A.(-)(a):(A \to \mathbf{2}) \to \mathrm{Bool}

from the type of boolean predicates on AA and Bool\mathrm{Bool} such that they behave like existential quantification and universal quantification.

Other properties

Boolβ‰…βˆ‘ P:𝒰isProp(P)Γ—isDecidable(P)\mathrm{Bool} \cong \sum_{P:\mathcal{U}} isProp(P) \times isDecidable(P)

As a result, sometimes the boolean domain is called a decidable subset classifier.

References

See also:

Discussion in type theory as a simple example of an inductive type:

Discussion in homotopy type theory:

…

Large elimination and descent of the boolean domain can be found in

Last revised on February 21, 2024 at 08:05:55. See the history of this page for a list of all contributions to it.