diff --git a/src/Quox/Syntax/Term/Base.idr b/src/Quox/Syntax/Term/Base.idr
index 22552f6..a377339 100644
--- a/src/Quox/Syntax/Term/Base.idr
+++ b/src/Quox/Syntax/Term/Base.idr
@@ -89,6 +89,10 @@ mutual
 %name ScopeTerm body
 %name DScopeTerm body
 
+public export %inline
+Arr : Qty -> Term d n -> Term d n -> Term d n
+Arr pi a b = Pi {qtm = pi, qty = zero, x = "_", arg = a, res = TUnused b}
+
 ||| same as `F` but as a term
 public export %inline
 FT : Name -> Term d n
diff --git a/tests/TAP.idr b/tests/TAP.idr
index 0367875..17acddf 100644
--- a/tests/TAP.idr
+++ b/tests/TAP.idr
@@ -45,21 +45,36 @@ All ToInfo es => ToInfo (OneOf es) where
 
 export %inline ToInfo () where toInfo () = []
 
+export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
+
+
 export
 data Test = One TestBase | Group String (List Test)
 
 
+private %inline
+success : ToInfo a => a -> IO Result
+success = pure . Tried True . toInfo
+
+private %inline
+failure : ToInfo e => e -> IO Result
+failure = pure . Tried False . toInfo
+
+private %inline
+lazyToIO : Lazy a -> IO a
+lazyToIO val = primIO $ \w => MkIORes (force val) w
+
 export
 testIO : (All ToInfo es, ToInfo a) => String -> ErrorT es IO a -> Test
 testIO label act = One $ MakeTest label $ do
   case !(runErrorT act) of
-       Left  err => pure $ Tried False $ toInfo err
-       Right val => pure $ Tried True  $ toInfo val
+       Right val => success val
+       Left  err => failure err
 
 export %inline
 test : (All ToInfo es, ToInfo a) => String -> Lazy (Error es a) -> Test
 test label val =
-  testIO label $ MkErrorT $ primIO $ \w => MkIORes (runError val) w
+  testIO label $ MkErrorT $ lazyToIO $ runError val
 
 export %inline
 todoWith : String -> String -> Test
@@ -77,11 +92,24 @@ export %inline
 skip : String -> Test
 skip label = skipWith label ""
 
+export
+testThrows : Show a => String -> Lazy (Error es a) -> Test
+testThrows label act = One $ MakeTest label $ do
+  case runError !(lazyToIO act) of
+       Left  err => success ()
+       Right val => failure [("success", val)]
+
 infix 0 :-
 export %inline
 (:-) : String -> List Test -> Test
 (:-) = Group
 
+export %inline
+bailOut : Test
+bailOut = One $ MakeTest "bail out" $ do
+  putStrLn "Bail out!"
+  exitFailure
+
 
 
 export %inline
diff --git a/tests/Tests.idr b/tests/Tests.idr
index b095b76..393c11a 100644
--- a/tests/Tests.idr
+++ b/tests/Tests.idr
@@ -1,7 +1,11 @@
 module Tests
 
+import Tests.Equal
+
 import TAP
 
-export main : IO ()
-main = run
-  [todo "write tests"]
+import System
+
+export main : IO Int
+main = exitWith =<< run
+  [Equal.tests]
diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr
new file mode 100644
index 0000000..4605607
--- /dev/null
+++ b/tests/Tests/Equal.idr
@@ -0,0 +1,101 @@
+module Tests.Equal
+
+import Quox.Equal
+import Quox.Pretty
+import TAP
+
+export
+ToInfo Equal.Error where
+  toInfo (ClashT mode s t) =
+    [("clash",  "term"),
+     ("mode",   show mode),
+     ("left",  prettyStr True s),
+     ("right", prettyStr True t)]
+  toInfo (ClashU mode k l) =
+    [("clash",  "universe"),
+     ("mode",   show mode),
+     ("left",  prettyStr True k),
+     ("right", prettyStr True l)]
+  toInfo (ClashQ pi rh) =
+    [("clash",  "quantity"),
+     ("left",  prettyStr True pi),
+     ("right", prettyStr True rh)]
+
+
+M = Error [Equal.Error]
+
+testEq : String -> Lazy (M ()) -> Test
+testEq = test
+
+testNeq : String -> Lazy (M ()) -> Test
+testNeq = testThrows
+
+
+subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+subT = Quox.Equal.subT
+%hide Quox.Equal.subT
+
+equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+equalT = Quox.Equal.equalT
+%hide Quox.Equal.equalT
+
+subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+subE = Quox.Equal.subE
+%hide Quox.Equal.subE
+
+equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+equalE = Quox.Equal.equalE
+%hide Quox.Equal.equalE
+
+
+export
+tests : Test
+tests = "equality & subtyping" :- [
+    "universes" :- [
+        testEq "Type 0 == Type 0" $
+          equalT (TYPE (U 0)) (TYPE (U 0)),
+        testNeq "Type 0 =/= Type 1" $
+          equalT (TYPE (U 0)) (TYPE (U 1)),
+        testNeq "Type 1 =/= Type 0" $
+          equalT (TYPE (U 1)) (TYPE (U 0)),
+        testEq "Type 0 <: Type 0" $
+          subT (TYPE (U 0)) (TYPE (U 0)),
+        testEq "Type 0 <: Type 1" $
+          subT (TYPE (U 0)) (TYPE (U 1)),
+        testNeq "Type 1 </: Type 0" $
+          subT (TYPE (U 1)) (TYPE (U 0))
+      ],
+    todo "pi",
+    todo "lambda",
+    todo "term closure",
+    todo "term d-closure",
+
+    "free var" :- [
+        testEq "A == A" $
+          equalE (F "A") (F "A"),
+        testNeq "A =/= B" $
+          equalE (F "A") (F "B"),
+        testEq "A <: A" $
+          subE (F "A") (F "A"),
+        testNeq "A </: B" $
+          subE (F "A") (F "B")
+      ],
+    todo "bound var",
+    "application" :-
+      let a    = F "a"; a' = E a
+          A    = FT "A"
+          λxx  = Lam "x" (TUsed (BVT 0))
+          A_A  = Arr one A A
+          λxx' = λxx :# A_A
+      in [
+        testEq "(λx. x : A -> A) a == ((a : A) : A)  (β)" $
+          equalE (λxx' :@ a') (E (a' :# A) :# A),
+        testEq "(λx. x : _) a == a  (βυ)" $
+          equalE (λxx' :@ a') a
+      ],
+    todo "annotation",
+    todo "elim closure",
+    todo "elim d-closure",
+
+    todo "clashes"
+  ]