diff --git a/lib/Haskell/Law.agda b/lib/Haskell/Law.agda
index a6cb54ee..d793b20c 100644
--- a/lib/Haskell/Law.agda
+++ b/lib/Haskell/Law.agda
@@ -3,13 +3,18 @@ module Haskell.Law where
 open import Haskell.Prim
 open import Haskell.Prim.Bool
 
+open import Haskell.Law.Def          public
 open import Haskell.Law.Applicative  public
 open import Haskell.Law.Bool         public
+open import Haskell.Law.Either       public
 open import Haskell.Law.Eq           public
 open import Haskell.Law.Equality     public
 open import Haskell.Law.Functor      public
+open import Haskell.Law.Int          public
+open import Haskell.Law.Integer      public
 open import Haskell.Law.List         public
 open import Haskell.Law.Maybe        public
 open import Haskell.Law.Monad        public
 open import Haskell.Law.Monoid       public
+open import Haskell.Law.Nat          public
 open import Haskell.Law.Ord          public
diff --git a/lib/Haskell/Law/Def.agda b/lib/Haskell/Law/Def.agda
new file mode 100644
index 00000000..1099dcf6
--- /dev/null
+++ b/lib/Haskell/Law/Def.agda
@@ -0,0 +1,6 @@
+module Haskell.Law.Def where
+
+open import Haskell.Prim
+
+Injective : (a → b) → Set _
+Injective f = ∀ {x y} → f x ≡ f y → x ≡ y
diff --git a/lib/Haskell/Law/Either.agda b/lib/Haskell/Law/Either.agda
new file mode 100644
index 00000000..4157885c
--- /dev/null
+++ b/lib/Haskell/Law/Either.agda
@@ -0,0 +1,12 @@
+module Haskell.Law.Either where
+
+open import Haskell.Prim
+open import Haskell.Prim.Either
+
+open import Haskell.Law.Def
+
+Left-injective : Injective (Left {a}{b})
+Left-injective refl = refl
+
+Right-injective : Injective (Right {a}{b})
+Right-injective refl = refl
diff --git a/lib/Haskell/Law/Eq.agda b/lib/Haskell/Law/Eq.agda
index 56bd326a..9a4c46fd 100644
--- a/lib/Haskell/Law/Eq.agda
+++ b/lib/Haskell/Law/Eq.agda
@@ -1,6 +1,4 @@
 module Haskell.Law.Eq where
 
-open import Haskell.Law.Eq.Def      public
-open import Haskell.Law.Eq.Bool     public
-open import Haskell.Law.Eq.Maybe    public
-open import Haskell.Law.Eq.Ordering public
+open import Haskell.Law.Eq.Def       public
+open import Haskell.Law.Eq.Instances public
diff --git a/lib/Haskell/Law/Eq/Bool.agda b/lib/Haskell/Law/Eq/Bool.agda
deleted file mode 100644
index e4c4a20d..00000000
--- a/lib/Haskell/Law/Eq/Bool.agda
+++ /dev/null
@@ -1,15 +0,0 @@
-module Haskell.Law.Eq.Bool where
-
-open import Haskell.Prim
-open import Haskell.Prim.Eq
-
-open import Haskell.Law.Eq.Def
-open import Haskell.Law.Equality
-
-instance
-  iLawfulEqBool : IsLawfulEq Bool
-  iLawfulEqBool .isEquality False False = refl
-  iLawfulEqBool .isEquality False True = λ()
-  iLawfulEqBool .isEquality True False = λ()
-  iLawfulEqBool .isEquality True True = refl
-
diff --git a/lib/Haskell/Law/Eq/Def.agda b/lib/Haskell/Law/Eq/Def.agda
index cd657b15..53781813 100644
--- a/lib/Haskell/Law/Eq/Def.agda
+++ b/lib/Haskell/Law/Eq/Def.agda
@@ -2,13 +2,7 @@ module Haskell.Law.Eq.Def where
 
 open import Haskell.Prim
 open import Haskell.Prim.Bool
