diff --git a/src/Naturals.idr b/src/Naturals.idr
index 0766666..93e1b4e 100644
--- a/src/Naturals.idr
+++ b/src/Naturals.idr
@@ -1,4 +1,37 @@
 module Naturals
 
-main : IO ()
-main = putStrLn "Hello!"
+%default total
+
+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