diff --git a/CHANGELOG b/CHANGELOG
deleted file mode 100644
--- a/CHANGELOG
+++ /dev/null
@@ -1,17 +0,0 @@
-0.1.2
-  * Add subst2. Thanks to James Koppel.
-
-0.1.1
-  * Turn on PolyKinds for GHC >= 7.6. Thanks to Ben Franksen.
-
-0.1.0.2
-  * Move 'Build-depends' to 'Library' section. Thanks to Brent Yorgey.
-
-0.1.0.1
-  * Added EqT instance for (:=:)
-  * Removed 'cast' as synonym for 'coerce'.
-  * Show and read instances for (:=:).
-  * Lots of small changes.
-
-0.1.0
-  * Initial version.
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,24 @@
+## 1.0.1
+
+  * Support GHC-8.6.5..GHC-9.10.1
+
+## 1
+  * Rewrite the library to contain a shim of recent `base` `Data.Type.Equality` module.
+
+## 0.1.2
+  * Add subst2. Thanks to James Koppel.
+
+## 0.1.1
+  * Turn on PolyKinds for GHC >= 7.6. Thanks to Ben Franksen.
+
+## 0.1.0.2
+  * Move 'Build-depends' to 'Library' section. Thanks to Brent Yorgey.
+
+## 0.1.0.1
+  * Added EqT instance for (:=:)
+  * Removed 'cast' as synonym for 'coerce'.
+  *  Show and read instances for (:=:).
+  * Lots of small changes.
+
+##  0.1.0
+  * Initial version.
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,28 +1,30 @@
-Copyright (c) Erik Hesselink 2009
+Copyright (c) 2009 Erik Hesselink, 2019 Oleg Grenrus, Ryan Scott
 
 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.
+modification, are permitted provided that the following conditions are met:
 
-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.
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
 
+    * 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.
+
+    * Neither the name of authors nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS 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 COPYRIGHT
+OWNER 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
deleted file mode 100644
--- a/Setup.lhs
+++ /dev/null
@@ -1,5 +0,0 @@
-#! /usr/bin/env runhaskell
-
->import Distribution.Simple
->main = defaultMain
-
diff --git a/src-hetero/Data/Type/Equality/Hetero.hs b/src-hetero/Data/Type/Equality/Hetero.hs
new file mode 100644
--- /dev/null
+++ b/src-hetero/Data/Type/Equality/Hetero.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TypeOperators       #-}
+-- | This module shims kind heterogeneous propositional equality.
+module Data.Type.Equality.Hetero (
+    (:~~:)(..),
+) where
+
+import Data.Type.Equality ((:~~:)(..))
diff --git a/src/Data/Type/Equality.hs b/src/Data/Type/Equality.hs
deleted file mode 100644
--- a/src/Data/Type/Equality.hs
+++ /dev/null
@@ -1,124 +0,0 @@
-{-# LANGUAGE TypeOperators
-           , GADTs
-           , FlexibleInstances
-           , CPP
-           #-}
-#if __GLASGOW_HASKELL__ >= 706
-{-# LANGUAGE PolyKinds #-}
-#endif
--------------------------------------------------------------------------------
--- |
--- 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
-  , subst2
-  
-  , 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 :=:
-
--- | Any value is just shown as "Refl", but this cannot be derived for
--- a GADT, so it is defined here manually.
-instance Show (a :=: b) where
-  showsPrec _ Refl = showString "Refl"
-
--- | We can only read values if the result is @a :=: a@, not @a :=: b@
--- since that is not true, in general. We just parse the string
--- "Refl", optionally surrounded with parentheses, and return 'Refl'.
-instance Read (a :=: a) where
-  readsPrec _ = readParen False (\s -> [(Refl, r) | ("Refl", r) <- lex s])
-
-#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
-
--- | Substitution inside nested type constructors. This is equivalent 
--- to 'coerce' '.' 'cong' '.' 'cong'.
-subst2 :: a :=: b -> f (g a) -> f (g b)
-subst2 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
--- a/type-equality.cabal
+++ b/type-equality.cabal
@@ -1,32 +1,50 @@
-Name:                type-equality
-Version:             0.1.2
-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.6
-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
-Tested-With:         GHC == 7.0.4, GHC == 7.4.1, GHC == 7.6.1
-Extra-Source-Files:  CHANGELOG
+name:               type-equality
+version:            1.0.1
+stability:          provisional
+cabal-version:      >=1.10
+build-type:         Simple
+author:
+  Oleg Grenrus <oleg.grenrus@iki.fi>, Ryan Scott <ryan.gl.scott@gmail.com>, Erik Hesselink <hesselink@gmail.com>, Martijn van Steenbergen
 
-Library
-  Build-Depends:       base >= 3 && < 5
-  HS-Source-Dirs:      src
-  GHC-Options:         -Wall
-  Exposed-Modules:     Data.Type.Equality
+maintainer:
+  Oleg Grenrus <oleg.grenrus@iki.fi>, Ryan Scott <ryan.gl.scott@gmail.com>, Erik Hesselink <hesselink@gmail.com>
 
-Source-Repository head
-  Type:                git
-  Location:            git://github.com/hesselink/type-equality.git
+license:            BSD3
+license-file:       LICENSE
+homepage:           https://github.com/hesselink/type-equality
+category:           Data, Dependent Types
+synopsis:           Data.Type.Equality compat package
+description:
+  This library defines a propositional equality data type,
+  shims @Data.Type.Equality@ as well as possible for older GHCs (< 7.8).
+  .
+  @
+  data a :~: b where
+  \    Refl :: a :~: a
+  @
+  .
+  The module @Data.Type.Equality.Hetero@ shims @:~~:@ equality, for
+  compilers with @PolyKinds@
+
+extra-source-files: CHANGELOG.md
+tested-with:
+  GHC ==8.6.5
+   || ==8.8.4
+   || ==8.10.7
+   || ==9.0.2
+   || ==9.2.8
+   || ==9.4.8
+   || ==9.6.5
+   || ==9.8.2
+   || ==9.10.1
+
+source-repository head
+  type:     git
+  location: git://github.com/hesselink/type-equality
+
+library
+  default-language: Haskell2010
+  build-depends:    base >=4.12 && <4.21
+  hs-source-dirs:   src-hetero
+  exposed-modules:  Data.Type.Equality.Hetero
+  other-extensions: PolyKinds