Type theory MOC

Type of booleans

The type of booleans has two canonical terms: and , 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 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: #m/def/type/ind

1. Formation rule

2. Introduction rules

3. Induction rule

4. Judgemental computation rules

data Bool : Type where
  true false : Bool

#state/develop | #lang/en | #SemBr