diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,28 @@
+Copyright (c) Erik Hesselink 2009
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ``AS IS'' AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
+SUCH DAMAGE.
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,5 @@
+#! /usr/bin/env runhaskell
+
+>import Distribution.Simple
+>main = defaultMain
+
diff --git a/src/Data/Type/Equality.hs b/src/Data/Type/Equality.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Type/Equality.hs
@@ -0,0 +1,103 @@
+{-# LANGUAGE TypeOperators
+           , GADTs
+           , CPP
+           #-}
+-------------------------------------------------------------------------------
+-- |
+-- Module      : Data.Type.Equality
+-- Copyright   : (c) 2009, Erik Hesselink
+-- License     : BSD3
+--
+-- Maintainer  : Erik Hesselink <hesselink@gmail.com>
+-- Stability   : Experimental
+--
+-- Type equality, coercion/cast and other operations.
+--
+-------------------------------------------------------------------------------
+module Data.Type.Equality 
+  ( (:=:)(Refl)
+  , sym
+  , trans
+  , subst
+  
+  , cong
+  , cong2
+  , cong3
+  
+  , coerce
+  
+  , EqT(eqT)
+  , EqT2(eqT2)
+  , EqT3(eqT3)
+  ) where
+
+import Prelude
+#if __GLASGOW_HASKELL__ >= 609
+               hiding (id, (.))
+import Control.Category
+#endif
+
+-- | Type equality. A value of @a :=: b@ is a proof that types @a@ and
+-- @b@ are equal. By pattern matching on @Refl@ this fact is
+-- introduced to the type checker.
+data a :=: b where
+  Refl :: a :=: a
+
+infix 4 :=:
+
+#if __GLASGOW_HASKELL__ >= 609
+instance Category (:=:) where
+  id = Refl
+  Refl . Refl = Refl
+#endif
+
+-- | Equality is symmetric.
+sym :: a :=: b -> b :=: a
+sym Refl = Refl
+
+-- | Equality is transitive. This is the same as (>>>) from the 'Category'
+-- instance, but also works in GHC 6.8.
+trans :: a :=: b -> b :=: c -> a :=: c
+trans Refl Refl = Refl
+
+-- | Equality is substitutive. This is defined directly, but can also
+-- be defined as 'coerce' '.' 'cong'.
+subst :: a :=: b -> f a -> f b
+subst Refl = id
+
+-- | Equality is congruential.
+cong :: a :=: b -> f a :=: f b
+cong Refl = Refl
+
+-- | Congruence for type constructors with two parameters.
+cong2 :: a :=: b -> c :=: d -> f a c :=: f b d
+cong2 Refl Refl = Refl
+
+-- | Congruence for type constructors with three parameters.
+cong3 :: a :=: a'-> b :=: b' -> c :=: c' -> f a b c :=: f a' b' c'
+cong3 Refl Refl Refl = Refl
+
+-- | Coerce a type to another using an equality proof.
+coerce :: a :=: b -> a -> b
+coerce Refl = id
+
+-- | A type class for constructing equality proofs. This is as close
+-- as we can get to decidable equality on types. Note that @f@ must be
+-- a GADT to be able to define 'eqT'.
+class EqT f where
+  eqT :: f a -> f b -> Maybe (a :=: b)
+
+-- | A type class for constructing equality proofs for type
+-- constructor with two parameters. Can be useful when representing
+-- relations between types.
+class EqT2 f where
+  eqT2 :: f a b -> f c d -> (Maybe (a :=: c), Maybe (b :=: d))
+
+-- | A type class for constructing equality proofs for type
+-- constructor with three parameters. If you find a use for this, let
+-- me know.
+class EqT3 f where
+  eqT3 :: f a b c -> f a' b' c' -> (Maybe (a :=: a'), Maybe (b :=: b'), Maybe (c :=: c'))
+
+instance EqT ((:=:) a) where
+  eqT Refl Refl = Just Refl
diff --git a/type-equality.cabal b/type-equality.cabal
new file mode 100644
--- /dev/null
+++ b/type-equality.cabal
@@ -0,0 +1,26 @@
+Name:             type-equality
+Version:          0.1.0
+Synopsis:         Type equality, coercion/cast and other operations.
+Description:      In the presence of GADTs, sometimes a proof is
+                  needed that two types are equal. This package
+                  contains an equality type for this purpose, plus its
+                  properties (reflexive, symmetric, transitive) and
+                  some useful operations (substitution, congruence,
+                  coercion/cast). It also contains a type class for
+                  producing equality proofs, providing some form of
+                  decidable equality on types.
+Category:         Data
+Cabal-Version:    >= 1.2.1
+Author:           Erik Hesselink, Martijn van Steenbergen
+License:          BSD3
+License-File:     LICENSE
+Maintainer:       hesselink@gmail.com
+Homepage:         http://github.com/hesselink/type-equality/
+Stability:        experimental
+Build-Type:       Simple
+Build-Depends:    base >= 3 && < 5
+Tested-With:      GHC == 6.8.2, GHC == 6.10.3
+
+HS-Source-Dirs:   src
+GHC-Options:      -Wall
+Exposed-Modules:  Data.Type.Equality