diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright 2012 Gábor Lehel
+
+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 AUTHORS ``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.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Type/Eq.hs b/Type/Eq.hs
new file mode 100644
--- /dev/null
+++ b/Type/Eq.hs
@@ -0,0 +1,173 @@
+{-# LANGUAGE GADTs, TypeFamilies, Rank2Types, TypeOperators, FlexibleInstances, FlexibleContexts, CPP #-}
+
+#include "macros.h"
+
+LANGUAGE_POLYKINDS
+LANGUAGE_TRUSTWORTHY
+
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+
+-- | Types and combinators for storing and manipulating type equality evidence.
+-- 
+--   This module is kind-polymorphic if @PolyKinds@ are available (GHC 7.6+).
+--
+--   Notable combinators missing from this module include @applyEq@, @constructorEq@, and @sameOuterEq@.
+-- 
+--   See also @"Type.Eq.Higher"@ and @"Type.Eq.Poly"@.
+
+module Type.Eq where
+
+import Control.Category         (Category(..))
+import Control.Applicative      (Applicative) -- for haddock
+#ifdef HAVE_DEPENDENCIES
+--import Control.Category.Product (Tensor(..))
+import Data.Groupoid            (Groupoid(..))
+import Data.Semigroupoid        (Semigroupoid(..))
+#endif
+import Data.Typeable     hiding (cast)
+import Type.Eq.Unsafe
+import Prelude           hiding ((.))
+import Unsafe.Coerce
+
+-- * Full equality
+
+-- | Evidence that type @a@ is the same as type @b@.
+-- 
+--   The @'Functor'@, @'Applicative'@, and @'Monad'@ instances of @Maybe@
+--   are extremely useful for working with values of type @Maybe (a :~: b)@.
+data a :~: b where
+    Eq :: (a ~ b) => a :~: b
+
+-- deriving Typeable and PolyKinds don't play well
+instance Typeable2 (:~:) where
+    typeOf2 = const $ mkTyConApp tyCon []
+        where tyCon = MK_TY_CON("Type.Eq",":~:")
+
+-- | Unpack equality evidence and use it.
+-- 
+--   This function compiles with GHC 6.10, but doesn't work. Beware!
+withEq :: (a ~ b => r) -> (a :~: b) -> r
+withEq x Eq = x
+-- This doesn't seem to work in 6.10, so for compatibility, we're not going to use it
+
+instance Category (:~:) where
+    id  = idEq
+    (.) = composeEq
+
+#ifdef HAVE_DEPENDENCIES
+instance Semigroupoid (:~:) where
+    o = composeEq
+
+instance Groupoid (:~:) where
+    inv = flipEq
+#endif
+
+-- would require a dependency on data-lens
+-- instance Tensor (:~:) where
+--  a *** b = idEq2 ||$|| a |$| b
+
+-- | Reflexivity
+idEq :: a :~: a
+idEq = Eq
+
+-- | Transitivity
+composeEq :: (b :~: c) -> (a :~: b) -> (a :~: c)
+composeEq Eq Eq = Eq
+
+-- | Symmetry
+flipEq :: (a :~: b) -> (b :~: a)
+flipEq Eq = Eq
+
+-- | Type constructors are injective
+argumentEq :: (f a :~: g b) -> (a :~: b)
+argumentEq Eq = BUG_5591(Eq)
+
+-- | Use equality evidence to cast between types
+cast, (|>) :: a -> (a :~: b) -> b
+cast a Eq = a
+(|>) = cast
+
+-- * Partial equality
+
+-- | Evidence that @f@ is the outermost type constructor of @a@
+data OuterEq f a where
+    OuterEq :: f i ~ a => OuterEq f a
+
+-- | Evidence that @i@ is the argument type of the outermost type constructor of @a@
+data InnerEq i a where
+    InnerEq :: f i ~ a => InnerEq i a
+
+-- | Unpack partial equality evidence and use it.
+--
+--   This function compiles with GHC 6.10, but doesn't work. Beware!
+withOuterEq :: (forall i. f i ~ a => r) -> OuterEq f a -> r
+withOuterEq x OuterEq = x
+
+-- | Unpack partial equality evidence and use it.
+--
+--   This function compiles with GHC 6.10, but doesn't work. Beware!
+withInnerEq :: (forall f. f i ~ a => r) -> InnerEq i a -> r
+withInnerEq x InnerEq = x
+
+outerEq :: f i :~: a -> OuterEq f a
+outerEq Eq = OuterEq
+
+innerEq :: f i :~: a -> InnerEq i a
+innerEq Eq = InnerEq
+
+assembleEq :: OuterEq f a -> InnerEq i a -> f i :~: a
+assembleEq OuterEq InnerEq = BUG_5591(Eq)
+
+sameInnerEq :: InnerEq i a -> InnerEq j a -> i :~: j
+sameInnerEq InnerEq InnerEq = BUG_5591(Eq)
+
+-- * Testing for equality
+
+DYNAMIC_EQ(,,:~:,a,b,)
+
+-- | Can be implemented by types storing evidence of type equalities, i.e. GADTs.
+-- 
+--   A return value of @Nothing@ can mean any of definite inequality, impossible arguments, or insufficient information.
+--
+--   Minimal complete definition: @maybeEq@ or @(~~)@, plus either:
+-- 
+--       - @piecewiseMaybeEq@, or
+-- 
+--       - both @maybeOuterEq@ and @maybeInnerEq@. or
+-- 
+--       - @(\<~>)@, or
+-- 
+--       - both @(~>)@ and @(<~)@.
+class TypeEq t where
+    maybeEq,          (~~)  :: t a     -> t b -> Maybe (a :~: b)
+    maybeOuterEq,     (~>)  :: t (f i) -> t a -> Maybe (OuterEq f a)
+    maybeInnerEq,     (<~)  :: t (f i) -> t a -> Maybe (InnerEq i a)
+    piecewiseMaybeEq, (<~>) :: t (f i) -> t a -> (Maybe (OuterEq f a), Maybe (InnerEq i a))
+    -- ^ > uncurry (liftA2 assembleEq) (a <~> b) = a ~~ b
+    maybeEq = (~~)
+    (~~)    = maybeEq
+    maybeOuterEq     a b = fst (a <~> b)
+    maybeInnerEq     a b = snd (a <~> b)
+    piecewiseMaybeEq a b = (a ~> b, a <~ b)
+    (~>)  = maybeOuterEq
+    (<~)  = maybeInnerEq
+    (<~>) = piecewiseMaybeEq
+
+instance TypeEq ((:~:) a) where
+    maybeEq      Eq Eq = Just Eq
+    maybeOuterEq Eq Eq = Just OuterEq
+    maybeInnerEq Eq Eq = Just InnerEq
+
+instance TypeEq (InnerEq i) where
+    maybeEq      _ _ = Nothing
+    maybeOuterEq _ _ = Nothing
+    maybeInnerEq InnerEq InnerEq = Just BUG_5591(InnerEq)
+
+instance TypeEq (OuterEq f) where
+    maybeEq      _ _ = Nothing
+    maybeOuterEq OuterEq OuterEq = Just BUG_5591(OuterEq)
+    maybeInnerEq _ _ = Nothing
+
+-- TODO
+-- fixities
+-- other compilers
diff --git a/Type/Eq.hs-boot b/Type/Eq.hs-boot
new file mode 100644
--- /dev/null
+++ b/Type/Eq.hs-boot
@@ -0,0 +1,11 @@
+{-# LANGUAGE GADTs, TypeFamilies, TypeOperators, CPP #-}
+
+#include "macros.h"
+
+LANGUAGE_POLYKINDS
+LANGUAGE_TRUSTWORTHY
+
+module Type.Eq where
+
+data a :~: b where
+    Eq :: (a ~ b) => a :~: b
diff --git a/Type/Eq/Higher.hs b/Type/Eq/Higher.hs
new file mode 100644
--- /dev/null
+++ b/Type/Eq/Higher.hs
@@ -0,0 +1,127 @@
+{-# LANGUAGE GADTs, TypeFamilies, Rank2Types, KindSignatures, TypeOperators, FlexibleContexts, CPP #-}
+
+#include "macros.h"
+
+LANGUAGE_TRUSTWORTHY
+
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+
+-- |  Types and combinators for storing and manipulating evidence of equality between types of higher kind.
+-- 
+--    Available up to @* -> * -> *@. Yell if you need more.
+
+module Type.Eq.Higher (module Type.Eq, module Type.Eq.Higher) where
+
+import Data.Typeable hiding (cast)
+import Type.Eq
+import Type.Eq.Higher.Unsafe
+import Unsafe.Coerce
+
+-- * Additional combinators, kind @*@
+
+-- | Type constructors are generative
+constructorEq :: f a :~: g b -> f ::~:: g
+constructorEq Eq = BUG_5591(Eq1)
+
+sameOuterEq :: OuterEq f a -> OuterEq g a -> f ::~:: g
+sameOuterEq OuterEq OuterEq = BUG_5591(Eq1)
+
+
+-- * Full equality, kind @* -> *@
+
+data (f :: * -> *) ::~:: (g :: * -> *) where
+    Eq1 :: (f ~ g) => f ::~:: g
+
+-- INSTANCE_TYPEABLE(1,::~::,f,g,"Type.Eq.Higher","::~::",())
+
+withEq1 :: (f ~ g => r) -> (f ::~:: g) -> r
+withEq1 x Eq1 = x
+
+-- | Reflexivity
+idEq1 :: f ::~:: f
+idEq1 = Eq1
+
+-- | Transitivity
+composeEq1, (|.|) :: (g ::~:: h) -> (f ::~:: g) -> (f ::~:: h)
+composeEq1 Eq1 Eq1 = Eq1
+(|.|) = composeEq1
+
+-- | Symmetry
+flipEq1 :: (f ::~:: g) -> (g ::~:: f)
+flipEq1 Eq1 = Eq1
+
+-- | Congruence?
+applyEq1, (|$|) :: f ::~:: g -> a :~: b -> f a :~: g b
+applyEq1 Eq1 Eq = Eq
+(|$|) = applyEq1
+
+-- | Type constructors are generative
+constructorEq1 :: m a ::~:: n b -> m :::~::: n
+constructorEq1 Eq1 = BUG_5591(Eq2)
+
+-- | Type constructors are injective
+argumentEq1 :: m a ::~:: n b -> a :~: b
+argumentEq1 Eq1 = BUG_5591(Eq)
+
+DYNAMIC_EQ(1,1,::~::,f,g,())
+
+
+-- * Partial equality, kind @* -> *@
+
+data OuterEq1 (m :: * -> * -> *) (f :: * -> *) where
+    OuterEq1 :: m a ~ f => OuterEq1 m f
+
+data InnerEq1 (a :: *) (f :: * -> *) where
+    InnerEq1 :: m a ~ f => InnerEq1 a f
+
+withOuterEq1 :: (forall a. m a ~ f => r) -> OuterEq1 m f -> r
+withOuterEq1 a OuterEq1 = a
+
+withInnerEq1 :: (forall m. m a ~ f => r) -> InnerEq1 a f -> r
+withInnerEq1 a InnerEq1 = a
+
+outerEq1 :: m a ::~:: f -> OuterEq1 m f
+outerEq1 Eq1 = OuterEq1
+
+innerEq1 :: m a ::~:: f -> InnerEq1 a f
+innerEq1 Eq1 = InnerEq1
+
+assembleEq1 :: OuterEq1 m f -> InnerEq1 a f -> m a ::~:: f
+assembleEq1 OuterEq1 InnerEq1 = BUG_5591(Eq1)
+
+sameOuterEq1 :: OuterEq1 m f -> OuterEq1 n f -> m :::~::: n
+sameOuterEq1 OuterEq1 OuterEq1 = BUG_5591(Eq2)
+
+sameInnerEq1 :: InnerEq1 a f -> InnerEq1 b f -> a :~: b
+sameInnerEq1 InnerEq1 InnerEq1 = BUG_5591(Eq)
+
+
+-- * Full equality, kind @* -> * -> *@
+
+data (m :: * -> * -> *) :::~::: (n :: * -> * -> *) where
+    Eq2 :: (m ~ n) => m :::~::: n
+
+-- INSTANCE_TYPEABLE(2,:::~:::,m,n,"Type.Eq.Higher",":::~:::",() ())
+
+withEq2 :: (m ~ n => r) -> (m :::~::: n) -> r
+withEq2 x Eq2 = x
+
+-- | Reflexivity
+idEq2 :: m :::~::: m
+idEq2 = Eq2
+
+-- | Transitivity
+composeEq2, (||.||) :: (n :::~::: o) -> (m :::~::: n) -> (m :::~::: o)
+composeEq2 Eq2 Eq2 = Eq2
+(||.||) = composeEq2
+
+-- | Symmetry
+flipEq2 :: (m :::~::: n) -> (n :::~::: m)
+flipEq2 Eq2 = Eq2
+
+-- | Congruence?
+applyEq2, (||$||) :: m :::~:::n -> a :~: b -> m a ::~:: n b
+applyEq2 Eq2 Eq = Eq1
+(||$||) = applyEq2
+
+DYNAMIC_EQ(2,2,:::~:::,n,m,() ())
diff --git a/Type/Eq/Higher.hs-boot b/Type/Eq/Higher.hs-boot
new file mode 100644
--- /dev/null
+++ b/Type/Eq/Higher.hs-boot
@@ -0,0 +1,13 @@
+{-# LANGUAGE GADTs, TypeFamilies, KindSignatures, TypeOperators, CPP #-}
+
+#include "macros.h"
+
+LANGUAGE_TRUSTWORTHY
+
+module Type.Eq.Higher where
+
+data (f :: * -> *) ::~:: (g :: * -> *) where
+    Eq1 :: (f ~ g) => f ::~:: g
+
+data (m :: * -> * -> *) :::~::: (n :: * -> * -> *) where
+    Eq2 :: (m ~ n) => m :::~::: n
diff --git a/Type/Eq/Higher/Unsafe.hs b/Type/Eq/Higher/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/Type/Eq/Higher/Unsafe.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE TypeOperators, CPP #-}
+
+#include "macros.h"
+
+LANGUAGE_UNSAFE
+
+module Type.Eq.Higher.Unsafe (module Type.Eq.Unsafe, module Type.Eq.Higher.Unsafe) where
+
+import Type.Eq.Unsafe
+import {-# SOURCE #-} Type.Eq.Higher
+import Unsafe.Coerce
+
+-- | Very unsafe! The same rules apply as for 'unsafeCoerce'.
+unsafeCoercion1 :: f ::~:: g
+unsafeCoercion1 = unsafeCoerce Eq1
+
+-- | Very unsafe! The same rules apply as for 'unsafeCoerce'.
+unsafeCoercion2 :: m :::~::: n
+unsafeCoercion2 = unsafeCoerce Eq2
diff --git a/Type/Eq/Unsafe.hs b/Type/Eq/Unsafe.hs
new file mode 100644
--- /dev/null
+++ b/Type/Eq/Unsafe.hs
@@ -0,0 +1,17 @@
+{-# LANGUAGE TypeOperators, CPP #-}
+
+#include "macros.h"
+
+LANGUAGE_POLYKINDS
+LANGUAGE_UNSAFE
+
+-- | This module is kind-polymorphic if @PolyKinds@ are available (GHC 7.6+).
+
+module Type.Eq.Unsafe where
+
+import {-# SOURCE #-} Type.Eq
+import Unsafe.Coerce
+
+-- | Very unsafe! The same rules apply as for 'unsafeCoerce'.
+unsafeCoercion :: a :~: b
+unsafeCoercion = unsafeCoerce Eq
diff --git a/type-eq.cabal b/type-eq.cabal
new file mode 100644
--- /dev/null
+++ b/type-eq.cabal
@@ -0,0 +1,97 @@
+name:          type-eq
+category:      Type System
+version:       0.1
+author:        Gábor Lehel
+maintainer:    Gábor Lehel <illissius@gmail.com>
+homepage:      http://github.com/glehel/type-eq
+copyright:     Copyright (C) 2012 Gábor Lehel
+license:       BSD3
+license-file:  LICENSE
+stability:     experimental
+cabal-version: >= 1.10
+build-type:    Simple
+synopsis:      Type equality evidence you can carry around
+description:
+    This package provides types and combinators to store and manipulate evidence of equality between types.
+    .
+    To take advantage of kind-polymorphism when it is available but not require it, this it is split into the following primary modules:
+    .
+        - @/Type.Eq/@: Types and combinators which can be kind-polymorphic if @PolyKinds@ are available, but are specific to kind @*@ otherwise.
+    .
+        - @/Type.Eq.Higher/@: Kind-monomorphic types and combinators of higher kind, up to @* -> * -> *@.
+    .
+        - @/Type.Eq.Poly/@: Combinators that require kind-polymorphism. This module is only available if @PolyKinds@ are available.
+    .
+    Support for kind-polymorphism first appeared with GHC 7.4, but because it is too buggy to be practical, it will only be enabled with GHC 7.6.
+    .
+    Major required extensions: @GADTs@, @TypeFamilies@ (for @~@), @Rank2Types@, @TypeOperators@
+    .
+    Optional extensions: @PolyKinds@ (GHC 7.6+)
+    .
+    Minimum GHC: 6.10
+    .
+    Related packages:
+    .
+        - <http://hackage.haskell.org/package/type-equality>
+    .
+        - <http://hackage.haskell.org/package/eq>
+    .
+        - <http://hackage.haskell.org/package/ty>
+    .
+        - <http://hackage.haskell.org/package/dependent-sum>
+    .
+        - <http://hackage.haskell.org/package/categories> (@Data.Category.Discrete@)
+
+source-repository head
+    type:      git
+    location:  git://github.com/glehel/type-eq.git
+
+library
+    default-language:
+        Haskell98
+
+    other-extensions:
+        CPP
+        GADTs
+        Rank2Types
+        TypeFamilies
+        TypeOperators
+        KindSignatures
+        FlexibleContexts
+
+    build-depends:
+        base >= 3.0 && < 4.6
+
+    exposed-modules:
+        Type.Eq
+        Type.Eq.Unsafe
+        Type.Eq.Higher
+        Type.Eq.Higher.Unsafe
+
+-- DeriveDataTypeable and PolyKinds sadly don't mix
+--    if impl(ghc)
+--        cpp-options: -DHAVE_TYPEABLE
+--        other-extensions: DeriveDataTypeable
+
+-- Ran into dependency problems with 6.10 and 6.12 and didn't feel like dealing with it
+    if impl(ghc >= 7.0)
+        cpp-options: -DHAVE_DEPENDENCIES
+        build-depends:
+-- Semigroupoid
+            semigroupoids >= 1.0 && < 1.4,
+-- Groupoid
+            groupoids     >= 0.1 && < 0.3
+-- Tensor
+--            data-lens     >= 2.9 && < 2.11
+
+    if impl(ghc >= 7.2)
+        other-extensions: Trustworthy
+
+--    if impl(ghc >= 7.6)
+--        exposed-modules:  Type.Eq.Poly
+--        other-extensions: PolyKinds, Unsafe
+
+    include-dirs: .
+
+    ghc-options:
+        -Wall