data Digit : Type
This is essentially Bool but with names that are easier to understand
O : Digit
I : Digit
isI : Digit -> Bool
Translation to Bool
toNat : Digit -> Nat