Type theory MOC

Type of booleans

The type of booleans 𝟚 has two canonical terms: 0 and 1, often called false and true. In (non-dependent) programming and classical mathematics, predicates are usually thought of as having values in 𝟚.

0 == 1 # False
1 == 1 # True

This is justified by the fact that, in the category Category of sets of classical mathematics,¹ the corresponding set 𝟚 is a subobject classifier. In constructive contexts where the Law of excluded middle is not assumed, however, this is not the case (we instead need a Universe of propositions Ω), so the role played by 𝟚 is quite different.

Standard presentation

The type of booleans is usually defined in a type theory as a positive inductive type. The standard presentation is as follows: ind

1. Formation rule

⊢𝟚

2. Introduction rules

⊢0:𝟚⊢1:𝟚

3. Induction rule

Γ,𝑥:𝟚⊢𝐶(𝑥)Γ,𝑐0:𝐶(0),𝑐1:𝐶(1),𝑝:𝟚⊢ind𝟚⁡(𝑐0,𝑐1,𝑝):𝐶(𝑝)

4. Judgemental computation rules

Γ,𝑥:𝟚⊢𝐶(𝑥)Γ,𝑐0:𝐶(0),𝑐1:𝐶(1)⊢ind𝟚⁡(𝑐0,𝑐1,0)=𝑐0:𝐶(0)Γ,𝑥:𝟚⊢𝐶(𝑥)Γ,𝑐0:𝐶(0),𝑐1:𝐶(1)⊢ind𝟚⁡(𝑐0,𝑐1,1)=𝑐1:𝐶(1)

Agda

1Lab

data Bool : Type where
  true false : Bool

---

develop | en | SemBr

Footnotes

1. See ETCS. ↩