diff --git a/.travis.yml b/.travis.yml
deleted file mode 100644
--- a/.travis.yml
+++ /dev/null
@@ -1,171 +0,0 @@
-# This Travis job script has been generated by a script via
-#
-#   haskell-ci '--output=.travis.yml' '--config=cabal.haskell-ci' 'cabal.project'
-#
-# To regenerate the script (for example after adjusting tested-with) run
-#
-#   haskell-ci regenerate
-#
-# For more information, see https://github.com/haskell-CI/haskell-ci
-#
-# version: 0.10
-#
-version: ~> 1.0
-language: c
-os: linux
-dist: xenial
-git:
-  # whether to recursively clone submodules
-  submodules: false
-notifications:
-  irc:
-    channels:
-      - irc.freenode.org#haskell-lens
-    skip_join: true
-    template:
-      - "\x0313eq\x03/\x0306%{branch}\x03 \x0314%{commit}\x03 %{build_url} %{message}"
-cache:
-  directories:
-    - $HOME/.cabal/packages
-    - $HOME/.cabal/store
-    - $HOME/.hlint
-before_cache:
-  - rm -fv $CABALHOME/packages/hackage.haskell.org/build-reports.log
-  # remove files that are regenerated by 'cabal update'
-  - rm -fv $CABALHOME/packages/hackage.haskell.org/00-index.*
-  - rm -fv $CABALHOME/packages/hackage.haskell.org/*.json
-  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.cache
-  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar
-  - rm -fv $CABALHOME/packages/hackage.haskell.org/01-index.tar.idx
-  - rm -rfv $CABALHOME/packages/head.hackage
-jobs:
-  include:
-    - compiler: ghc-8.10.1
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.10.1","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-8.8.3
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.8.3","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-8.6.5
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.6.5","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-8.4.4
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.4.4","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-8.2.2
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.2.2","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-8.0.2
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-8.0.2","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-7.10.3
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.10.3","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-7.8.4
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.8.4","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-7.6.3
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.6.3","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-7.4.2
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.4.2","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-7.2.2
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.2.2","cabal-install-3.2"]}}
-      os: linux
-    - compiler: ghc-7.0.4
-      addons: {"apt":{"sources":[{"sourceline":"deb http://ppa.launchpad.net/hvr/ghc/ubuntu xenial main","key_url":"https://keyserver.ubuntu.com/pks/lookup?op=get&search=0x063dab2bdc0b3f9fcebc378bff3aeacef6f88286"}],"packages":["ghc-7.0.4","cabal-install-3.2"]}}
-      os: linux
-  allow_failures:
-    - compiler: ghc-7.0.4
-    - compiler: ghc-7.2.2
-before_install:
-  - HC=$(echo "/opt/$CC/bin/ghc" | sed 's/-/\//')
-  - WITHCOMPILER="-w $HC"
-  - HADDOCK=$(echo "/opt/$CC/bin/haddock" | sed 's/-/\//')
-  - HCPKG="$HC-pkg"
-  - unset CC
-  - CABAL=/opt/ghc/bin/cabal
-  - CABALHOME=$HOME/.cabal
-  - export PATH="$CABALHOME/bin:$PATH"
-  - TOP=$(pwd)
-  - "HCNUMVER=$(${HC} --numeric-version|perl -ne '/^(\\d+)\\.(\\d+)\\.(\\d+)(\\.(\\d+))?$/; print(10000 * $1 + 100 * $2 + ($3 == 0 ? $5 != 1 : $3))')"
-  - echo $HCNUMVER
-  - CABAL="$CABAL -vnormal+nowrap"
-  - set -o pipefail
-  - TEST=--enable-tests
-  - BENCH=--enable-benchmarks
-  - HEADHACKAGE=false
-  - rm -f $CABALHOME/config
-  - |
-    echo "verbose: normal +nowrap +markoutput"          >> $CABALHOME/config
-    echo "remote-build-reporting: anonymous"            >> $CABALHOME/config
-    echo "write-ghc-environment-files: always"          >> $CABALHOME/config
-    echo "remote-repo-cache: $CABALHOME/packages"       >> $CABALHOME/config
-    echo "logs-dir:          $CABALHOME/logs"           >> $CABALHOME/config
-    echo "world-file:        $CABALHOME/world"          >> $CABALHOME/config
-    echo "extra-prog-path:   $CABALHOME/bin"            >> $CABALHOME/config
-    echo "symlink-bindir:    $CABALHOME/bin"            >> $CABALHOME/config
-    echo "installdir:        $CABALHOME/bin"            >> $CABALHOME/config
-    echo "build-summary:     $CABALHOME/logs/build.log" >> $CABALHOME/config
-    echo "store-dir:         $CABALHOME/store"          >> $CABALHOME/config
-    echo "install-dirs user"                            >> $CABALHOME/config
-    echo "  prefix: $CABALHOME"                         >> $CABALHOME/config
-    echo "repository hackage.haskell.org"               >> $CABALHOME/config
-    echo "  url: http://hackage.haskell.org/"           >> $CABALHOME/config
-install:
-  - ${CABAL} --version
-  - echo "$(${HC} --version) [$(${HC} --print-project-git-commit-id 2> /dev/null || echo '?')]"
-  - |
-    echo "program-default-options"                >> $CABALHOME/config
-    echo "  ghc-options: $GHCJOBS +RTS -M6G -RTS" >> $CABALHOME/config
-  - cat $CABALHOME/config
-  - rm -fv cabal.project cabal.project.local cabal.project.freeze
-  - travis_retry ${CABAL} v2-update -v
-  # Generate cabal.project
-  - rm -rf cabal.project cabal.project.local cabal.project.freeze
-  - touch cabal.project
-  - |
-    echo "packages: ." >> cabal.project
-  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package eq' >> cabal.project ; fi
-  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
-  - |
-  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(eq)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
-  - cat cabal.project || true
-  - cat cabal.project.local || true
-  - if [ -f "./configure.ac" ]; then (cd "." && autoreconf -i); fi
-  - ${CABAL} v2-freeze $WITHCOMPILER ${TEST} ${BENCH}
-  - "cat cabal.project.freeze | sed -E 's/^(constraints: *| *)//' | sed 's/any.//'"
-  - rm  cabal.project.freeze
-  - travis_wait 40 ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} --dep -j2 all
-script:
-  - DISTDIR=$(mktemp -d /tmp/dist-test.XXXX)
-  # Packaging...
-  - ${CABAL} v2-sdist all
-  # Unpacking...
-  - mv dist-newstyle/sdist/*.tar.gz ${DISTDIR}/
-  - cd ${DISTDIR} || false
-  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec tar -xvf '{}' \;
-  - find . -maxdepth 1 -type f -name '*.tar.gz' -exec rm       '{}' \;
-  - PKGDIR_eq="$(find . -maxdepth 1 -type d -regex '.*/eq-[0-9.]*')"
-  # Generate cabal.project
-  - rm -rf cabal.project cabal.project.local cabal.project.freeze
-  - touch cabal.project
-  - |
-    echo "packages: ${PKGDIR_eq}" >> cabal.project
-  - if [ $HCNUMVER -ge 80200 ] ; then echo 'package eq' >> cabal.project ; fi
-  - "if [ $HCNUMVER -ge 80200 ] ; then echo '  ghc-options: -Werror=missing-methods' >> cabal.project ; fi"
-  - |
-  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(eq)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
-  - cat cabal.project || true
-  - cat cabal.project.local || true
-  # Building with tests and benchmarks...
-  # build & run tests, build benchmarks
-  - ${CABAL} v2-build $WITHCOMPILER ${TEST} ${BENCH} all
-  # cabal check...
-  - (cd ${PKGDIR_eq} && ${CABAL} -vnormal check)
-  # haddock...
-  - ${CABAL} v2-haddock $WITHCOMPILER --with-haddock $HADDOCK ${TEST} ${BENCH} all
-
-# REGENDATA ("0.10",["--output=.travis.yml","--config=cabal.haskell-ci","cabal.project"])
-# EOF
diff --git a/CHANGELOG.markdown b/CHANGELOG.markdown
--- a/CHANGELOG.markdown
+++ b/CHANGELOG.markdown
@@ -1,3 +1,25 @@
+4.3 [2021.10.31]
+----------------
+* Generalize the types of `Data.Eq.Type.lower{,2,3}`:
+
+  ```diff
+  -lower :: f a := f b -> a := b
+  +lower :: f a := g b -> a := b
+
+  -lower2 :: f a c := f b c  -> a := b
+  +lower2 :: f a c := g b c' -> a := b
+
+  -lower3 :: f a c d := f b c  d  -> a := b
+  +lower3 :: f a c d := g b c' d' -> a := b
+  ```
+
+  The types of `Data.Eq.Type.Hetero.lower{,2,3}` have been generalized
+  analogously.
+* `Data.Eq.Type.Hetero.lower{,2,3}` now have the same order of type variables
+  as their counterparts in `Data.Eq.Type`.
+* Add an `apply` function to `Data.Eq.Type` and `Data.Eq.Type.Hetero`.
+* Drop support for pre-7.0 versions of GHC.
+
 4.2.1 [2020.10.01]
 ------------------
 * Allow building with GHC 9.0.
