diff --git a/Data/Eq/Type.hs b/Data/Eq/Type.hs
--- a/Data/Eq/Type.hs
+++ b/Data/Eq/Type.hs
@@ -1,21 +1,26 @@
-{-# LANGUAGE GADTs, TypeOperators #-}
+{-# LANGUAGE CPP, Rank2Types, TypeOperators #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Eq.Type
--- Copyright   :  (C) 2011 Edward Kmett, Dan Doel
+-- Copyright   :  (C) 2011 Edward Kmett
 -- License     :  BSD-style (see the file LICENSE)
 --
 -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
 -- Stability   :  provisional
--- Portability :  GADTs, type operators
+-- Portability :  rank2 types, type operators, (optional) type families
 --
+-- Leibnizian equality. Injectivity in the presence of type families 
+-- is provided by a generalization of a trick by Oleg Kiselyv posted here:
+--
+-- <http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html>
 ----------------------------------------------------------------------------
 
 module Data.Eq.Type
   ( 
-  -- * Equality
+  -- * Leibnizian equality
     (:=)(..)
   -- * Equality as an equivalence relation
+  , refl
   , trans
   , symm 
   , coerce
@@ -23,10 +28,12 @@
   , lift
   , lift2, lift2'
   , lift3, lift3'
+#ifdef LANGUAGE_TypeFamilies
   -- * Lowering equality
   , lower
   , lower2
   , lower3
+#endif
   ) where
 
 import Prelude ()
@@ -35,48 +42,76 @@
 
 infixl 4 :=
 
-data a := b where
-  Refl :: a := a
+-- | 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 } 
 
-subst :: (a := b) -> p a -> p b
-subst Refl pa = pa
+-- | Equality is reflexive
+refl :: a := a
+refl = Refl id
 
-trans :: (a := b) -> (b := c) -> (a := c)
-trans Refl Refl = Refl
+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
 
-symm :: (a := b) -> b := a
-symm Refl = Refl
+-- | Equality forms a category
+instance Category (:=) where
+  id = Refl id
+  (.) = subst
 
-coerce :: (a := b) -> a -> b
-coerce Refl x = x
+instance Semigroupoid (:=) where
+  o = subst
 
-lift :: a := b -> (f a := f b)
-lift Refl = Refl
+-- | Equality is transitive
+trans :: a := b -> b := c -> a := c
+trans = (>>>)
 
-lift2 :: a := b -> (f a c := f b c)
-lift2 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))
 
-lift2' :: (a := b) -> (c := d) -> f a c := f b d
-lift2' Refl Refl = Refl
+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))
 
-lift3 :: (a := b) -> (f a c d := f b c d)
-lift3 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))
 
-lift3' :: (a := b) -> (c := d) -> (e := f) -> (g a c e := g b d f)
-lift3' Refl Refl Refl = Refl
+lift2' :: a := b -> c := d -> f a c := f b d
+lift2' ab cd = lift2 ab . lift cd
 
-lower :: (f a := f b) -> (a := b)
-lower 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))
 
-lower2 :: (f a c := f b c) -> (a := b)
-lower2 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
 
-lower3 :: (f a c d := f b c d) -> (a := b)
-lower3 Refl = Refl
+#ifdef LANGUAGE_TypeFamilies
 
-instance Category (:=) where
-  id = Refl
-  (.) = subst
+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)))
 
-instance Semigroupoid (:=) where
-  o = subst
+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)))
+
+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)))
+
+#endif
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright 2010-2011 Edward Kmett, Dan Doel
+Copyright 2010-2011 Edward Kmett
 
 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.2.0
+version:       0.3.0
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -8,9 +8,9 @@
 maintainer:    Edward A. Kmett <ekmett@gmail.com>
 stability:     provisional
 homepage:      http://github.com/ekmett/eq/
-copyright:     Copyright (C) 2011 Edward A. Kmett, Dan Doel
-synopsis:      GADT-based type-level equality
-description:   GADT-based type-level equality
+copyright:     Copyright (C) 2011 Edward A. Kmett
+synopsis:      Leibnizian equality
+description:   Leibnizian equality
 build-type:    Simple
 
 source-repository head
@@ -22,7 +22,7 @@
     base >= 4 && < 5,
     semigroupoids >= 1.1.1 && < 1.2.0
 
-  extensions: GADTs, TypeOperators
+  extensions: TypeOperators
 
   exposed-modules:
     Data.Eq.Type