diff --git a/.ghci b/.ghci
new file mode 100644
--- /dev/null
+++ b/.ghci
@@ -0,0 +1,1 @@
+:set -isrc -idist/build/autogen -optP-include -optPdist/build/autogen/cabal_macros.h
diff --git a/.gitignore b/.gitignore
new file mode 100644
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,13 @@
+dist
+docs
+wiki
+TAGS
+tags
+wip
+.DS_Store
+.*.swp
+.*.swo
+*.o
+*.hi
+*~
+*#
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -1,1 +1,8 @@
 language: haskell
+notifications:
+  irc:
+    channels:
+      - "irc.freenode.org#haskell-lens"
+    skip_join: true
+    template:
+      - "\x0313eq\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
diff --git a/.vim.custom b/.vim.custom
new file mode 100644
--- /dev/null
+++ b/.vim.custom
@@ -0,0 +1,31 @@
+" Add the following to your .vimrc to automatically load this on startup
+
+" if filereadable(".vim.custom")
+"     so .vim.custom
+" endif
+
+function StripTrailingWhitespace()
+  let myline=line(".")
+  let mycolumn = col(".")
+  silent %s/  *$//
+  call cursor(myline, mycolumn)
+endfunction
+
+" enable syntax highlighting
+syntax on
+
+" search for the tags file anywhere between here and /
+set tags=TAGS;/
+
+" highlight tabs and trailing spaces
+set listchars=tab:‗‗,trail:‗
+set list
+
+" f2 runs hasktags
+map <F2> :exec ":!hasktags -x -c --ignore src"<CR><CR>
+
+" strip trailing whitespace before saving
+" au BufWritePre *.hs,*.markdown silent! cal StripTrailingWhitespace()
+
+" rebuild hasktags after saving
+au BufWritePost *.hs silent! :exec ":!hasktags -x -c --ignore src"
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.markdown
@@ -0,0 +1,9 @@
+3.1
+---
+* Disabled observing injectivity through `TypeFamilies` for GHC >= 7.6
+
+3.0.1
+-----
+* Updated build system
+* Removed my personal intra-package dependency upper bounds
+* Added `README` and `CHANGELOG`
diff --git a/Data/Eq/Type.hs b/Data/Eq/Type.hs
deleted file mode 100644
--- a/Data/Eq/Type.hs
+++ /dev/null
@@ -1,120 +0,0 @@
-{-# LANGUAGE CPP, Rank2Types, TypeOperators #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Data.Eq.Type
--- Copyright   :  (C) 2011 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  provisional
--- 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
-  ( 
-  -- * Leibnizian equality
-    (:=)(..)
-  -- * Equality as an equivalence relation
-  , refl
-  , trans
-  , symm 
-  , coerce
-  -- * Lifting equality
-  , lift
-  , lift2, lift2'
-  , lift3, lift3'
-#ifdef LANGUAGE_TypeFamilies
-  -- * Lowering equality
-  , lower
-  , lower2
-  , lower3
-#endif
-  ) where
-
-import Prelude ()
-import Control.Category 
-import Data.Semigroupoid
-import Data.Groupoid
-
-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
-
-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
-
--- | Equality forms a category
-instance Category (:=) where
-  id = Refl id
-  (.) = subst
-
-instance Semigroupoid (:=) where
-  o = subst
-
-instance Groupoid (:=) where
-  inv = symm
-
--- | Equality is transitive
-trans :: a := b -> b := c -> a := c
-trans = (>>>)
-
-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))
-
-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))
-
-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 -> c := d -> f a c := f b d
-lift2' ab cd = lift2 ab . lift cd
-
-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 -> c := d -> e := f -> g a c e := g b d f
-lift3' ab cd ef = lift3 ab . lift2 cd . lift ef
-
-#ifdef LANGUAGE_TypeFamilies
-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)))
-
-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
+Copyright 2010-2013 Edward Kmett
 
 All rights reserved.
 
