Natural Number Type
Natural numbers can be defined in terms of Peano algebra. This is not very practical for everyday use but has nice properties for proving things about natural numbers.
Elimination is usually a way to prove properties of inductivly defined types like this.
For example, for natural numbers: 
nat_induction : (prop : Nat > Type) >  Property to show (prop Z) >  Base case ((k : Nat) > prop k > prop (S k)) >  Inductive step (x : Nat) >  Show for all x prop x nat_induction prop p_Z p_S Z = p_Z nat_induction prop p_Z p_S (S k) = p_S k (nat_induction prop p_Z p_S k) 
That is, for all properties on natural numbers, if it holds for zero and P n implies P (S n) then the property holds for all numbers. (proof by induction).
Notation
Rules
Types are defined by their formation, term introduction, term eliminator and computation rules.
In order to avoid having a infinite number of constructors we can define Nat in terms of functions Z and S.
Nat Type 


formation rule N exists 


term introduction rules



term eliminator Proof by induction To prove property P (implemented as a type) we need to proove P(0) and P(x) implies P(sx) rec is recursor (see recursor section above) where: rec
nat
z_{0} z_{s} O
=
z_{0} where



computation rules 



Idris Code
Idris Code for Nat is here.
The formation and term introduction rules can be represented in Idris like this: 
data Nat = Z  S Nat 
The term eliminator can be implemented by the 'case' construct.  
computation and local completeness rules  ie 
Computer Implementation
How do we implement natural numbers in computer algebra and proof assistant programs? Some alternatives are:
 Define inductively from Zero and Successor as in Coq (Calculus of Inductive Constructions) .
 Define them as predicates in higher order logic.
 Define them axiomatically.
defined inductively  predicates in higher order logic  define them axiomatically  

advantages  Can automatically generate induction proof principle. Can define functions by wellfounded recursion. 
Keeps program simple Don't need to show each recursive definition represents a terminating algorithm, unique for each input. 

disadvantages  each function requires a proof. 
Idris
Elimination (pattern matching) is built in to Idris. 
data Nat =  Zero Z   Successor S Nat Eq Nat where Z == Z = True (S l) == (S r) = l == r _ == _ = False 
Coq
github  Inductive nat : Set :=  0 : nat  S : nat > nat. 
Enumeration Type
An enumerated type is any type given by a finite disjoint sum of unit types.
Can be thought of as a sum (1+1...) or as a degenerate form of an inductive type.
Inductive Types
Natural Number Type
Natural Number Type 


formation rule N exists 


term introduction rules



term eliminator Proof by induction To prove property P (implemented as a type) we need to proove P(0) and P(x) implies P(sx) rec is recursor (see recursor section above) where: rec
nat
z_{0} z_{s} O
=
z_{0} where



computation rules 



WTypes
This is ageneralisation of the way natural numbers can be inductivly defined, see page here.
Next Steps
Other types are discussed on the following pages: