We can use sum to get boolean from two units (1+1=2)
Notation
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. 


term introduction rule 


term eliminator assume: a implies c 


computation rule  beta reduction match(inl(a), x.c_{A} y.c_{B}) >_{β} c_{A}[a/x] match(inr(b), x.c_{A} y.c_{B}) >_{β} c_{B}[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 ifthenelse 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
We can then add negation
formation rule 

term introduction rule 


term eliminator  
computation rule  
Local completeness rule 
Bottom Rule
formation rule 

term introduction rule 


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. 


term introduction rule 


term eliminator assume: a implies c 


computation rule  beta reduction match(inl(a), x.c_{A} y.c_{B}) >_{β} c_{A}[a/x] match(inr(b), x.c_{A} y.c_{B}) >_{β} c_{B}[b/x] 

Local completeness rule 
We can then add negation
Negation Rule
formation rule 

term introduction rule 


term eliminator  
computation rule  
Local completeness rule 
Bottom Rule
formation rule 

term introduction rule 


term eliminator  
computation rule  
Local completeness rule 
Next Steps
Other types are discussed on the following pages: