Define the natural numbers

src/Naturals.idr

@@ -1,4 +1,37 @@
 module Naturals
 
-main : IO ()
+%default total
-main = putStrLn "Hello!"
+
+data Natural : Type where
+  ||| Zero is a natural number
+  Zero : Natural
+  ||| The successor of a natural n is a natural
+  S : Natural -> Natural
+
+one : Natural
+one = S Zero
+
+two : Natural
+two = S (S Zero)
+
+data Equality : Natural -> Natural -> Type where
+  ||| A natural n is equal to itself
+  Reflexive : {n : Natural} -> Equality n n
+
+oneEqualsOne : Equality (S Zero) (S Zero)
+oneEqualsOne = Reflexive
+
+zeroNotEqualOne : Equality (S Zero) Zero -> Void
+zeroNotEqualOne x impossible
+
+symmetric : (n, m : Natural) -> Equality n m -> Equality m n
+symmetric n n Reflexive = Reflexive
+
+transitive : (n, m, o : Natural) -> Equality n m -> Equality m o -> Equality n o
+transitive n n n Reflexive Reflexive = Reflexive
+
+injection : (n, m : Natural) -> Equality (S n) (S m) -> Equality n m
+injection n n Reflexive = Reflexive
+
+succNotZero : (n : Natural) -> Equality (S n) Zero -> Void
+succNotZero _ Reflexive impossible