-open import Haskell.Prim.Integer
-open import Haskell.Prim.Int
-open import Haskell.Prim.Word
 open import Haskell.Prim.Double
-open import Haskell.Prim.Tuple
-open import Haskell.Prim.Maybe
-open import Haskell.Prim.Either
 
 open import Haskell.Prim.Eq
 
@@ -73,28 +67,4 @@ eqNegation : ⦃ iEq : Eq e ⦄ → ⦃ IsLawfulEq e ⦄
 eqNegation = refl
 
 postulate instance
-  iLawfulEqNat : IsLawfulEq Nat
-
-  iLawfulEqInteger : IsLawfulEq Integer
-
-  iLawfulEqInt : IsLawfulEq Int
-
-  iLawfulEqWord : IsLawfulEq Word
-
   iLawfulEqDouble : IsLawfulEq Double
-
-  iLawfulEqChar : IsLawfulEq Char
-
-  iLawfulEqUnit : IsLawfulEq ⊤
-
-  iLawfulEqTuple₂ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄
-                  → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄
-                  → IsLawfulEq (a × b)
-
-  iLawfulEqTuple₃ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ ⦃ iEqC : Eq c ⦄
-                  → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → ⦃ IsLawfulEq c ⦄
-                  → IsLawfulEq (a × b × c)
-
-  iLawfulEqList : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (List a)
-
-  iLawfulEqEither : ⦃ iEqA : Eq a ⦄ → ⦃ iEqB : Eq b ⦄ → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → Eq (Either a b)
diff --git a/lib/Haskell/Law/Eq/Instances.agda b/lib/Haskell/Law/Eq/Instances.agda
new file mode 100644
index 00000000..da7ef9b3
--- /dev/null
+++ b/lib/Haskell/Law/Eq/Instances.agda
@@ -0,0 +1,135 @@
+module Haskell.Law.Eq.Instances where
+
+open import Agda.Builtin.Char.Properties renaming (primCharToNatInjective to c2n-injective)
+open import Agda.Builtin.Word.Properties renaming (primWord64ToNatInjective to w2n-injective)
+
+open import Haskell.Prim
+open import Haskell.Prim.Eq
+
+open import Haskell.Prim.Either using ( Either; Left; Right )
+open import Haskell.Prim.Int    using ( Int; int64 )
+open import Haskell.Prim.Maybe
+open import Haskell.Prim.Ord    using ( Ordering; LT; GT; EQ )
+open import Haskell.Prim.Tuple
+open import Haskell.Prim.Word   using ( Word )
+
+open import Haskell.Extra.Dec   using ( mapReflects )
+
+open import Haskell.Law.Eq.Def
+open import Haskell.Law.Equality
+
+open import Haskell.Law.Either
+open import Haskell.Law.Int
+open import Haskell.Law.Integer
+open import Haskell.Law.List    using ( ∷-injective-left; ∷-injective-right )
+open import Haskell.Law.Maybe
+open import Haskell.Law.Nat
+
+instance
+  iLawfulEqNat : IsLawfulEq Nat
+  iLawfulEqNat .isEquality zero    zero    = refl
+  iLawfulEqNat .isEquality zero    (suc _) = λ ()
+  iLawfulEqNat .isEquality (suc _) zero    = λ ()
+  iLawfulEqNat .isEquality (suc x) (suc y) = mapReflects 
+    (cong suc) 
+    suc-injective 
+    (isEquality x y)
+
+  iLawfulEqWord : IsLawfulEq Word
+  iLawfulEqWord .isEquality x y 
+    with (w2n x) in h₁ | (w2n y) in h₂ 
+  ... | a | b  = mapReflects
+    (λ h → w2n-injective x y $ sym $ trans (trans h₂ $ sym h) (sym h₁))
+    (λ h → trans (sym $ trans (cong w2n (sym h)) h₁) h₂)
+    (isEquality a b)
+
+  iLawfulEqBool : IsLawfulEq Bool
+  iLawfulEqBool .isEquality False False = refl
+  iLawfulEqBool .isEquality False True  = λ()
+  iLawfulEqBool .isEquality True  False = λ()
+  iLawfulEqBool .isEquality True  True  = refl
+
+  iLawfulEqChar : IsLawfulEq Char
+  iLawfulEqChar .isEquality x y 
+    with (c2n x) in h₁ | (c2n y) in h₂ 
+  ... | a | b  = mapReflects { a ≡ b } { x ≡ y } { eqNat a b } 
+    (λ h → c2n-injective x y $ sym $ trans (trans h₂ $ sym h) (sym h₁))
+    (λ h → trans (sym $ trans (cong c2n (sym h)) h₁) h₂)
+    (isEquality a b)
+
+  iLawfulEqEither : ⦃ iEqA : Eq a ⦄ → ⦃ iEqB : Eq b ⦄ 
+    → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ 
+    → IsLawfulEq (Either a b)
+  iLawfulEqEither .isEquality (Left  _) (Right _) = λ ()
+  iLawfulEqEither .isEquality (Right _) (Left  _) = λ ()
+  iLawfulEqEither .isEquality (Left  x) (Left  y) = mapReflects 
+    (cong Left) (Left-injective) (isEquality x y)
+  iLawfulEqEither .isEquality (Right x) (Right y) = mapReflects 
+    (cong Right) (Right-injective) (isEquality x y)
+
+  iLawfulEqInt : IsLawfulEq Int
+  iLawfulEqInt .isEquality (int64 x) (int64 y) = mapReflects
+    (cong int64) int64-injective (isEquality x y) 
+
+  iLawfulEqInteger : IsLawfulEq Integer
+  iLawfulEqInteger .isEquality (pos n)    (pos m)    = mapReflects 
+    (cong pos) pos-injective (isEquality n m)
+  iLawfulEqInteger .isEquality (pos _)    (negsuc _) = λ () 
+  iLawfulEqInteger .isEquality (negsuc _) (pos _)    = λ ()
+  iLawfulEqInteger .isEquality (negsuc n) (negsuc m) = mapReflects 
+    (cong negsuc) neg-injective (isEquality n m)
+  
+  iLawfulEqList : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (List a)
+  iLawfulEqList .isEquality []       []      = refl
+  iLawfulEqList .isEquality []       (_ ∷ _) = λ ()
+  iLawfulEqList .isEquality (_ ∷ _)  []      = λ ()
+  iLawfulEqList .isEquality (x ∷ xs) (y ∷ ys) 
+    with (x == y) in h₁
+  ... | True  = mapReflects 
+    (λ h → cong₂ (_∷_) (equality x y h₁)  h) 
+    ∷-injective-right 
+    (isEquality xs ys)
+  ... | False = λ h → (nequality x y h₁) (∷-injective-left h)
+
+  iLawfulEqMaybe : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (Maybe a)
+  iLawfulEqMaybe .isEquality Nothing  Nothing  = refl
+  iLawfulEqMaybe .isEquality Nothing  (Just _) = λ()
+  iLawfulEqMaybe .isEquality (Just _) Nothing  = λ()
+  iLawfulEqMaybe .isEquality (Just x) (Just y) = mapReflects 
+    (cong Just) Just-injective (isEquality x y)
+
+  iLawfulEqOrdering : IsLawfulEq Ordering
+  iLawfulEqOrdering .isEquality LT LT = refl
+  iLawfulEqOrdering .isEquality LT EQ = λ()
+  iLawfulEqOrdering .isEquality LT GT = λ()
+  iLawfulEqOrdering .isEquality EQ LT = λ()
+  iLawfulEqOrdering .isEquality EQ EQ = refl
+  iLawfulEqOrdering .isEquality EQ GT = λ()
+  iLawfulEqOrdering .isEquality GT LT = λ()
+  iLawfulEqOrdering .isEquality GT EQ = λ()
+  iLawfulEqOrdering .isEquality GT GT = refl
+
+  iLawfulEqTuple₂ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄
+    → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄
+    → IsLawfulEq (a × b)
+  iLawfulEqTuple₂ .isEquality (x₁ , x₂) (y₁ , y₂)
+    with (x₁ == y₁) in h₁
+  ... | True  = mapReflects
+    (λ h → cong₂ _,_ (equality x₁ y₁ h₁) h) 
+    (cong snd) 
+    (isEquality x₂ y₂)
+  ... | False = λ h → exFalso (equality' x₁ y₁ (cong fst h)) h₁
+
+  iLawfulEqTuple₃ : ⦃ iEqA : Eq a ⦄ ⦃ iEqB : Eq b ⦄ ⦃ iEqC : Eq c ⦄
+    → ⦃ IsLawfulEq a ⦄ → ⦃ IsLawfulEq b ⦄ → ⦃ IsLawfulEq c ⦄
+    → IsLawfulEq (a × b × c)
+  iLawfulEqTuple₃ .isEquality (x₁ , x₂ , x₃) (y₁ , y₂ , y₃) 
+    with (x₁ == y₁) in h₁ 
+  ... | True  = mapReflects
+    (λ h → cong₂ (λ a (b , c) → a , b , c) (equality x₁ y₁ h₁) h) 
+    (cong λ h → snd₃ h , thd₃ h) 
+    (isEquality (x₂ , x₃) (y₂ , y₃))
+  ... | False = λ h → exFalso (equality' x₁ y₁ (cong  fst₃ h)) h₁ 
+
+  iLawfulEqUnit : IsLawfulEq ⊤
+  iLawfulEqUnit .isEquality tt tt = refl
diff --git a/lib/Haskell/Law/Eq/Maybe.agda b/lib/Haskell/Law/Eq/Maybe.agda
deleted file mode 100644
index b01af12b..00000000
--- a/lib/Haskell/Law/Eq/Maybe.agda
+++ /dev/null
@@ -1,19 +0,0 @@
-module Haskell.Law.Eq.Maybe where
-
-open import Haskell.Prim
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Maybe
-
-open import Haskell.Extra.Dec
-
-open import Haskell.Law.Eq.Def
-open import Haskell.Law.Equality
-open import Haskell.Law.Maybe
-
-instance
-  iLawfulEqMaybe : ⦃ iEqA : Eq a ⦄ → ⦃ IsLawfulEq a ⦄ → IsLawfulEq (Maybe a)
-  iLawfulEqMaybe .isEquality Nothing Nothing = refl
-  iLawfulEqMaybe .isEquality Nothing (Just _) = λ()
-  iLawfulEqMaybe .isEquality (Just _) Nothing = λ()
-  iLawfulEqMaybe .isEquality (Just x) (Just y) = mapReflects (cong Just) injective (isEquality x y)
-
diff --git a/lib/Haskell/Law/Eq/Ordering.agda b/lib/Haskell/Law/Eq/Ordering.agda
deleted file mode 100644
index 58c3277c..00000000
--- a/lib/Haskell/Law/Eq/Ordering.agda
+++ /dev/null
@@ -1,22 +0,0 @@
-module Haskell.Law.Eq.Ordering where
-
-open import Haskell.Prim
-open import Haskell.Prim.Eq
-open import Haskell.Prim.Ord using ( Ordering; LT; GT; EQ )
-
-open import Haskell.Law.Eq.Def
-open import Haskell.Law.Equality
-
-instance
-  iLawfulEqOrdering : IsLawfulEq Ordering
-
-  iLawfulEqOrdering .isEquality LT LT = refl
-  iLawfulEqOrdering .isEquality LT EQ = λ()
-  iLawfulEqOrdering .isEquality LT GT = λ()
-  iLawfulEqOrdering .isEquality EQ LT = λ()
-  iLawfulEqOrdering .isEquality EQ EQ = refl
-  iLawfulEqOrdering .isEquality EQ GT = λ()
-  iLawfulEqOrdering .isEquality GT LT = λ()
-  iLawfulEqOrdering .isEquality GT EQ = λ()
-  iLawfulEqOrdering .isEquality GT GT = refl
-
diff --git a/lib/Haskell/Law/Int.agda b/lib/Haskell/Law/Int.agda
new file mode 100644
index 00000000..8fd40caa
--- /dev/null
+++ b/lib/Haskell/Law/Int.agda
@@ -0,0 +1,9 @@
+module Haskell.Law.Int where
+
+open import Haskell.Prim
+open import Haskell.Prim.Int using ( int64 )
+
+open import Haskell.Law.Def
+
+int64-injective : Injective int64
+int64-injective refl = refl 
diff --git a/lib/Haskell/Law/Integer.agda b/lib/Haskell/Law/Integer.agda
new file mode 100644
index 00000000..37005798
--- /dev/null
+++ b/lib/Haskell/Law/Integer.agda
@@ -0,0 +1,11 @@
+module Haskell.Law.Integer where
+
+open import Haskell.Prim
+
+open import Haskell.Law.Def
+
+pos-injective : Injective pos
+pos-injective refl = refl
+
+neg-injective : Injective negsuc
+neg-injective refl = refl
diff --git a/lib/Haskell/Law/Maybe.agda b/lib/Haskell/Law/Maybe.agda
index ec4203ba..348140d8 100644
--- a/lib/Haskell/Law/Maybe.agda
+++ b/lib/Haskell/Law/Maybe.agda
@@ -3,5 +3,7 @@ module Haskell.Law.Maybe where
 open import Haskell.Prim
 open import Haskell.Prim.Maybe
 
-injective : ∀ {x y : a} → Just x ≡ Just y → x ≡ y
-injective refl = refl
+open import Haskell.Law.Def
+
+Just-injective : Injective (Just {a = a})
+Just-injective refl = refl
diff --git a/lib/Haskell/Law/Nat.agda b/lib/Haskell/Law/Nat.agda
new file mode 100644
index 00000000..b10981fb
--- /dev/null
+++ b/lib/Haskell/Law/Nat.agda
@@ -0,0 +1,8 @@
+module Haskell.Law.Nat where
+
+open import Haskell.Prim
+
+open import Haskell.Law.Def
+
+suc-injective : Injective suc
+suc-injective refl = refl
diff --git a/lib/Haskell/Prelude.agda b/lib/Haskell/Prelude.agda
index 78cca2bc..a0bb63e8 100644
--- a/lib/Haskell/Prelude.agda
+++ b/lib/Haskell/Prelude.agda
@@ -18,6 +18,7 @@ open import Haskell.Prim.Absurd      public
 open import Haskell.Prim.Applicative public
 open import Haskell.Prim.Bool        public
 open import Haskell.Prim.Bounded     public
+open import Haskell.Prim.Char        public
 open import Haskell.Prim.Double      public
 open import Haskell.Prim.Either      public
 open import Haskell.Prim.Enum        public
diff --git a/lib/Haskell/Prim.agda b/lib/Haskell/Prim.agda
index abc39993..65f6e3f5 100644
--- a/lib/Haskell/Prim.agda
+++ b/lib/Haskell/Prim.agda
@@ -11,7 +11,7 @@ open import Agda.Primitive          public
 open import Agda.Builtin.Bool       public renaming (true to True; false to False)
 open import Agda.Builtin.Int        public renaming (Int to Integer)
 open import Agda.Builtin.Nat        public renaming (_==_ to eqNat; _<_ to ltNat; _+_ to addNat; _-_ to monusNat; _*_ to mulNat)
-open import Agda.Builtin.Char       public
+open import Agda.Builtin.Char       public renaming (primCharToNat to c2n)
 open import Agda.Builtin.Unit       public
 open import Agda.Builtin.Equality   public
 open import Agda.Builtin.FromString public
diff --git a/lib/Haskell/Prim/Char.agda b/lib/Haskell/Prim/Char.agda
new file mode 100644
index 00000000..8883bdb0
--- /dev/null
+++ b/lib/Haskell/Prim/Char.agda
@@ -0,0 +1,9 @@
+module Haskell.Prim.Char where
+
+open import Haskell.Prim
+
+import Agda.Builtin.Char 
+open Agda.Builtin.Char using (Char)
+    
+eqChar : Char → Char → Bool
+eqChar a b = eqNat (c2n a) (c2n b)
diff --git a/lib/Haskell/Prim/Enum.agda b/lib/Haskell/Prim/Enum.agda
index 1eca84e6..3e5e6c02 100644
--- a/lib/Haskell/Prim/Enum.agda
+++ b/lib/Haskell/Prim/Enum.agda
@@ -196,7 +196,7 @@ instance
   iEnumUnit = boundedEnumViaInteger (λ _ → 0) λ _ → tt
 
   iEnumChar : Enum Char
-  iEnumChar = boundedEnumViaInteger (pos ∘ primCharToNat)
+  iEnumChar = boundedEnumViaInteger (pos ∘ c2n)
                                     λ where (pos n) → primNatToChar n; _ → '_'
 
   -- Missing:
diff --git a/lib/Haskell/Prim/Eq.agda b/lib/Haskell/Prim/Eq.agda
index b17820ed..f8bcd23a 100644
--- a/lib/Haskell/Prim/Eq.agda
+++ b/lib/Haskell/Prim/Eq.agda
@@ -3,6 +3,7 @@ module Haskell.Prim.Eq where
 
 open import Haskell.Prim
 open import Haskell.Prim.Bool
+open import Haskell.Prim.Char
 open import Haskell.Prim.Integer
 open import Haskell.Prim.Int
 open import Haskell.Prim.Word
@@ -48,16 +49,16 @@ instance
   iEqBool ._==_ _     _     = False
 
   iEqChar : Eq Char
-  iEqChar ._==_ = primCharEquality
+  iEqChar ._==_ = eqChar
 
   iEqUnit : Eq ⊤
   iEqUnit ._==_ _ _ = True
 
   iEqTuple₂ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → Eq (a × b)
-  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₂ == y₂
+  iEqTuple₂ ._==_ (x₁ , y₁) (x₂ , y₂) = x₁ == x₂ && y₁ == y₂
 
   iEqTuple₃ : ⦃ Eq a ⦄ → ⦃ Eq b ⦄ → ⦃ Eq c ⦄ → Eq (a × b × c)
-  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₂ == y₂ && z₁ == z₂
+  iEqTuple₃ ._==_ (x₁ , y₁ , z₁) (x₂ , y₂ , z₂) = x₁ == x₂ && y₁ == y₂ && z₁ == z₂
 
   iEqList : ⦃ Eq a ⦄ → Eq (List a)
   iEqList {a} ._==_ = eqList
diff --git a/lib/Haskell/Prim/Ord.agda b/lib/Haskell/Prim/Ord.agda
index b6982ef8..9f2403da 100644
--- a/lib/Haskell/Prim/Ord.agda
+++ b/lib/Haskell/Prim/Ord.agda
@@ -117,7 +117,7 @@ instance
   iOrdDouble = ordFromLessThan primFloatLess
 
   iOrdChar : Ord Char
-  iOrdChar = ordFromLessThan λ x y → primCharToNat x < primCharToNat y
+  iOrdChar = ordFromLessThan λ x y → c2n x < c2n y
 
   iOrdBool : Ord Bool
   iOrdBool = ordFromCompare λ where
diff --git a/lib/Haskell/Prim/Tuple.agda b/lib/Haskell/Prim/Tuple.agda
index 71bb8624..f566e13b 100644
--- a/lib/Haskell/Prim/Tuple.agda
+++ b/lib/Haskell/Prim/Tuple.agda
@@ -34,3 +34,12 @@ second f (x , y) = x , f y
 
 _***_ : (a → b) → (c → d) → a × c → b × d
 (f *** g) (x , y) = f x , g y
+
+fst₃ : (a × b × c) → a
+fst₃ (x , _ , _) = x 
+
+snd₃ : (a × b × c) → b
+snd₃ (_ , y , _) = y
+
+thd₃ : (a × b × c) → c
+thd₃ (_ , _ , z) = z