diff --git a/README.markdown b/README.markdown
--- a/README.markdown
+++ b/README.markdown
@@ -1,11 +1,11 @@
 eq
 ==
 
-[![Hackage](https://img.shields.io/hackage/v/eq.svg)](https://hackage.haskell.org/package/eq) [![Build Status](https://secure.travis-ci.org/ekmett/eq.png?branch=master)](http://travis-ci.org/ekmett/eq)
+[![Hackage](https://img.shields.io/hackage/v/eq.svg)](https://hackage.haskell.org/package/eq) [![Build Status](https://github.com/ekmett/eq/workflows/Haskell-CI/badge.svg)](https://github.com/ekmett/eq/actions?query=workflow%3AHaskell-CI)
 
 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) 
+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
diff --git a/eq.cabal b/eq.cabal
--- a/eq.cabal
+++ b/eq.cabal
@@ -1,6 +1,6 @@
 name:          eq
 category:      Type System
-version:       4.2.1
+version:       4.3
 license:       BSD3
 cabal-version: >= 1.10
 license-file:  LICENSE
@@ -23,13 +23,14 @@
              , GHC == 8.2.2
              , GHC == 8.4.4
              , GHC == 8.6.5
-             , GHC == 8.8.3
-             , GHC == 8.10.1
+             , GHC == 8.8.4
+             , GHC == 8.10.7
+             , GHC == 9.0.1
+             , GHC == 9.2.1
 
 extra-source-files:
   .gitignore
   .vim.custom
-  .travis.yml
   CHANGELOG.markdown
   README.markdown
 
@@ -44,18 +45,21 @@
     TypeOperators
 
   build-depends:
-    base          == 4.*,
+    base          >= 4.3 && <5,
     semigroupoids >= 4 && < 6
 
   exposed-modules:
     Data.Eq.Type
 
-  if impl(ghc >= 7.0)
-    default-extensions: TypeFamilies
-    cpp-options: -DLANGUAGE_TypeFamilies
+  -- We always have TypeFamilies, we don't support pre GHC-7 compilers.
+  -- TypeFamilies are needed to implement lower combinators.
+  default-extensions: TypeFamilies
 
   if impl(ghc >= 8.2)
     exposed-modules: Data.Eq.Type.Hetero
+
+  if !impl(ghc >= 7.8)
+     build-depends: type-equality >=1 && <2
 
   ghc-options: -Wall
   default-language: Haskell2010
diff --git a/src/Data/Eq/Type.hs b/src/Data/Eq/Type.hs
--- a/src/Data/Eq/Type.hs
+++ b/src/Data/Eq/Type.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE CPP, Rank2Types, TypeOperators #-}
+{-# LANGUAGE CPP, Rank2Types, ScopedTypeVariables, TypeOperators #-}
 #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 706
 #define LANGUAGE_PolyKinds
 {-# LANGUAGE PolyKinds #-}
@@ -7,10 +7,9 @@
 {-# LANGUAGE RoleAnnotations #-}
 #endif
 #if defined(__GLASGOW_HASKELL__) && MIN_VERSION_base(4,7,0)
-#define HAS_DATA_TYPE_EQUALITY 1
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE ScopedTypeVariables #-}
+#define HAS_DATA_TYPE_COERCION 1
 #endif
+{-# LANGUAGE GADTs #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -37,22 +36,23 @@
   , trans
   , symm
   , coerce
+#ifdef LANGUAGE_PolyKinds
+  , apply
+#endif
   -- * Lifting equality
   , lift
   , lift2, lift2'
   , lift3, lift3'
-#ifdef LANGUAGE_TypeFamilies
   -- * Lowering equality
   , lower
   , lower2
   , lower3
-#endif
-#ifdef HAS_DATA_TYPE_EQUALITY
   -- * 'Eq.:~:' equivalence
   -- | "Data.Type.Equality" GADT definition is equivalent in power
   , fromLeibniz
   , toLeibniz
 
+#ifdef HAS_DATA_TYPE_COERCION
   -- * 'Co.Coercion' conversion
   -- | Leibnizian equality can be converted to representational equality
   , reprLeibniz
@@ -64,10 +64,10 @@
 import Data.Semigroupoid
 import Data.Groupoid
 
-#ifdef HAS_DATA_TYPE_EQUALITY
+#ifdef HAS_DATA_TYPE_COERCION
 import qualified Data.Type.Coercion as Co
-import qualified Data.Type.Equality as Eq
 #endif
+import qualified Data.Type.Equality as Eq
 
 infixl 4 :=
 
@@ -87,6 +87,14 @@
 coerce :: a := b -> a -> b
 coerce f = uncoerce . subst f . Coerce
 
+#ifdef LANGUAGE_PolyKinds
+newtype Apply a b f g = Apply { unapply :: f a := g b }
+
+-- | Apply one equality to another, respectively
+apply :: f := g -> a := b -> f a := g b
+apply fg ab = unapply (subst fg (Apply (lift ab)))
+#endif
+
 -- | Equality forms a category
 instance Category (:=) where
   id = Refl id
@@ -127,40 +135,62 @@
 lift3' :: a := b -> c := d -> e := f -> g a c e := g b d f
 lift3' ab cd ef = lift3 ab `subst` lift2 cd `subst` lift ef
 
-#ifdef LANGUAGE_TypeFamilies
-# ifdef LANGUAGE_PolyKinds
-type family Inj  (f :: j -> k)           (a :: k) :: j
-type family Inj2 (f :: i -> j -> k)      (a :: k) :: i
-type family Inj3 (f :: h -> i -> j -> k) (a :: k) :: h
-# else
-type family Inj  (f :: * -> *)           (a :: *) :: *
-type family Inj2 (f :: * -> * -> *)      (a :: *) :: *
-type family Inj3 (f :: * -> * -> * -> *) (a :: *) :: *
-# endif
+#ifdef LANGUAGE_PolyKinds
+-- This is all more complicated than it needs to be. Ideally, we would just
+-- write:
+--
+--   data family Lower (a :: j) (b :: k)
+--   newtype instance Lower a (f x) = Lower { unlower :: a := x }
+--
+--   lower :: forall a b f g. f a := g b -> a := b
+--   lower eq = unlower (subst eq (Lower refl :: Lower a (f a)))
+--
+-- And similarly for Lower{2,3}. Unfortunately, this won't typecheck on
+-- GHC 7.6 through 7.10 due to an old typechecker bug. To work around the
+-- issue, we must:
+--
+-- 1. Pass `f` and `g` as explicit arguments to the GenInj{,2,3} type family,
+--    and
+--
+-- 2. Define overlapping instances for GenInj{,2,3}.
+--
+-- Part (2) of this workaround prevents us from using a data family here, as
+-- GHC will reject overlapping data family instances as conflicting.
+type family GenInj  (f :: j -> k)           (g :: j -> k)             (x :: k) :: j
+type family GenInj2 (f :: i -> j -> k)      (g :: i -> j' -> k)       (x :: k) :: i
+type family GenInj3 (f :: h -> i -> j -> k) (g :: h -> i' -> j' -> k) (x :: k) :: h
+#else
+type family GenInj  (f :: * -> *)           (g :: * -> *)           (x :: *) :: *
+type family GenInj2 (f :: * -> * -> *)      (g :: * -> * -> *)      (x :: *) :: *
+type family GenInj3 (f :: * -> * -> * -> *) (g :: * -> * -> * -> *) (x :: *) :: *
+#endif
 
-type instance Inj  f (f a)     = a
-type instance Inj2 f (f a b)   = a
-type instance Inj3 f (f a b c) = a
+type instance GenInj  f g (f a) = a
+type instance GenInj  f g (g b) = b
 
-newtype Lower  f a b = Lower  { unlower  :: Inj  f a := Inj  f b }
-newtype Lower2 f a b = Lower2 { unlower2 :: Inj2 f a := Inj2 f b }
-newtype Lower3 f a b = Lower3 { unlower3 :: Inj3 f a := Inj3 f b }
+type instance GenInj2 f g (f a c)  = a
+type instance GenInj2 f g (g b c') = b
 
--- | Type constructors are injective, so you can lower equality through any
--- type constructor ...
-lower :: forall a b f. f a := f b -> a := b
-lower eq = unlower (subst eq (Lower refl :: Lower f (f a) (f a)))
+type instance GenInj3 f g (f a c  d)  = a
+type instance GenInj3 f g (g b c' d') = b
 
+newtype Lower  f g a x = Lower  { unlower  :: a := GenInj  f g x }
+newtype Lower2 f g a x = Lower2 { unlower2 :: a := GenInj2 f g x }
+newtype Lower3 f g a x = Lower3 { unlower3 :: a := GenInj3 f g x }
+
+-- | Type constructors are generative and injective, so you can lower equality
+-- through any type constructors ...
+lower :: forall a b f g. f a := g b -> a := b
+lower eq = unlower (subst eq (Lower refl :: Lower f g a (f a)))
+
 -- | ... in any position ...
-lower2 :: forall a b c f. f a c := f b c -> a := b
-lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 f (f a c) (f a c)))
+lower2 :: forall a b f g c c'. f a c := g b c' -> a := b
+lower2 eq = unlower2 (subst eq (Lower2 refl :: Lower2 f g a (f a c)))
 
 -- | ... these definitions are poly-kinded on GHC 7.6 and up.
-lower3 :: forall a b c d f. f a c d := f b c d -> a := b
-lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 f (f a c d) (f a c d)))
-#endif
+lower3 :: forall a b f g c c' d d'. f a c d := g b c' d' -> a := b
+lower3 eq = unlower3 (subst eq (Lower3 refl :: Lower3 f g a (f a c d)))
 
-#ifdef HAS_DATA_TYPE_EQUALITY
 fromLeibniz :: a := b -> a Eq.:~: b
 fromLeibniz a = subst a Eq.Refl
 
@@ -170,6 +200,7 @@
 instance Eq.TestEquality ((:=) a) where
   testEquality fa fb = Just (fromLeibniz (trans (symm fa) fb))
 
+#ifdef HAS_DATA_TYPE_COERCION
 reprLeibniz :: a := b -> Co.Coercion a b
 reprLeibniz a = subst a Co.Coercion
 
diff --git a/src/Data/Eq/Type/Hetero.hs b/src/Data/Eq/Type/Hetero.hs
--- a/src/Data/Eq/Type/Hetero.hs
+++ b/src/Data/Eq/Type/Hetero.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 {-# LANGUAGE TypeOperators #-}
@@ -29,6 +30,7 @@
   , trans
   , symm
   , coerce
+  , apply
   -- * Lifting equality
   , lift
   , lift2, lift2'
@@ -61,7 +63,6 @@
 import qualified Data.Type.Equality as Eq
 import           Data.Kind
 import qualified Data.Eq.Type as ET
-import           GHC.Exts (Any)
 import           Prelude hiding (id, (.))
 
 infixl 4 :==
@@ -78,16 +79,37 @@
 refl :: a :== a
 refl = HRefl id
 
-newtype Coerce (a :: k) = Coerce { uncoerce :: MassageKind Type a }
-
-type family MassageKind (j :: Type) (a :: k) :: j where
-  MassageKind j (a :: j) = a
-  MassageKind _ _        = Any
+data family Coerce :: forall k. k -> Type
+newtype instance Coerce (a :: Type) = Coerce { uncoerce :: a }
 
 -- | If two things are equal, you can convert one to the other.
 coerce :: a :== b -> a -> b
 coerce f = uncoerce . hsubst f . Coerce
 
+newtype Pair1 :: forall j1 k1 j2.
+                 j1 -> k1 -> j2
+              -> forall k2. k2 -> Type where
+  Pair1 :: { unpair1 :: '(a1, a2) :== '(b1, b2) } -> Pair1 a1 b1 a2 b2
+
+newtype Pair2 :: forall j2 k2 j1.
+                 j2 -> k2 -> j1
+              -> forall k1. k1 -> Type where
+  Pair2 :: { unpair2 :: '(a1, a2) :== '(b1, b2) } -> Pair2 a2 b2 a1 b1
+
+-- | Lift two equalities pairwise.
+pair :: a1 :== b1 -> a2 :== b2 -> '(a1, a2) :== '(b1, b2)
+pair ab1 ab2 = unpair2 $ hsubst ab1 $ Pair2 $ unpair1 $ hsubst ab2 $ Pair1 refl
+
+data family Apply :: forall j1 j2.
+                     (j1 -> j2) -> j1
+                  -> forall k. k -> Type
+newtype instance Apply (f :: j1 -> j2) (a :: j1) '((g :: k1 -> k2), (b :: k1))
+  = Apply { unapply :: f a :== g b }
+
+-- | Apply one equality to another, respectively
+apply :: f :== g -> a :== b -> f a :== g b
+apply fg ab = unapply $ hsubst (pair fg ab) $ Apply refl
+
 newtype Push :: (forall j k. j -> k -> Type)
              -> forall j. j -> forall k. k -> Type where
   Push :: forall (p :: forall j k. j -> k -> Type)
@@ -123,24 +145,22 @@
 symm :: a :== b -> b :== a
 symm ab = unpush $ unsymm $ hsubst ab $ Symm $ Push refl
 
-newtype Lift :: forall j r.
-                (j -> r) -> j
-             -> forall k. k
-             -> Type where
-  Lift :: forall j r k (f :: j -> r) (a :: j) (b :: k).
-          { unlift :: f a :== f (MassageKind j b) } -> Lift f a b
+data family Lift :: forall j r. (j -> r) -> j
+                 -> forall k. k
+                 -> Type
+newtype instance Lift f (a :: j) (b :: j) =
+  Lift { unlift :: f a :== f b }
 
 -- | You can lift equality into any type constructor...
 lift :: a :== b -> f a :== f b
 lift f = unlift $ hsubst f $ Lift refl
 
-newtype Lift2 :: forall j1 j2 r.
-                 (j1 -> j2 -> r) -> j1 -> j2
-              -> forall k. k
-              -> Type where
-  Lift2 :: forall j1 j2 r k
-                  (f :: j1 -> j2 -> r) (a :: j1) (b :: k) (c :: j2).
-           { unlift2 :: f a c :== f (MassageKind j1 b) c } -> Lift2 f a c b
+data family Lift2 :: forall j1 j2 r.
+                     (j1 -> j2 -> r) -> j1 -> j2
+                  -> forall k. k
+                  -> Type
+newtype instance Lift2 f (a :: j1) (c :: j2) (b :: j1) =
+  Lift2 { unlift2 :: f a c :== f b c }
 
 -- | ... in any position.
 lift2 :: a :== b -> f a c :== f b c
@@ -149,13 +169,12 @@
 lift2' :: a :== b -> c :== d -> f a c :== f b d
 lift2' ab cd = unpush $ lift2 ab `hsubst` Push (lift cd)
 
-newtype Lift3 :: forall j1 j2 j3 r.
-                 (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3
-              -> forall k. k
-              -> Type where
-  Lift3 :: forall j1 j2 j3 r k
-                  (f :: j1 -> j2 -> j3 -> r) (a :: j1) (b :: k) (c :: j2) (d :: j3).
-           { unlift3 :: f a c d :== f (MassageKind j1 b) c d } -> Lift3 f a c d b
+data family Lift3 :: forall j1 j2 j3 r.
+                     (j1 -> j2 -> j3 -> r) -> j1 -> j2 -> j3
+                  -> forall k. k
+                  -> Type
+newtype instance Lift3 f (a :: j1) (c :: j2) (d :: j3) (b :: j1) =
+  Lift3 { unlift3 :: f a c d :== f b c d }
 
 lift3 :: a :== b -> f a c d :== f b c d
 lift3 f = unlift3 $ hsubst f $ Lift3 refl
@@ -163,58 +182,37 @@
 lift3' :: a :== b -> c :== d -> e :== f -> g a c e :== g b d f
 lift3' ab cd ef = unpush $ unpush (lift3 ab `hsubst` Push (lift2 cd)) `hsubst` Push (lift ef)
 
-newtype Lower :: Type
-              -> forall j. j
-              -> forall k. k
-              -> Type where
-  Lower :: forall i j k (a :: j) (b :: k).
-           { unlower :: Inj i a :== Inj i (MassageKind j b) } -> Lower i a b
-
-type family Inj (j :: Type) (a :: k) :: j where
-  Inj j (f (a :: j)) = a
-  Inj _ _            = Any
-
--- | Type constructors are injective, so you can lower equality through any type constructor.
-lower :: forall j k (f :: j -> k) (a :: j) (b :: j).
-         f a :== f b -> a :== b
-lower f = unlower $ hsubst f (Lower refl :: Lower j (f a) (f a))
-
-newtype Lower2 :: Type
-               -> forall j. j
-               -> forall k. k
-               -> Type where
-  Lower2 :: forall i j k (a :: j) (b :: k).
-            { unlower2 :: Inj2 i a :== Inj2 i (MassageKind j b) } -> Lower2 i a b
+data family Lower :: forall j. j
+                  -> forall k. k
+                  -> Type
+newtype instance Lower a (f x) = Lower { unlower :: a :== x }
 
-type family Inj2 (j :: Type) (a :: k) :: j where
-  Inj2 j (f (a :: j) b) = a
-  Inj2 _ _              = Any
+-- | Type constructors are generative and injective, so you can lower equality
+-- through any type constructors.
+lower :: forall a b f g. f a :== g b -> a :== b
+lower f = unlower $ hsubst f (Lower refl :: Lower a (f a))
 
-lower2 :: forall i j k (f :: i -> j -> k) (a :: i) (b :: i) (c :: j).
-          f a c :== f b c -> a :== b
-lower2 f = unlower2 $ hsubst f (Lower2 refl :: Lower2 i (f a c) (f a c))
+data family Lower2 :: forall j. j
+                   -> forall k. k
+                   -> Type
+newtype instance Lower2 a (f x c) = Lower2 { unlower2 :: a :== x }
 
-newtype Lower3 :: Type
-               -> forall j. j
-               -> forall k. k
-               -> Type where
-  Lower3 :: forall i j k (a :: j) (b :: k).
-            { unlower3 :: Inj3 i a :== Inj3 i (MassageKind j b) } -> Lower3 i a b
+lower2 :: forall a b f g c c'. f a c :== g b c' -> a :== b
+lower2 f = unlower2 $ hsubst f (Lower2 refl :: Lower2 a (f a c))
 
-type family Inj3 (j :: Type) (a :: k) :: j where
-  Inj3 j (f (a :: j) b c) = a
-  Inj3 _ _                = Any
+data family Lower3 :: forall j. j
+                   -> forall k. k
+                   -> Type
+newtype instance Lower3 a (f x c d) = Lower3 { unlower3 :: a :== x }
 
-lower3 :: forall h i j k (f :: h -> i -> j -> k) (a :: h) (b :: h) (c :: i) (d :: j).
-          f a c d :== f b c d -> a :== b
-lower3 f = unlower3 $ hsubst f (Lower3 refl :: Lower3 h (f a c d) (f a c d))
+lower3 :: forall a b f g c c' d d'. f a c d :== g b c' d' -> a :== b
+lower3 f = unlower3 $ hsubst f (Lower3 refl :: Lower3 a (f a c d))
 
-newtype Flay :: forall j.
-                (j -> j -> Type) -> j
-             -> forall k. k
-             -> Type where
-  Flay :: forall j k (p :: j -> j -> Type) (a :: j) (b :: k).
-          { unflay :: p a (MassageKind j b) } -> Flay p a b
+data family Flay :: forall j.
+                    (j -> j -> Type) -> j
+                 -> forall k. k
+                 -> Type
+newtype instance Flay p (a :: j) (b :: j) = Flay { unflay :: p a b }
 
 -- | Convert an appropriately kinded heterogeneous Leibnizian equality into
 -- a homogeneous Leibnizian equality '(ET.:=)'.
@@ -233,7 +231,7 @@
 toLeibniz Eq.Refl = refl
 
 heteroFromLeibniz :: a :== b -> a Eq.:~~: b
-heteroFromLeibniz f = unpush $ hsubst f $ Push $ Eq.HRefl
+heteroFromLeibniz f = unpush $ hsubst f $ Push Eq.HRefl
 
 heteroToLeibniz :: a Eq.:~~: b -> a :== b
 heteroToLeibniz Eq.HRefl = refl