diff --git a/README.markdown b/README.markdown
new file mode 100644
--- /dev/null
+++ b/README.markdown
@@ -0,0 +1,18 @@
+eq
+==
+
+[![Build Status](https://secure.travis-ci.org/ekmett/eq.png?branch=master)](http://travis-ci.org/ekmett/eq)
+
+This package provides a data type that witnesses equality between two types using Leibnizian equality.
+
+It includes a [refinement to the notion of Leibnizian equality by Oleg Kiselyov](http://www.haskell.org/pipermail/haskell-cafe/2010-May/077177.html) 
+that permits it to refine equality using the injectively of type constructors via type families.
+
+Contact Information
+-------------------
+
+Contributions and bug reports are welcome!
+
+Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.
+
+-Edward Kmett
diff --git a/eq.cabal b/eq.cabal
--- a/eq.cabal
+++ b/eq.cabal
@@ -1,6 +1,6 @@
 name:          eq
 category:      Type System
-version:       3.0
+version:       3.1
 license:       BSD3
 cabal-version: >= 1.6
 license-file:  LICENSE
@@ -9,12 +9,18 @@
 stability:     provisional
 homepage:      http://github.com/ekmett/eq/
 bug-reports:   http://github.com/ekmett/eq/issues
-copyright:     Copyright (C) 2011 Edward A. Kmett
+copyright:     Copyright (C) 2011-2013 Edward A. Kmett
 synopsis:      Leibnizian equality
 description:   Leibnizian equality
 build-type:    Simple
 
-extra-source-files: .travis.yml
+extra-source-files:
+  .ghci
+  .gitignore
+  .vim.custom
+  .travis.yml
+  CHANGELOG.markdown
+  README.markdown
 
 source-repository head
   type: git
@@ -28,14 +34,15 @@
 
   build-depends:
     base          == 4.*,
-    semigroupoids == 3.0.*,
-    groupoids     == 3.0.*
+    semigroupoids >= 3,
+    groupoids     >= 3
 
   exposed-modules:
     Data.Eq.Type
 
-  if impl(ghc >= 7.0)
+  if impl(ghc >= 7.0) && impl(ghc < 7.6)
     extensions: TypeFamilies
     cpp-options: -DLANGUAGE_TypeFamilies
 
   ghc-options: -Wall
+  hs-source-dirs: src
diff --git a/src/Data/Eq/Type.hs b/src/Data/Eq/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Eq/Type.hs
@@ -0,0 +1,120 @@
+{-# LANGUAGE CPP, Rank2Types, TypeOperators #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Eq.Type
+-- Copyright   :  (C) 2011 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- 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
+  ( 
+  -- * Leibnizian equality
+    (:=)(..)
+  -- * Equality as an equivalence relation
+  , refl
+  , trans
+  , symm 
+  , coerce
+  -- * Lifting equality
+  , lift
+  , lift2, lift2'
+  , lift3, lift3'
+#ifdef LANGUAGE_TypeFamilies
+  -- * Lowering equality
+  , lower
+  , lower2
+  , lower3
+#endif
+  ) where
+
+import Prelude ()
+import Control.Category 
+import Data.Semigroupoid
+import Data.Groupoid
+
+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
+
+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
+
+-- | Equality forms a category
+instance Category (:=) where
+  id = Refl id
+  (.) = subst
+
+instance Semigroupoid (:=) where
+  o = subst
+
+instance Groupoid (:=) where
+  inv = symm
+
+-- | Equality is transitive
+trans :: a := b -> b := c -> a := c
+trans = (>>>)
+
+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))
+
+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))
+
+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 -> c := d -> f a c := f b d
+lift2' ab cd = lift2 ab . lift cd
+
+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 -> c := d -> e := f -> g a c e := g b d f
+lift3' ab cd ef = lift3 ab . lift2 cd . lift ef
+
+#ifdef LANGUAGE_TypeFamilies
+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)))
+
+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