diff --git a/ImpredicativeTypes/Church.hs b/ImpredicativeTypes/Church.hs
new file mode 100644
index 0000000..e1cb311
--- /dev/null
+++ b/ImpredicativeTypes/Church.hs
@@ -0,0 +1,350 @@
+{-# LANGUAGE RankNTypes, TypeApplications, ImpredicativeTypes #-}
+{- Church Encodings  -
+ - - - - - - - - - - - 
+ - By Risto Stevcev  -}
+
+module Church where
+import Prelude hiding (succ, pred, and, or, not, exp, div, head, tail)
+
+
+
+{- Church Logical Operators  -
+ - - - - - - - - - - - - - - -}
+
+type ChurchBool = forall a. a -> a -> a
+
+-- Church Boolean (True)
+-- λt.λf.t
+true :: ChurchBool
+true = \t -> \f -> t
+
+-- Church Boolean (False)
+-- λt.λf.f
+false :: ChurchBool
+false = \t -> \f -> f
+
+-- Church AND
+-- λa.λb.a b false
+and :: ChurchBool -> ChurchBool -> ChurchBool
+and = \a -> \b -> a b false
+
+-- Church OR
+-- λa.λb.a true b
+or :: ChurchBool -> ChurchBool -> ChurchBool
+or = \a -> \b -> a true b
+
+-- Church NOT
+-- λp.λa.λb.p b a
+not :: ChurchBool -> ChurchBool
+not = \p -> \a -> \b -> p b a
+
+-- Church XOR
+-- λa.λb.a (not b) b
+xor :: ChurchBool -> ChurchBool -> ChurchBool
+xor = \a -> \b -> a (not b) b
+
+-- Convert Church Boolean to Haskell Bool
+-- (λa.λb.λc.c a b) True False
+unchurch_bool :: (Bool -> Bool -> a) -> a
+unchurch_bool = (\a -> \b -> \c -> c a b) True False
+
+
+
+{- Church Natural Numbers (n ∈ ℕ)  -
+ - - - - - - - - - - - - - - - - - -}
+
+type Church = forall a. (a -> a) -> a -> a
+
+-- Church Numeral: 0
+-- λf.λx.x
+zero :: Church
+zero = \f -> \x -> x
+
+-- Church Numeral: 1
+-- λf.λx.f x
+one :: Church
+one = \f -> \x -> f x
+
+-- Church Numeral: 2
+-- λf.λx.f (f x)
+two :: Church
+two = \f -> \x -> f (f x)
+
+-- Church Numeral: 3
+-- λf.λx.f (f (f x))
+three :: Church
+three = \f -> \x -> f (f (f x))
+
+-- Church Numeral: n (where n ∈ ℕ)
+-- num 0 = λf.λx.x
+-- num n = λf.λx.f (num (n-1) f x)
+num :: Integer -> Church
+num 0 = \f -> \x -> x
+num n = \f -> \x -> f ((num (n-1)) f x)
+
+-- Convert Church Numeral (n ∈ ℕ) to Haskell Integer
+-- λa.a (λb.b+1) (0)
+unchurch_num :: Church -> Integer
+unchurch_num = \a -> a (\b -> b + 1) (0)
+
+
+
+{- Church Conditionals -
+ - - - - - - - - - - - -}
+
+-- Church Conditional (If/Else)
+-- λp.λa.λb.p a b
+ifelse :: ChurchBool -> a -> a -> a
+ifelse = \p -> \a -> \b -> p a b
+
+
+
+{- Church Loops -
+ - - - - - - - - -}
+
+-- Y Combinator
+-- Y = λf.(λx.f (x x)) (λx.f (x x))
+--
+-- Beta reduction of this gives,
+-- Y g = (λf.(λx.f (x x)) (λx.f (x x))) g
+--     = (λx.g (x x)) (λx.g (x x))
+--     = g((λx.g (x x)) (λx.g (x x)))
+--     = g (Y g)
+y :: (a -> a) -> a
+y g = g (y g)
+
+-- A non-recursive version of the Y combinator
+newtype Mu a = Mu (Mu a -> a)
+ynr f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
+
+
+
+{- Church Arithmetic Operators (n ∈ ℕ) -
+ - - - - - - - - - - - - - - - - - - - -}
+
+-- Church Successor
+-- λn.λf.λx.f (n f x)
+succ :: Church -> Church
+
+succ = \n -> \f -> \x -> f (n f x)
+
+-- Church Predecessor
+-- λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
+pred :: Church -> Church
+pred = \n -> \f -> \x -> n (\g -> \h -> h (g f)) (\u -> x) (\u -> u)
+
+-- Church Addition
+-- λm.λn.λf.λx.m f (n f x)
+add :: Church -> Church -> Church
+add = \m -> \n -> \f -> \x -> m f (n f x)
+
+-- Church Subtraction
+-- λm.λn. n pred m
+sub :: Church -> Church -> Church
+sub = \m -> \n -> n @Church pred m
+
+-- Church Multiplication
+-- λm.λn.λf.m (n f)
+mult :: Church -> Church -> Church
+mult = \m -> \n -> \f -> m (n f)
+
+-- Church Division (gets the floor if divides to a fraction)
+-- λd n m.ifelse (geq n m) (succ (d (sub n m) m)) zero
+div :: Church -> Church -> Church
+div = y @(Church -> Church -> Church) (\d n m -> ifelse (geq n m) (succ (d (sub n m) m)) zero)
+
+-- Church Exponentiation
+-- λm.λn.n m
+exp :: Church -> Church -> Church
+exp = \m -> \n -> n m
+
+-- Church Factorial
+-- λf n.ifelse (is_zero n) one (mult n (fac (pred n)))
+fac :: Church -> Church
+fac = y @(Church -> Church) (\f n -> ifelse (is_zero n) one (mult n $ f $ pred n))
+
+
+
+{- Church Comparison Operators -
+ - - - - - - - - - - - - - - - -}
+
+-- Church Comparison (== 0)
+-- λn.n (λx.false) true
+is_zero :: Church -> ChurchBool
+is_zero = \n -> n (\x -> false) true
+
+-- Church Comparison (<)
+-- λm.λn.and (is_zero (sub m n)) (not (is_zero (sub n m)))
+lt :: Church -> Church -> ChurchBool
+lt = \m -> \n -> and (is_zero $ sub m n) (not (is_zero $ sub n m))
+
+-- Church Comparison (<=)
+-- λm.λn.is_zero (sub m n)
+leq :: Church -> Church -> ChurchBool
+leq = \m -> \n -> is_zero (sub m n)
+
+-- Church Comparison (==)
+-- λm.λn.and (leq m n) (leq n m)
+eq :: Church -> Church -> ChurchBool
+eq = \m -> \n -> and (leq m n) (leq n m) 
+
+-- Church Comparison (>=)
+-- λm.λn.or (not (leq m n)) (eq m n)
+geq :: Church -> Church -> ChurchBool
+geq = \m -> \n -> or (not (leq m n)) (eq m n)
+
+-- Church Comparison (>)
+-- λm.λn.not (leq m n)
+gt :: Church -> Church -> ChurchBool
+gt = \m -> \n -> not (leq m n)
+
+
+
+{- Church Lists  - 
+ - - - - - - - - -}
+
+-- Church Pairs
+-- λx.λy.λz.z x y
+pair :: a1 -> a2 -> (a1 -> a2 -> a) -> a
+pair = \x -> \y -> \z -> z x y
+
+pairC :: Church -> Church -> (Church -> Church -> a) -> a
+pairC = pair @Church @Church
+
+-- Church Pairs (first item)
+-- λp.p -> (λx.λy.x)
+first :: ((a2 -> a1 -> a2) -> a) -> a
+first = \p -> p (\x -> \y -> x)
+
+firstC :: ((Church -> Church -> Church) -> Church) -> Church
+firstC = first @Church @Church @Church
+
+-- Church Pairs (second item)
+-- λp.p -> (λx.λy.y)
+second :: ((a1 -> a2 -> a2) -> a) -> a
+second = \p -> p (\x -> \y -> y)
+
+secondC :: ((Church -> Church -> Church) -> Church) -> Church
+secondC = second @Church @Church @Church
+
+-- Church Pairs (nil)
+-- pair true true
+nil :: ((a1 -> a1 -> a1) -> (a2 -> a2 -> a2) -> a) -> a
+nil = pair true true
+
+-- Church Comparison (is_nil)
+-- first (true for nil pair)
+is_nil :: ((a2 -> a1 -> a2) -> a) -> a
+is_nil = first
+
+-- Church Cons
+-- λh.λt.pair false (pair h t)
+cons :: a2 -> a3 -> ((a1 -> a1 -> a1) -> ((a2 -> a3 -> a4) -> a4) -> a) -> a
+cons = \h -> \t -> pair false (pair h t)
+
+-- Church Head
+-- λz.first (second z)
+head :: ((a3 -> a4 -> a4) -> (a2 -> a1 -> a2) -> a) -> a
+head = \z -> first (second z)
+
+-- Church Tail
+-- λz.second (second z)
+tail :: ((a3 -> a4 -> a4) -> (a1 -> a2 -> a2) -> a) -> a
+tail = \z -> second (second z)
+
+
+
+{- Church Tuples -
+ - - - - - - - - -}
+
+-- Tuples differ from lists in two ways,
+-- 1. Elements in a tuple can only be of one type (in this case, a ChurchBool or a ChurchNum)
+-- 2. Tuples are fixed in size
+data ChurchElem = ChurchNumber Church | ChurchBoolean ChurchBool
+type ChurchTuple2 = forall a. (ChurchElem -> ChurchElem -> ChurchElem) -> ChurchElem
+
+-- Church Tuple (of size 2)
+tuple2 :: ChurchElem -> ChurchElem -> ChurchTuple2
+tuple2 = \x -> \y -> \z -> z x y
+
+tuple2_first :: ChurchTuple2 -> ChurchElem
+tuple2_first = \p -> p (\x -> \y -> x)
+
+tuple2_second :: ChurchTuple2 -> ChurchElem
+tuple2_second = \p -> p (\x -> \y -> y)
+
+unchurch_bool_elem :: ChurchElem -> Bool
+unchurch_bool_elem (ChurchBoolean x) = unchurch_bool x
+
+unchurch_num_elem :: ChurchElem -> Integer
+unchurch_num_elem (ChurchNumber x) = unchurch_num x
+
+
+
+{- Church Integers (n ∈ ℤ) -
+ - - - - - - - - - - - - - -}
+
+type ChurchInteger = forall a. (Church -> Church -> Church) -> Church
+
+
+-- Convert Church Numeral (natural number) to Church Integer
+-- λx.pair x zero
+convertNZ :: Church -> ChurchInteger
+convertNZ = \x -> pairC x zero
+
+-- Church Negation
+-- λx.pair (second x) (first x)
+neg :: ChurchInteger -> ChurchInteger
+neg = \x -> pairC (secondC x) (firstC x)
+
+-- Church OneZero 
+-- (Fixes incorrect integer representations that don't have a zero in the pair. 
+-- Ex: (7, 2) == 7 - 2 == 5) 
+-- λoneZ x.ifelse (is_zero (first x)) 
+--   x (ifelse (is_zero (second x)) x (oneZ (pair (pred (first x)) (pred (second x)))))
+onezero :: ChurchInteger -> ChurchInteger
+onezero  = y @(ChurchInteger -> ChurchInteger) ( \oneZ x -> ifelse (is_zero $ firstC x) x
+                            (ifelse (is_zero $ secondC x) x
+                              (oneZ $ pairC (pred $ firstC x) (pred $ secondC x))) )
+
+-- Convert Church Integer to Haskell Integer
+-- λx.ifelse (is_zero (first x)) (-1*(unchurch_num (second x))) 
+--                               (unchurch_num (first x))
+unchurch_int :: ChurchInteger -> Integer
+unchurch_int = \x -> ifelse (is_zero (firstC x))
+                       ((-1)*(unchurch_num $ secondC x)) (unchurch_num $ firstC x)
+
+
+
+{- Church Arithmetic Operators (n ∈ ℤ) -
+ - - - - - - - - - - - - - - - - - - - -}
+
+-- Church Addition
+-- λx.λy.onezero (pair (add (first x) (first y)) (add (second x) (second y)))
+addZ :: ChurchInteger -> ChurchInteger -> ChurchInteger
+addZ = \x -> \y -> onezero (pairC (add (firstC x) (firstC y)) (add (secondC x) (secondC y)))
+
+-- Church Subtraction
+-- λx.λy.onezero (pair (add (first x) (second y)) (add (second x) (first y)))
+subZ :: ChurchInteger -> ChurchInteger -> ChurchInteger
+subZ = \x -> \y -> onezero (pairC (add (firstC x) (secondC y)) (add (secondC x) (firstC y)))
+
+-- Church Multiplication
+-- λx.λy.pair (add (mult (first x) (first y)) (mult (second x) (second y)))
+--            (add (mult (first x) (second y)) (mult (second x) (first y)))
+multZ :: ChurchInteger -> ChurchInteger -> ChurchInteger
+multZ = \x -> \y -> pairC (add (mult (firstC x) (firstC y)) (mult (secondC x) (secondC y)))
+                         (add (mult (firstC x) (secondC y)) (mult (secondC x) (firstC y)))
+
+-- Church DivNoZero
+-- (Divides only if the value is not zero)
+-- λx.λy.is_zero y zero (div x y)
+divnZ :: Church -> Church -> Church
+divnZ = \x -> \y -> is_zero y zero (div x y)
+
+-- Church Division
+-- λx.λy.pair (add (divnZ (first x) (first y)) (divnZ (second x) (second y)))
+--            (add (divnZ (first x) (second y)) (divnZ (second x) (first y)))
+divZ :: ChurchInteger -> ChurchInteger -> ChurchInteger
+divZ = \x -> \y -> pairC (add (divnZ (firstC x) (firstC y)) (divnZ (secondC x) (secondC y)))
+                        (add (divnZ (firstC x) (secondC y)) (divnZ (secondC x) (firstC y)))
diff --git a/ImpredicativeTypes/Makefile b/ImpredicativeTypes/Makefile
new file mode 100644
index 0000000..248b361
--- /dev/null
+++ b/ImpredicativeTypes/Makefile
@@ -0,0 +1,14 @@
+GHC = ghc
+
+.PHONY:
+default: TestChurch
+
+TestChurch:
+	$(GHC) TestChurch.hs
+
+.PHONY:
+all: clean default
+
+.PHONY:
+clean:
+	rm -f *.o *.hi *.*~ TestChurch
diff --git a/ImpredicativeTypes/TestChurch.hs b/ImpredicativeTypes/TestChurch.hs
new file mode 100644
index 0000000..b9d1110
--- /dev/null
+++ b/ImpredicativeTypes/TestChurch.hs
@@ -0,0 +1,522 @@
+{- Church Encoding Tests -
+ - - - - - - - - - - - - - 
+ - By Risto Stevcev      -}
+
+import Test.HUnit
+import Church
+import Prelude hiding (succ, pred, and, or, not, exp, div, head, tail)
+
+
+
+{- Test Logical Operators  -
+ - - - - - - - - - - - - - -}
+
+test_true = TestCase $ assertBool "true == True" (unchurch_bool true)
+test_true_num = TestCase $ assertEqual "true 2.5 3.2 == 2.5" 2.5 (true 2.5 3.2)
+test_false = TestCase $ assertEqual "false == False" False (unchurch_bool false)
+test_false_num = TestCase $ assertEqual "false 5 6 == 6" 6 (false 5 6)
+
+test_true_and_true = TestCase $ assertBool "true and true == true" 
+  (unchurch_bool $ and true true)
+test_true_and_false = TestCase $ assertEqual "true and false == false"
+  False (unchurch_bool $ and true false)
+test_false_and_true = TestCase $ assertEqual "false and true == false"
+  False (unchurch_bool $ and false true)
+test_false_and_false = TestCase $ assertEqual "false and false == false"
+  False (unchurch_bool $ and false false)
+
+test_true_or_true = TestCase $ assertBool "true or true == true"
+  (unchurch_bool $ or true true)
+test_true_or_false = TestCase $ assertBool "true or false == true"
+  (unchurch_bool $ or true false)
+test_false_or_true = TestCase $ assertBool "false or true == true"
+  (unchurch_bool $ or false true)
+test_false_or_false = TestCase $ assertEqual "false or false == false"
+  False (unchurch_bool $ or false false)
+
+test_not_true = TestCase $ assertEqual "not true == false"
+  False (unchurch_bool $ not true)
+test_not_false = TestCase $ assertBool "not false == true"
+  (unchurch_bool $ not false)
+test_not_false_or_true = TestCase $ assertEqual "not false or true == false"
+  False (unchurch_bool $ not $ or false true)
+test_not_true_and_false = TestCase $ assertBool "not true and false == true"
+  (unchurch_bool $ not $ and true false)
+test_not_true_xor_true = TestCase $ assertBool "not true xor true == true"
+  (unchurch_bool $ not $ xor true true)
+
+test_true_xor_true = TestCase $ assertEqual "true xor true == false"
+  False (unchurch_bool $ xor true true)
+test_true_xor_false = TestCase $ assertBool "true xor false == true"
+  (unchurch_bool $ xor true false)
+test_false_xor_true = TestCase $ assertBool "false xor true == true"
+  (unchurch_bool $ xor false true)
+test_false_xor_false = TestCase $ assertEqual "false xor false == false"
+  False (unchurch_bool $ xor false false)
+
+
+tests_logical_operators = 
+  TestList [TestLabel "test true" test_true,
+            TestLabel "test true number" test_true_num,
+            TestLabel "test false" test_false,
+            TestLabel "test false number" test_false_num,
+
+            TestLabel "test true and true" test_true_and_true,
+            TestLabel "test true and false" test_true_and_false,
+            TestLabel "test false and true" test_false_and_true,
+            TestLabel "test false and false" test_false_and_false,
+
+            TestLabel "test true or true" test_true_or_true,
+            TestLabel "test true or false" test_true_or_false,
+            TestLabel "test false or true" test_false_or_true,
+            TestLabel "test false or false" test_false_or_false,
+
+            TestLabel "test not true" test_not_true,
+            TestLabel "test not false" test_not_false,
+            TestLabel "test not false or true" test_not_false_or_true,
+            TestLabel "test not true or false" test_not_true_and_false,
+            TestLabel "test not true xor true" test_not_true_xor_true,
+
+            TestLabel "test true xor true" test_true_xor_true,
+            TestLabel "test true xor false" test_true_xor_false,
+            TestLabel "test false xor true" test_false_xor_true,
+            TestLabel "test false xor false" test_false_xor_false]
+
+
+
+{- Test Naturals (n ∈ ℕ) -
+ - - - - - - - - - - - - -}
+
+test_zero = TestCase $ assertEqual "numeral zero == 0"
+  0 (unchurch_num zero)
+test_one = TestCase $ assertEqual "numeral one == 1"
+  1 (unchurch_num one)
+test_two = TestCase $ assertEqual "numeral two == 2"
+  2 (unchurch_num two)
+test_three = TestCase $ assertEqual "numeral three == 3"
+  3 (unchurch_num three)
+test_num_12 = TestCase $ assertEqual "numeral 12 == 12"
+  12 (unchurch_num $ num 12)
+test_num_17 = TestCase $ assertEqual "numeral 17 == 17"
+  17 (unchurch_num $ num 17)
+test_num_123779 = TestCase $ assertEqual "numeral 123779 == 123779"
+  123779 (unchurch_num $ num 123779)
+
+
+tests_naturals = 
+  TestList [TestLabel "test zero" test_zero,
+            TestLabel "test one" test_one,
+            TestLabel "test two" test_two,
+            TestLabel "test three" test_three,
+            TestLabel "test numeral 12" test_num_12,
+            TestLabel "test numeral 17" test_num_17,
+            TestLabel "test numeral 123779" test_num_123779]
+
+
+
+{- Test Conditionals -
+ - - - - - - - - - - -}
+
+test_ifelse_true = TestCase $ assertEqual "ifelse true one three == 1"
+  1 (unchurch_num $ ifelse true one three)
+test_ifelse_false = TestCase $ assertEqual "ifelse false two three == 3"
+  3 (unchurch_num $ ifelse false two three) 
+
+
+tests_conditionals = 
+  TestList [TestLabel "test ifelse true" test_ifelse_true,
+            TestLabel "test ifelse false" test_ifelse_false]
+
+
+
+{- Test Arithmetic Operators for Naturals (n ∈ ℕ)  -
+ - - - - - - - - - - - - - - - - - - - - - - - - - -}
+
+test_succ_zero = TestCase $ assertEqual "succ zero == 1"
+  1 (unchurch_num $ succ zero)
+test_succ_129 = TestCase $ assertEqual "succ 129 == 130"
+  130 (unchurch_num $ succ $ num 129)
+test_pred_zero = TestCase $ assertEqual "pred zero == 0"
+  0 (unchurch_num $ pred zero)
+test_pred_one = TestCase $ assertEqual "pred one == 0"
+  0 (unchurch_num $ pred one)
+test_pred_130 = TestCase $ assertEqual "pred 130 == 129"
+  129 (unchurch_num $ pred $ num 130)
+
+test_add_zero_zero = TestCase $ assertEqual "add zero zero == 0"
+  0 (unchurch_num $ add zero zero)
+test_add_zero_one = TestCase $ assertEqual "add zero one == 1"
+  1 (unchurch_num $ add zero one)
+test_add_three_zero = TestCase $ assertEqual "add three zero == 3"
+  3 (unchurch_num $ add three zero)
+test_add_77_213 = TestCase $ assertEqual "add 77 213 == 290"
+  290 (unchurch_num $ add (num 77) (num 213))
+
+test_sub_zero_zero = TestCase $ assertEqual "sub zero zero == 0"
+  0 (unchurch_num $ sub zero zero)
+test_sub_zero_one = TestCase $ assertEqual "sub zero one == 0"
+  0 (unchurch_num $ sub zero one)
+test_sub_three_zero = TestCase $ assertEqual "sub three zero == 3"
+  3 (unchurch_num $ sub three zero)
+test_sub_213_77 = TestCase $ assertEqual "sub 213 77 == 136"
+  136 (unchurch_num $ sub (num 213) (num 77))
+
+test_mult_zero_zero = TestCase $ assertEqual "mult zero zero == 0"
+  0 (unchurch_num $ mult zero zero)
+test_mult_three_zero = TestCase $ assertEqual "mult three zero == 0"
+  0 (unchurch_num $ mult three zero)
+test_mult_13_99 = TestCase $ assertEqual "mult 13 99 == 1287"
+  1287 (unchurch_num $ mult (num 13) (num 99))
+test_mult_1_121 = TestCase $ assertEqual "mult 1 121 == 121"
+  121 (unchurch_num $ mult (num 1) (num 121))
+
+test_div_8_two = TestCase $ assertEqual "div 8 two == 4"
+  4 (unchurch_num $ div (num 8) two)
+test_div_zero_three = TestCase $ assertEqual "div zero three == 0"
+  0 (unchurch_num $ div zero three)
+test_div_99_4 = TestCase $ assertEqual "div 99 4 == 24"
+  24 (unchurch_num $ div (num 99) (num 4))
+test_div_1275_25 = TestCase $ assertEqual "div 1275 25 == 51"
+  51 (unchurch_num $ div (num 1275) (num 25))
+
+test_exp_zero_zero = TestCase $ assertEqual "exp zero zero == 1"
+  1 (unchurch_num $ exp zero zero)
+test_exp_zero_3 = TestCase $ assertEqual "exp zero 3 == 0"
+  0 (unchurch_num $ exp zero (num 3))
+test_exp_2_8 = TestCase $ assertEqual "exp 2 8 == 256"
+  256 (unchurch_num $ exp (num 2) (num 8))
+test_exp_133_1 = TestCase $ assertEqual "exp 133 1 == 133"
+  133 (unchurch_num $ exp (num 133) (num 1))
+
+test_fac_zero = TestCase $ assertEqual "fac zero = 1"
+  1 (unchurch_num $ fac zero)
+test_fac_one = TestCase $ assertEqual "fac one = 1"
+  1 (unchurch_num $ fac one)
+test_fac_three = TestCase $ assertEqual "fac three = 6"
+  6 (unchurch_num $ fac three)
+test_fac_5 = TestCase $ assertEqual "fac 5 = 120"
+  120 (unchurch_num $ fac $ num 5)
+test_fac_7 = TestCase $ assertEqual "fac 7 = 5040"
+  5040 (unchurch_num $ fac $ num 7)
+
+
+tests_arithmetic_operators_N =
+  TestList [TestLabel "test succ zero" test_succ_zero,
+            TestLabel "test succ 129" test_succ_129,
+
+            TestLabel "test pred zero" test_pred_zero,
+            TestLabel "test pred one" test_pred_one,
+            TestLabel "test pred 130" test_pred_130,
+
+            TestLabel "test add zero zero" test_add_zero_zero,
+            TestLabel "test add zero one" test_add_zero_one,
+            TestLabel "test add three zero" test_add_three_zero,
+            TestLabel "test add 77 213" test_add_77_213,
+
+            TestLabel "test sub zero zero" test_sub_zero_zero,
+            TestLabel "test sub zero one" test_sub_zero_one,
+            TestLabel "test sub three zero" test_sub_three_zero,
+            TestLabel "test sub 213 77" test_sub_213_77,
+
+            TestLabel "test mult zero zero" test_mult_zero_zero,
+            TestLabel "test mult three zero" test_mult_three_zero,
+            TestLabel "test mult 13 99" test_mult_13_99,
+            TestLabel "test mult 1 121" test_mult_1_121,
+
+            TestLabel "test div zero zero" test_div_8_two,
+            TestLabel "test div zero three" test_div_zero_three,
+            TestLabel "test div 99 4 (floor)" test_div_99_4,
+            TestLabel "test div 1275 25" test_div_1275_25,
+
+            TestLabel "test exp zero zero" test_exp_zero_zero,
+            TestLabel "test exp zero 3" test_exp_zero_3,
+            TestLabel "test exp 2 8" test_exp_2_8,
+            TestLabel "test exp 133 1" test_exp_133_1,
+
+            TestLabel "test fac zero" test_fac_zero,
+            TestLabel "test fac one" test_fac_one,
+            TestLabel "test fac three" test_fac_three,
+            TestLabel "test fac 5" test_fac_5,
+            TestLabel "test fac 7" test_fac_7] 
+
+
+
+{- Test Comparison Operators -
+ - - - - - - - - - - - - - - -}
+
+test_if_zero = TestCase $ assertBool "is_zero zero == true"
+  (unchurch_bool $ is_zero zero)
+test_if_not_zero = TestCase $ assertEqual "is_zero one == false"
+  False (unchurch_bool $ is_zero one)
+
+test_lt_0_0 = TestCase $ assertEqual "lt 0 0 == false"
+  False (unchurch_bool $ lt (num 0) (num 0)) 
+test_lt_7_7 = TestCase $ assertEqual "lt 7 7 == false"
+  False (unchurch_bool $ lt (num 7) (num 7)) 
+test_lt_14_1 = TestCase $ assertEqual "lt 14 1 == false"
+  False (unchurch_bool $ lt (num 14) (num 1)) 
+test_lt_1_2 = TestCase $ assertBool "lt 1 2 == true"
+  (unchurch_bool $ lt (num 1) (num 2)) 
+
+test_leq_0_0 = TestCase $ assertBool "leq 0 0 == true"
+  (unchurch_bool $ leq (num 0) (num 0)) 
+test_leq_7_7 = TestCase $ assertBool "leq 7 7 == true"
+  (unchurch_bool $ leq (num 7) (num 7)) 
+test_leq_14_1 = TestCase $ assertEqual "leq 14 1 == false"
+  False (unchurch_bool $ leq (num 14) (num 1)) 
+test_leq_1_2 = TestCase $ assertBool "leq 1 2 == true"
+  (unchurch_bool $ leq (num 1) (num 2)) 
+
+test_eq_0_0 = TestCase $ assertBool "eq 0 0 == true"
+  (unchurch_bool $ eq (num 0) (num 0)) 
+test_eq_7_7 = TestCase $ assertBool "eq 7 7 == true"
+  (unchurch_bool $ eq (num 7) (num 7)) 
+test_eq_14_1 = TestCase $ assertEqual "eq 14 1 == false"
+  False (unchurch_bool $ eq (num 14) (num 1)) 
+test_eq_1_2 = TestCase $ assertEqual "eq 1 2 == false"
+  False (unchurch_bool $ eq (num 1) (num 2)) 
+
+test_geq_0_0 = TestCase $ assertBool "geq 0 0 == true"
+  (unchurch_bool $ geq (num 0) (num 0)) 
+test_geq_7_7 = TestCase $ assertBool "geq 7 7 == true"
+  (unchurch_bool $ geq (num 7) (num 7)) 
+test_geq_14_1 = TestCase $ assertBool "geq 14 1 == true"
+  (unchurch_bool $ geq (num 14) (num 1)) 
+test_geq_1_2 = TestCase $ assertEqual "geq 1 2 == false"
+  False (unchurch_bool $ geq (num 1) (num 2)) 
+
+test_gt_0_0 = TestCase $ assertEqual "gt 0 0 == false"
+  False (unchurch_bool $ gt (num 0) (num 0)) 
+test_gt_7_7 = TestCase $ assertEqual "gt 7 7 == false"
+  False (unchurch_bool $ gt (num 7) (num 7)) 
+test_gt_14_1 = TestCase $ assertBool "gt 14 1 == true"
+  (unchurch_bool $ gt (num 14) (num 1)) 
+test_gt_1_2 = TestCase $ assertEqual "gt 1 2 == false"
+  False (unchurch_bool $ gt (num 1) (num 2)) 
+
+
+tests_comparison_operators =
+  TestList [TestLabel "test if zero" test_if_zero,
+            TestLabel "test if not zero" test_if_not_zero,
+
+            TestLabel "test lt 0 0" test_lt_0_0,
+            TestLabel "test lt 7 7" test_lt_7_7,
+            TestLabel "test lt 14 1" test_lt_14_1,
+            TestLabel "test lt 1 2" test_lt_1_2,
+
+            TestLabel "test leq 0 0" test_leq_0_0,
+            TestLabel "test leq 7 7" test_leq_7_7,
+            TestLabel "test leq 14 1" test_leq_14_1,
+            TestLabel "test leq 1 2" test_leq_1_2,
+
+            TestLabel "test eq 0 0" test_eq_0_0,
+            TestLabel "test eq 7 7" test_eq_7_7,
+            TestLabel "test eq 14 1" test_eq_14_1,
+            TestLabel "test eq 1 2" test_eq_1_2,
+
+            TestLabel "test geq 0 0" test_geq_0_0,
+            TestLabel "test geq 7 7" test_geq_7_7,
+            TestLabel "test geq 14 1" test_geq_14_1,
+            TestLabel "test geq 1 2" test_geq_1_2,
+
+            TestLabel "test gt 0 0" test_gt_0_0,
+            TestLabel "test gt 7 7" test_gt_7_7,
+            TestLabel "test gt 14 1" test_gt_14_1,
+            TestLabel "test gt 1 2" test_gt_1_2]
+
+
+
+{- Test Lists  -
+ - - - - - - - -}
+
+test_pair_zero_zero_first = TestCase $ assertEqual "first (pair zero zero) == 0"
+  0 (unchurch_num $ first $ pair zero zero)
+test_pair_zero_zero_second = TestCase $ assertEqual "second (pair zero zero) == 0"
+  0 (unchurch_num $ second $ pair zero zero)
+test_pair_5_12_first = TestCase $ assertEqual "first (pair 5 12) == 5"
+  5 (unchurch_num $ first $ pair (num 5) (num 12))
+test_pair_5_12_second = TestCase $ assertEqual "second (pair 5 12) == 5"
+  12 (unchurch_num $ second $ pair (num 5) (num 12))
+test_nil_pair_first = TestCase $ assertBool "first nil == true"
+  (unchurch_bool $ first nil)
+test_nil_pair_second = TestCase $ assertBool "second nil == true"
+  (unchurch_bool $ second nil)
+test_is_nil_nil = TestCase $ assertBool "is_nil nil == true"
+  (unchurch_bool $ is_nil nil)
+
+-- List construction is done using cons
+-- 133:412:7:[] == [133,412,7]
+test_list = cons (num 133) (cons (num 412) (cons (num 7) nil))
+
+test_list_node1 = TestCase $ assertEqual "node 1 (133 :412:7:[]) == 133"
+  133 (unchurch_num $ head test_list)
+test_list_node2 = TestCase $ assertEqual "node 2 (133: 412 :7:[]) == 412"
+  412 (unchurch_num $ head $ tail test_list)
+test_list_node3 = TestCase $ assertEqual "node 3 (133:412: 7 :[]) == 7"
+  7 (unchurch_num $ head $ tail $ tail test_list)
+test_list_node4 = TestCase $ assertBool "node 4 (133:412:7: []) == nil"
+  (unchurch_bool $ is_nil $ head $ tail $ tail $ tail test_list)
+
+
+tests_lists =
+  TestList [TestLabel "test pair zero zero (first)" test_pair_zero_zero_first,
+            TestLabel "test pair zero zero (second)" test_pair_zero_zero_second,
+            TestLabel "test pair 5 12 (first)" test_pair_5_12_first,
+            TestLabel "test pair 5 12 (second)" test_pair_5_12_second,
+            TestLabel "test nil pair (first)" test_nil_pair_first,
+            TestLabel "test nil pair (second)" test_nil_pair_second,
+            TestLabel "test is_nil nil" test_is_nil_nil,
+            TestLabel "test list node 1" test_list_node1,
+            TestLabel "test list node 2" test_list_node2,
+            TestLabel "test list node 3" test_list_node3,
+            TestLabel "test list node 4" test_list_node4]          
+
+
+
+{- Test Tuples -
+ - - - - - - - -}
+
+test_tuple2_zero_zero_first = TestCase $ assertEqual "first (tuple2 zero zero) == 0"
+  0 (unchurch_num_elem $ tuple2_first $ tuple2 (ChurchNumber zero) (ChurchNumber zero))
+test_tuple2_zero_zero_second = TestCase $ assertEqual "second (tuple2 zero zero) == 0"
+  0 (unchurch_num_elem $ tuple2_second $ tuple2 (ChurchNumber zero) (ChurchNumber zero))
+
+test_tuple2_5_12_first = TestCase $ assertEqual "first (tuple2 5 12) == 5"
+  5 (unchurch_num_elem $ tuple2_first $ tuple2 (ChurchNumber $ num 5) (ChurchNumber $ num 12))
+test_tuple2_5_12_second = TestCase $ assertEqual "second (tuple2 5 12) == 12"
+  12 (unchurch_num_elem $ tuple2_second $ tuple2 (ChurchNumber $ num 5) (ChurchNumber $ num 12))
+
+test_tuple2_true_false_first = TestCase $ assertBool "first (tuple2 true false) == true"
+  (unchurch_bool_elem $ tuple2_first $ tuple2 (ChurchBoolean true) (ChurchBoolean false))
+test_tuple2_true_false_second = TestCase $ assertEqual "second (tuple2 true false) == false"
+  False (unchurch_bool_elem $ tuple2_second $ tuple2 (ChurchBoolean true) (ChurchBoolean false))
+
+test_tuple2_false_true_first = TestCase $ assertEqual "first (tuple2 false true) == false"
+  False (unchurch_bool_elem $ tuple2_first $ tuple2 (ChurchBoolean false) (ChurchBoolean true))
+test_tuple2_false_true_second = TestCase $ assertBool "second (tuple2 false true) == true"
+  (unchurch_bool_elem $ tuple2_second $ tuple2 (ChurchBoolean false) (ChurchBoolean true))
+
+test_tuple2_true_true_first = TestCase $ assertBool "first (tuple2 true true) == true"
+  (unchurch_bool_elem $ tuple2_first $ tuple2 (ChurchBoolean true) (ChurchBoolean true))
+test_tuple2_true_true_second = TestCase $ assertBool "second (tuple2 true true) == true"
+  (unchurch_bool_elem $ tuple2_second $ tuple2 (ChurchBoolean true) (ChurchBoolean true))
+
+
+tests_tuples = 
+  TestList [TestLabel "first (tuple2 zero zero)" test_tuple2_zero_zero_first,
+            TestLabel "second (tuple2 zero zero)" test_tuple2_zero_zero_second,
+
+            TestLabel "first (tuple2 5 12)" test_tuple2_5_12_first,
+            TestLabel "second (tuple2 5 12)" test_tuple2_5_12_second,
+
+            TestLabel "first (tuple2 true false)" test_tuple2_true_false_first,
+            TestLabel "second (tuple2 true false)" test_tuple2_true_false_second,
+
+            TestLabel "first (tuple2 false true)" test_tuple2_false_true_first,
+            TestLabel "second (tuple2 false true)" test_tuple2_false_true_second,
+
+            TestLabel "first (tuple2 true true)" test_tuple2_true_true_first,
+            TestLabel "second (tuple2 true true)" test_tuple2_true_true_second]
+
+
+
+{- Test Integers (n ∈ ℤ) -
+ - - - - - - - - - - - - -}
+
+test_convertNZ_zero = TestCase $ assertEqual "convertNZ zero == zero" 
+  0 (unchurch_int $ convertNZ zero)
+test_convertNZ_three = TestCase $ assertEqual "convertNZ three == three"
+  3 (unchurch_int $ convertNZ three)
+test_convertNZ_45 = TestCase $ assertEqual "convertNZ 45 == 45"
+  45 (unchurch_int $ convertNZ $ num 45)
+test_neg_zero = TestCase $ assertEqual "neg 0 == 0"
+  0 (unchurch_int $ neg $ convertNZ $ zero)
+test_neg_27 = TestCase $ assertEqual "neg 27 == -27"
+  (-27) (unchurch_int $ neg $ convertNZ $ num 27)
+
+
+tests_integers = 
+  TestList [TestLabel "convertNZ zero" test_convertNZ_zero,
+            TestLabel "convertNZ three" test_convertNZ_three,
+            TestLabel "convertNZ 45" test_convertNZ_45,
+            TestLabel "neg 0" test_neg_zero,
+            TestLabel "neg 27" test_neg_27]
+
+
+
+{- Test Arithmetic Operators for Integers (n ∈ ℤ) -
+ - - - - - - - - - - - - - - -- - - - - - - - - - -}
+
+test_addZ_zero_zero = TestCase $ assertEqual "addZ zero zero == 0"
+  0 (unchurch_int $ addZ (convertNZ zero) (convertNZ zero))
+test_addZ_zero_one = TestCase $ assertEqual "addZ zero one == 1"
+  1 (unchurch_int $ addZ (convertNZ zero) (convertNZ one))
+test_addZ_three_zero = TestCase $ assertEqual "addZ three zero == 3"
+  3 (unchurch_int $ addZ (convertNZ three) (convertNZ zero))
+test_addZ_77_n213 = TestCase $ assertEqual "addZ 77 -213 == -136"
+  (-136) (unchurch_int $ addZ (convertNZ $ num 77) (neg $ convertNZ $ num 213))
+
+test_subZ_zero_zero = TestCase $ assertEqual "subZ zero zero == 0"
+  0 (unchurch_int $ subZ (convertNZ zero) (convertNZ zero))
+test_subZ_zero_one = TestCase $ assertEqual "subZ zero one == -1"
+  (-1) (unchurch_int $ subZ (convertNZ zero) (convertNZ one))
+test_subZ_n14_99 = TestCase $ assertEqual "subZ -14 99 == -113"
+  (-113) (unchurch_int $ subZ (neg $ convertNZ $ num 14) (convertNZ $ num 99))
+test_subZ_213_77 = TestCase $ assertEqual "subZ 213 77 == 136"
+  136 (unchurch_int $ subZ (convertNZ $ num 213) (convertNZ $ num 77))
+test_subZ_n3_n99 = TestCase $ assertEqual "subZ -3 -99 == 96"
+  96 (unchurch_int $ subZ (neg $ convertNZ $ num 3) (neg $ convertNZ $ num 99))
+
+test_multZ_zero_zero = TestCase $ assertEqual "multZ zero zero == 0"
+  0 (unchurch_int $ multZ (convertNZ zero) (convertNZ zero))
+test_multZ_three_zero = TestCase $ assertEqual "multZ three zero == 0"
+  0 (unchurch_int $ multZ (convertNZ three) (convertNZ zero))
+test_multZ_n3_99 = TestCase $ assertEqual "multZ -3 99 == -297"
+  (-297) (unchurch_int $ multZ (neg $ convertNZ $ num 3) (convertNZ $ num 99))
+test_multZ_n1_n121 = TestCase $ assertEqual "mult -1 -121 == 121"
+  121 (unchurch_int $ multZ (neg $ convertNZ $ num 1) (neg $ convertNZ $ num 121))
+
+test_divZ_8_two = TestCase $ assertEqual "divZ 8 two == 4"
+  4 (unchurch_int $ divZ (convertNZ $ num 8) (convertNZ two))
+test_divZ_zero_three = TestCase $ assertEqual "divZ zero three == 0"
+  0 (unchurch_int $ divZ (convertNZ zero) (convertNZ three))
+test_divZ_n99_4 = TestCase $ assertEqual "divZ -99 4 == 24"
+  (-24) (unchurch_int $ divZ (neg $ convertNZ $ num 99) (convertNZ $ num 4))
+test_divZ_n1275_n25 = TestCase $ assertEqual "divZ -1275 -25 == 51"
+  51 (unchurch_int $ divZ (neg $ convertNZ $ num 1275) (neg $ convertNZ $ num 25))
+
+
+tests_arithmetic_operators_Z =
+  TestList [TestLabel "addZ zero zero" test_addZ_zero_zero,
+            TestLabel "addZ zero one" test_addZ_zero_one,
+            TestLabel "addZ three zero" test_addZ_three_zero,
+            TestLabel "addZ 77 -213" test_addZ_77_n213,
+
+            TestLabel "subZ zero zero" test_subZ_zero_zero,
+            TestLabel "subZ zero one" test_subZ_zero_one,
+            TestLabel "subZ -14 99" test_subZ_n14_99,
+            TestLabel "subZ 213 77" test_subZ_213_77,
+            TestLabel "subZ -3 -99" test_subZ_n3_n99,
+
+            TestLabel "multZ zero zero" test_multZ_zero_zero,
+            TestLabel "multZ three zero" test_multZ_three_zero,
+            TestLabel "multZ -3 99" test_multZ_n3_99,
+            TestLabel "multZ -1 -121" test_multZ_n1_n121,
+
+            TestLabel "divZ 8 two" test_divZ_8_two,
+            TestLabel "divZ zero three" test_divZ_zero_three,
+            TestLabel "divZ -99 4" test_divZ_n99_4,
+            TestLabel "divZ -1275 -25" test_divZ_n1275_n25]
+
+
+
+main = do
+  runTestTT tests_logical_operators
+  runTestTT tests_naturals
+  runTestTT tests_conditionals
+  runTestTT tests_arithmetic_operators_N
+  runTestTT tests_comparison_operators
+  runTestTT tests_lists
+  runTestTT tests_tuples
+  runTestTT tests_integers
+  runTestTT tests_arithmetic_operators_Z
diff --git a/README.md b/README.md
index 483cd97..a94d162 100644
--- a/README.md
+++ b/README.md
@@ -23,6 +23,11 @@ So far I've translated church booleans, church boolean operators, church conditi
 I can still translate the leftover operators for integers, as well as real, rational, imaginary and complex numbers.
 
 
+## ImpredicativeTypes
+
+This avoids having to roll and unroll Church numerals, but comes at the expense of type inference in many of the places they're used, since Haskell doesn't currently support inferring impredicative types.
+
+
 ## Credits
 
 I'd like to give credit where it's due: