diff --git a/Data/Eq/Type.hs b/Data/Eq/Type.hs
--- a/Data/Eq/Type.hs
+++ b/Data/Eq/Type.hs
@@ -1,26 +1,21 @@
-{-# LANGUAGE Rank2Types, TypeOperators #-}
+{-# LANGUAGE GADTs, TypeOperators #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Eq.Type
--- Copyright   :  (C) 2011 Edward Kmett
+-- Copyright   :  (C) 2011 Edward Kmett, Dan Doel
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
 -- Stability   :  provisional
--- Portability :  rank2 types, type operators, type families (optional)
---
--- Leibnizian equality. Injectivity in the presence of type families 
--- is provided by a generalization of a trick by Oleg Kiselyv posted here:
+-- Portability :  GADTs, type operators
 --
--- <http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html>
 ----------------------------------------------------------------------------
 
 module Data.Eq.Type
   ( 
-  -- * Leibnizian equality
+  -- * Equality
     (:=)(..)
   -- * Equality as an equivalence relation
-  , refl
   , trans
   , symm 
   , coerce
@@ -28,86 +23,60 @@
   , lift
   , lift2, lift2'
   , lift3, lift3'
-#ifdef LANGUAGE_TypeFamilies
   -- * Lowering equality
   , lower
   , lower2
   , lower3
-#endif
   ) where
 
 import Prelude ()
 import Control.Category 
+import Data.Semigroupoid
 
 infixl 4 :=
 
--- | Leibnizian equality states that two things are equal if you can 
--- substite one for the other in all contexts
-data a := b = Refl { subst :: forall c. c a -> c b } 
-
--- | Equality is reflexive
-refl :: a := a
-refl = Refl id
+data a := b where
+  Refl :: a := a
 
-newtype Coerce a = Coerce { uncoerce :: a } 
--- | If two things are equal you can convert one to the other
-coerce :: a := b -> a -> b
-coerce f = uncoerce . subst f . Coerce
+subst :: (a := b) -> p a -> p b
+subst Refl pa = pa
 
--- | Equality forms a category
-instance Category (:=) where
-  id = Refl id
-  (.) = subst
+trans :: (a := b) -> (b := c) -> (a := c)
+trans Refl Refl = Refl
 
--- | Equality is transitive
-trans :: a := b -> b := c -> a := c
-trans = (>>>)
+symm :: (a := b) -> b := a
+symm Refl = Refl
 
-newtype Symm p a b = Symm { unsymm :: p b a } 
--- | Equality is symmetric
-symm :: (a := b) -> (b := a)
-symm a = unsymm (subst a (Symm id))
+coerce :: (a := b) -> a -> b
+coerce Refl x = x
 
-newtype Lift f a b = Lift { unlift :: f a := f b } 
--- | You can lift equality into any type constructor
-lift :: a := b -> f a := f b
-lift a = unlift (subst a (Lift id))
+lift :: a := b -> (f a := f b)
+lift Refl = Refl
 
-newtype Lift2 f c a b = Lift2 { unlift2 :: f a c := f b c }  
--- | ... in any position
-lift2 :: a := b -> f a c := f b c
-lift2 a = unlift2 (subst a (Lift2 id))
+lift2 :: a := b -> (f a c := f b c)
+lift2 Refl = Refl
 
-lift2' :: a := b -> c := d -> f a c := f b d
-lift2' ab cd = lift2 ab . lift cd
+lift2' :: (a := b) -> (c := d) -> f a c := f b d
+lift2' Refl Refl = Refl
 
-newtype Lift3 f c d a b = Lift3 { unlift3 :: f a c d := f b c d } 
-lift3 :: a := b -> f a c d := f b c d
-lift3 a = unlift3 (subst a (Lift3 id))
+lift3 :: (a := b) -> (f a c d := f b c d)
+lift3 Refl = Refl
 
-lift3' :: a := b -> c := d -> e := f -> g a c e := g b d f
-lift3' ab cd ef = lift3 ab . lift2 cd . lift ef
+lift3' :: (a := b) -> (c := d) -> (e := f) -> (g a c e := g b d f)
+lift3' Refl Refl Refl = Refl
 
-#ifdef LANGUAGE_TypeFamilies
+lower :: (f a := f b) -> (a := b)
+lower Refl = Refl
 
-type family Inj f :: *
-type instance Inj (f a) = a
-newtype Lower a b = Lower { unlower :: Inj a := Inj b }
--- | Type constructors are injective, so you can lower equality through any type constructor
-lower :: f a := f b -> a := b
-lower eq = unlower (subst eq (Lower id :: Lower (f a) (f a)))
+lower2 :: (f a c := f b c) -> (a := b)
+lower2 Refl = Refl
 
-type family Inj2 f :: *
-type instance Inj2 (f a b) = a
-newtype Lower2 a b = Lower2 { unlower2 :: Inj2 a := Inj2 b }
--- | ... in any position
-lower2 :: f a c := f b c -> a := b
-lower2 eq = unlower2 (subst eq (Lower2 id :: Lower2 (f a c) (f a c)))
+lower3 :: (f a c d := f b c d) -> (a := b)
+lower3 Refl = Refl
 
-type family Inj3 f :: *
-type instance Inj3 (f a b c) = a
-newtype Lower3 a b = Lower3 { unlower3 :: Inj3 a := Inj3 b }
-lower3 :: f a c d := f b c d -> a := b
-lower3 eq = unlower3 (subst eq (Lower3 id :: Lower3 (f a c d) (f a c d)))
+instance Category (:=) where
+  id = Refl
+  (.) = subst
 
-#endif
+instance Semigroupoid (:=) where
+  o = subst
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2010-2011 Edward Kmett
+Copyright 2010-2011 Edward Kmett, Dan Doel
 
 All rights reserved.
 
diff --git a/eq.cabal b/eq.cabal
--- a/eq.cabal
+++ b/eq.cabal
@@ -1,6 +1,6 @@
 name:          eq
 category:      Type System
-version:       0.1.3
+version:       0.2.0
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -8,27 +8,21 @@
 maintainer:    Edward A. Kmett <ekmett@gmail.com>
 stability:     provisional
 homepage:      http://github.com/ekmett/eq/
-copyright:     Copyright (C) 2010-2011 Edward A. Kmett
-synopsis:      Leibnizian equality
-description:   Leibnizian equality
+copyright:     Copyright (C) 2011 Edward A. Kmett, Dan Doel
+synopsis:      GADT-based type-level equality
+description:   GADT-based type-level equality
 build-type:    Simple
 
 source-repository head
   type: git
   location: git://github.com/ekmett/eq.git
 
-flag TypeFamilies
-  default: True
-
 library
   build-depends: 
-    base >= 4 && < 5
-
-  extensions: CPP
+    base >= 4 && < 5,
+    semigroupoids >= 1.1.1 && < 1.2.0
 
-  if flag(TypeFamilies)
-    cpp-options: -DLANGUAGE_TypeFamilies
-    extensions: TypeFamilies
+  extensions: GADTs, TypeOperators
 
   exposed-modules:
     Data.Eq.Type