Type of booleans

The type of booleans $𝟚$ has two canonical terms: true and false. 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 $𝖲 𝖾 𝗍$ 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

Here we give a formal presentation of $𝟚$ in the cartesian calculus of substitutions, following Principles of dependent type theory. #m/def/type/ind The formation rule is

Γ ⊢ Γ ⊢ 𝟚 (𝟚) Δ ⊢ 𝛾 : Γ Δ ⊢ 𝟚 [𝛾] = 𝟚 (𝟚 - N) .

$𝟚$ is an inductive type with two constructors for “true” and “false”

Γ ⊢ Γ ⊢ 𝐭 𝐫 𝐮 𝐞 : 𝟚 (𝟚 I t) Γ ⊢ Γ ⊢ 𝐟 𝐚 𝐥 𝐬 𝐞 : 𝟚 (𝟚 I f)

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐭 𝐫 𝐮 𝐞 [𝛾] = 𝐭 𝐫 𝐮 𝐞 : 𝟚 (𝟚 I t - N) Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐟 𝐚 𝐥 𝐬 𝐞 [𝛾] = 𝐟 𝐚 𝐥 𝐬 𝐞 : 𝟚 (𝟚 I f - N)

Thus the induction principle gives the elimination rule

Γ . 𝟚 ⊢ 𝐴 Γ ⊢ 𝑎 t : 𝐴 [𝐢 𝐝 . 𝐭 𝐫 𝐮 𝐞] Γ ⊢ 𝑎 f : 𝐴 [𝐢 𝐝 . 𝐟 𝐚 𝐥 𝐬 𝐞] Γ ⊢ 𝑏 : 𝟚 Γ ⊢ 𝐢 𝐟 (𝑏, 𝑎 t, 𝑎 f) : 𝐴 [𝐢 𝐝 . 𝑏] (𝟚 E)

Δ ⊢ 𝛾 : Γ Γ . 𝟚 ⊢ 𝐴 Γ ⊢ 𝑎 t : 𝐴 [𝐢 𝐝 . 𝐭 𝐫 𝐮 𝐞] Γ ⊢ 𝑎 f : 𝐴 [𝐢 𝐝 . 𝐟 𝐚 𝐥 𝐬 𝐞] Γ ⊢ 𝑏 : 𝟚 Γ ⊢ 𝐢 𝐟 (𝑏, 𝑎 t, 𝑎 f) [𝛾] = 𝐢 𝐟 (𝑏 [𝛾], 𝑎 t [𝛾], 𝑎 f [𝛾]) : 𝐴 [𝛾 . 𝑏 [𝛾]] (𝟚 E - N)

and $𝛽$ -computation rules

Γ . 𝟚 ⊢ 𝐴 Γ ⊢ 𝑎 t : 𝐴 [𝐢 𝐝 . 𝐭 𝐫 𝐮 𝐞] Γ ⊢ 𝑎 f : 𝐴 [𝐢 𝐝] . 𝐟 𝐚 𝐥 𝐬 𝐞 Γ ⊢ 𝐢 𝐟 (𝐭 𝐫 𝐮 𝐞, 𝑎 t, 𝑎 f) = 𝑎 t : 𝐴 [𝐢 𝐝 . 𝐭 𝐫 𝐮 𝐞] (𝟚 𝛽 t)

Γ . 𝟚 ⊢ 𝐴 Γ ⊢ 𝑎 t : 𝐴 [𝐢 𝐝 . 𝐭 𝐫 𝐮 𝐞] Γ ⊢ 𝑎 f : 𝐴 [𝐢 𝐝] . 𝐟 𝐚 𝐥 𝐬 𝐞 Γ ⊢ 𝐢 𝐟 (𝐟 𝐚 𝐥 𝐬 𝐞, 𝑎 t, 𝑎 f) = 𝑎 f : 𝐴 [𝐢 𝐝 . 𝐟 𝐚 𝐥 𝐬 𝐞] (𝟚 𝛽 f)

We omit an $𝜂$ -unicity rule in the standard presentation, since it can be shown given an Extensional equality type.

Agda

1Lab

data Bool : Type where
  true false : Bool

Internalizing judgemental structure

In terms of Internalizing judgemental structure, we have for any context $Γ$

𝟚 Γ \in T y (Γ); 𝐭 𝐫 𝐮 𝐞 Γ, 𝐟 𝐚 𝐥 𝐬 𝐞 Γ \in T m (Γ, 𝟚)

and for any dependent type $Γ . 𝟚 ⊢ 𝐴$ ,

((𝐢 𝐝 . 𝐭 𝐫 𝐮 𝐞) *, (𝐢 𝐝 . 𝐟 𝐚 𝐥 𝐬 𝐞) *) : T m (Γ . 𝟚, 𝐴) ≅ T m (Γ, 𝐴 [𝐢 𝐝 . 𝐭 𝐫 𝐮 𝐞]) \times T m (Γ, 𝐴 [𝐢 𝐝 . 𝐟 𝐚 𝐥 𝐬 𝐞]),

is a bijection natural in $Γ$ , where we have used the pullback meta-function ^PB3 and the universal property of the product in the metatheory.

#state/tidy | #lang/en | #SemBr

See ETCS. ↩

Type of booleans

Standard presentation

Internalizing judgemental structure

Footnotes