# Maths - Boolean Types

We can use sum to get boolean from two units (1+1=2)

### Rules

Types are defined by their formation, term introduction, term eliminator and computation rules:

Boolean Type

formation rule

dont really need to have two copies of Unit, just making the point this is a sum. Unit:Type Unit:Type Boolean : Type
term introduction rule
 Γ a:Unit Γ b:Unit Γ inl(a): Boolean Γ inr(b): Boolean

term eliminator

assume: a implies c
and b implies c

 Γ p:Boolean Γ a:Unit cA :C Γ b:Unit cB :C Γ match(p, a.cA b.cB):C
computation rule

beta reduction

match(inl(a), x.cA y.cB) ->β cA[a/x]

match(inr(b), x.cA y.cB) ->β cB[b/x]

Local completeness rule

#### Idris Code

Idris Code for Boolean is here.

 The formation and term introduction rules can be represented simply in Idris like this: ```||| Boolean Data Type data Bool = False | True``` The term eliminator can be implemented by the if-then-else construct or perhaps, a bit more generally the 'case' construct. ```||| The underlying implementation of the if ... then ... else ... syntax ||| @ b the condition on the if ||| @ t the value if b is true ||| @ e the value if b is false ifThenElse : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a ifThenElse True t e = t ifThenElse False t e = e``` computation and local completeness rules ```if True then True else False if False then False else True ```

### Negation

formation rule

term introduction rule

 P   ¬P
term eliminator
computation rule

Local completeness rule

#### Bottom Rule

formation rule

term introduction rule P ¬P  term eliminator
computation rule

Local completeness rule

```
The formation rule (e.g. Bool : Set)

The introduction rules (e.g. true : Bool and false : Bool)

The elimination rules (e.g. if P : Bool -> Set, b : Bool, pt : P true, and pf : P false, then if b then pt else pf : P b)

The computation rules (e.g. if true then pt else pf = pt and if false then pt else pf = pf)
```

We can use sum to get boolean from two units (1+1=2)

Boolean Type

formation rule

dont really need to have two copies of Unit, just making the point this is a sum. Unit:Type Unit:Type Boolean : Type
term introduction rule
 Γ a:Unit Γ b:Unit Γ inl(a): Boolean Γ inr(b): Boolean

term eliminator

assume: a implies c
and b implies c

 Γ p:Boolean Γ a:Unit  cA :C Γ b:Unit  cB :C Γ match(p, a.cA b.cB):C
computation rule

beta reduction

match(inl(a), x.cA y.cB) ->β cA[a/x]

match(inr(b), x.cA y.cB) ->β cB[b/x]

Local completeness rule

#### Negation Rule

formation rule

term introduction rule

 P   ¬P
term eliminator
computation rule

Local completeness rule

#### Bottom Rule

formation rule

term introduction rule P ¬P  term eliminator
computation rule

Local completeness rule

### Next Steps

Other types are discussed on the following pages:

http://www.mathreference.com/

Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them.      Computation and Reasoning - This book is about type theory. Although it is very technical it is aimed at computer scientists, so it has more discussion than a book aimed at pure mathematicians. It is especially useful for the coverage of dependant types.