diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,2 @@
+# 0.1 [2017-07-02]
+* Initial release.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2017, 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:
+
+    * 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 Ryan Scott 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,18 @@
+# `eliminators`
+[![Hackage](https://img.shields.io/hackage/v/eliminators.svg)][Hackage: eliminators]
+[![Hackage Dependencies](https://img.shields.io/hackage-deps/v/eliminators.svg)](http://packdeps.haskellers.com/reverse/eliminators)
+[![Haskell Programming Language](https://img.shields.io/badge/language-Haskell-blue.svg)][Haskell.org]
+[![BSD3 License](http://img.shields.io/badge/license-BSD3-brightgreen.svg)][tl;dr Legal: BSD3]
+[![Build](https://img.shields.io/travis/RyanGlScott/eliminators.svg)](https://travis-ci.org/RyanGlScott/eliminators)
+
+[Hackage: eliminators]:
+  http://hackage.haskell.org/package/eliminators
+  "eliminators package on Hackage"
+[Haskell.org]:
+  http://www.haskell.org
+  "The Haskell Programming Language"
+[tl;dr Legal: BSD3]:
+  https://tldrlegal.com/license/bsd-3-clause-license-%28revised%29
+  "BSD 3-Clause License (Revised)"
+
+This library provides eliminators for inductive data types, leveraging the power of the `singletons` library to allow dependently typed elimination.
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/eliminators.cabal b/eliminators.cabal
new file mode 100644
--- /dev/null
+++ b/eliminators.cabal
@@ -0,0 +1,49 @@
+name:                eliminators
+version:             0.1
+synopsis:            Dependently typed elimination functions using singletons
+description:         This library provides eliminators for inductive data types,
+                     leveraging the power of the @singletons@ library to allow
+                     dependently typed elimination.
+homepage:            https://github.com/RyanGlScott/eliminators
+bug-reports:         https://github.com/RyanGlScott/eliminators/issues
+license:             BSD3
+license-file:        LICENSE
+author:              Ryan Scott
+maintainer:          Ryan Scott <ryan.gl.scott@gmail.com>
+stability:           Experimental
+copyright:           (C) 2017 Ryan Scott
+category:            Dependent Types
+build-type:          Simple
+extra-source-files:  CHANGELOG.md, README.md
+cabal-version:       >=1.10
+tested-with:         GHC == 8.2.1
+
+source-repository head
+  type:                git
+  location:            https://github.com/RyanGlScott/eliminators
+
+library
+  exposed-modules:     Data.Eliminator
+  build-depends:       base       >= 4.10 && < 4.11
+                     , singletons >= 2.3  && < 2.4
+  hs-source-dirs:      src
+  default-language:    Haskell2010
+  ghc-options:         -Wall -Wno-unticked-promoted-constructors
+
+test-suite spec
+  type:                exitcode-stdio-1.0
+  main-is:             Spec.hs
+  other-modules:       EqualitySpec
+                       GADTSpec
+                       ListSpec
+                       ListTypes
+                       PeanoSpec
+                       PeanoTypes
+                       VecSpec
+  build-depends:       base       >= 4.10 && < 4.11
+                     , eliminators
+                     , hspec      >= 2    && < 3
+                     , singletons >= 2.3  && < 2.4
+  hs-source-dirs:      tests
+  default-language:    Haskell2010
+  ghc-options:         -Wall -Wno-unticked-promoted-constructors -threaded -rtsopts
diff --git a/src/Data/Eliminator.hs b/src/Data/Eliminator.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Eliminator.hs
@@ -0,0 +1,510 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-|
+Module:      Data.Eliminator
+Copyright:   (C) 2017 Ryan Scott
+License:     BSD-style (see the file LICENSE)
+Maintainer:  Ryan Scott
+Stability:   Experimental
+Portability: GHC
+
+Dependently typed elimination functions using @singletons@.
+-}
+module Data.Eliminator (
+    -- * Eliminator functions
+    -- ** Eliminators using '(->)'
+    -- $eliminators
+    elimBool
+  , elimEither
+  , elimList
+  , elimMaybe
+  , elimNat
+  , elimNonEmpty
+  , elimOrdering
+  , elimTuple0
+  , elimTuple2
+  , elimTuple3
+  , elimTuple4
+  , elimTuple5
+  , elimTuple6
+  , elimTuple7
+
+    -- ** Eliminators using '(~>)'
+    -- $eliminators-TyFun
+  , elimBoolTyFun
+  , elimEitherTyFun
+  , elimListTyFun
+  , elimMaybeTyFun
+  , elimNatTyFun
+  , elimNonEmptyTyFun
+  , elimOrderingTyFun
+  , elimTuple0TyFun
+  , elimTuple2TyFun
+  , elimTuple3TyFun
+  , elimTuple4TyFun
+  , elimTuple5TyFun
+  , elimTuple6TyFun
+  , elimTuple7TyFun
+
+    -- ** Arrow-polymorphic eliminators (very experimental)
+    -- $eliminators-Poly
+  , FunArrow(..)
+  , FunType(..)
+  , type (-?>)
+  , AppType(..)
+  , FunApp
+
+  , elimBoolPoly
+  , elimEitherPoly
+  , elimListPoly
+  , elimMaybePoly
+  , elimNonEmptyPoly
+  , elimNatPoly
+  , elimOrderingPoly
+  , elimTuple0Poly
+  , elimTuple2Poly
+  , elimTuple3Poly
+  , elimTuple4Poly
+  , elimTuple5Poly
+  , elimTuple6Poly
+  , elimTuple7Poly
+  ) where
+
+import Data.Kind (Type)
+import Data.List.NonEmpty (NonEmpty(..))
+import Data.Singletons.Prelude
+import Data.Singletons.Prelude.List.NonEmpty (Sing(..))
+import Data.Singletons.TypeLits
+
+import Unsafe.Coerce (unsafeCoerce)
+
+{- $eliminators
+
+These eliminators are defined with propositions of kind @\<Datatype\> -> 'Type'@
+(that is, using the '(->)' kind). As a result, these eliminators' type signatures
+are the most readable in this library, and most closely resemble eliminator functions
+in other dependently typed languages.
+-}
+
+elimBool :: forall (p :: Bool -> Type) (b :: Bool).
+            Sing b
+         -> p False
+         -> p True
+         -> p b
+elimBool = elimBoolPoly @(:->)
+
+elimEither :: forall (a :: Type) (b :: Type) (p :: Either a b -> Type) (e :: Either a b).
+              Sing e
+           -> (forall (l :: a). Sing l -> p (Left  l))
+           -> (forall (r :: b). Sing r -> p (Right r))
+           -> p e
+elimEither = elimEitherPoly @(:->)
+
+elimList :: forall (a :: Type) (p :: [a] -> Type) (l :: [a]).
+            Sing l
+         -> p '[]
+         -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p xs -> p (x:xs))
+         -> p l
+elimList = elimListPoly @(:->)
+
+elimMaybe :: forall (a :: Type) (p :: Maybe a -> Type) (m :: Maybe a).
+             Sing m
+          -> p Nothing
+          -> (forall (x :: a). Sing x -> p (Just x))
+          -> p m
+elimMaybe = elimMaybePoly @(:->)
+
+elimNat :: forall (p :: Nat -> Type) (n :: Nat).
+           Sing n
+        -> p 0
+        -> (forall (k :: Nat). Sing k -> p k -> p (k :+ 1))
+        -> p n
+elimNat = elimNatPoly @(:->)
+
+elimNonEmpty :: forall (a :: Type) (p :: NonEmpty a -> Type) (n :: NonEmpty a).
+                Sing n
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p (x :| xs))
+             -> p n
+elimNonEmpty = elimNonEmptyPoly @(:->)
+
+elimOrdering :: forall (p :: Ordering -> Type) (o :: Ordering).
+                Sing o
+             -> p LT
+             -> p EQ
+             -> p GT
+             -> p o
+elimOrdering = elimOrderingPoly @(:->)
+
+elimTuple0 :: forall (p :: () -> Type) (u :: ()).
+              Sing u
+           -> p '()
+           -> p u
+elimTuple0 = elimTuple0Poly @(:->)
+
+elimTuple2 :: forall (a :: Type) (b :: Type)
+                     (p :: (a, b) -> Type) (t :: (a, b)).
+              Sing t
+           -> (forall (aa :: a) (bb :: b).
+                      Sing aa -> Sing bb
+                   -> p '(aa, bb))
+           -> p t
+elimTuple2 = elimTuple2Poly @(:->)
+
+elimTuple3 :: forall (a :: Type) (b :: Type) (c :: Type)
+                     (p :: (a, b, c) -> Type) (t :: (a, b, c)).
+              Sing t
+           -> (forall (aa :: a) (bb :: b) (cc :: c).
+                      Sing aa -> Sing bb -> Sing cc
+                   -> p '(aa, bb, cc))
+           -> p t
+elimTuple3 = elimTuple3Poly @(:->)
+
+elimTuple4 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type)
+                     (p :: (a, b, c, d) -> Type) (t :: (a, b, c, d)).
+              Sing t
+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d).
+                      Sing aa -> Sing bb -> Sing cc -> Sing dd
+                   -> p '(aa, bb, cc, dd))
+           -> p t
+elimTuple4 = elimTuple4Poly @(:->)
+
+elimTuple5 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type)
+                     (p :: (a, b, c, d, e) -> Type) (t :: (a, b, c, d, e)).
+              Sing t
+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e).
+                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee
+                   -> p '(aa, bb, cc, dd, ee))
+           -> p t
+elimTuple5 = elimTuple5Poly @(:->)
+
+elimTuple6 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type)
+                     (p :: (a, b, c, d, e, f) -> Type) (t :: (a, b, c, d, e, f)).
+              Sing t
+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f).
+                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff
+                   -> p '(aa, bb, cc, dd, ee, ff))
+           -> p t
+elimTuple6 = elimTuple6Poly @(:->)
+
+elimTuple7 :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type)
+                     (p :: (a, b, c, d, e, f, g) -> Type) (t :: (a, b, c, d, e, f, g)).
+              Sing t
+           -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g).
+                      Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg
+                   -> p '(aa, bb, cc, dd, ee, ff, gg))
+           -> p t
+elimTuple7 = elimTuple7Poly @(:->)
+
+{- $eliminators-TyFun
+
+These eliminators are defined with propositions of kind @\<Datatype\> ~> 'Type'@
+(that is, using the '(~>)' kind). These eliminators are designed for
+defunctionalized (i.e., \"partially applied\") type families as predicates,
+and as a result, the predicates must be applied manually with '(@@)'.
+-}
+
+elimBoolTyFun :: forall (p :: Bool ~> Type) (b :: Bool).
+                 Sing b
+              -> p @@ False
+              -> p @@ True
+              -> p @@ b
+elimBoolTyFun = elimBoolPoly @(:~>) @p
+
+elimEitherTyFun :: forall (a :: Type) (b :: Type) (p :: Either a b ~> Type) (e :: Either a b).
+                   Sing e
+                -> (forall (l :: a). Sing l -> p @@ (Left  l))
+                -> (forall (r :: b). Sing r -> p @@ (Right r))
+                -> p @@ e
+elimEitherTyFun = elimEitherPoly @(:~>) @_ @_ @p
+
+elimListTyFun :: forall (a :: Type) (p :: [a] ~> Type) (l :: [a]).
+                 Sing l
+              -> p @@ '[]
+              -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ xs -> p @@ (x:xs))
+              -> p @@ l
+elimListTyFun = elimListPoly @(:~>) @_ @p
+
+elimMaybeTyFun :: forall (a :: Type) (p :: Maybe a ~> Type) (m :: Maybe a).
+                  Sing m
+               -> p @@ Nothing
+               -> (forall (x :: a). Sing x -> p @@ (Just x))
+               -> p @@ m
+elimMaybeTyFun = elimMaybePoly @(:~>) @_ @p
+
+elimNatTyFun :: forall (p :: Nat ~> Type) (n :: Nat).
+                Sing n
+             -> p @@ 0
+             -> (forall (k :: Nat). Sing k -> p @@ k -> p @@ (k :+ 1))
+             -> p @@ n
+elimNatTyFun = elimNatPoly @(:~>) @p
+
+elimNonEmptyTyFun :: forall (a :: Type) (p :: NonEmpty a ~> Type) (n :: NonEmpty a).
+                     Sing n
+                  -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> p @@ (x :| xs))
+                  -> p @@ n
+elimNonEmptyTyFun = elimNonEmptyPoly @(:~>) @_ @p
+
+elimOrderingTyFun :: forall (p :: Ordering ~> Type) (o :: Ordering).
+                     Sing o
+                  -> p @@ LT
+                  -> p @@ EQ
+                  -> p @@ GT
+                  -> p @@ o
+elimOrderingTyFun = elimOrderingPoly @(:~>) @p
+
+elimTuple0TyFun :: forall (p :: () ~> Type) (u :: ()).
+                   Sing u
+                -> p @@ '()
+                -> p @@ u
+elimTuple0TyFun = elimTuple0Poly @(:~>) @p
+
+elimTuple2TyFun :: forall (a :: Type) (b :: Type)
+                          (p :: (a, b) ~> Type) (t :: (a, b)).
+                   Sing t
+                -> (forall (aa :: a) (bb :: b).
+                           Sing aa -> Sing bb
+                        -> p @@ '(aa, bb))
+                -> p @@ t
+elimTuple2TyFun = elimTuple2Poly @(:~>) @_ @_ @p
+
+elimTuple3TyFun :: forall (a :: Type) (b :: Type) (c :: Type)
+                          (p :: (a, b, c) ~> Type) (t :: (a, b, c)).
+                   Sing t
+                -> (forall (aa :: a) (bb :: b) (cc :: c).
+                           Sing aa -> Sing bb -> Sing cc
+                        -> p @@ '(aa, bb, cc))
+                -> p @@ t
+elimTuple3TyFun = elimTuple3Poly @(:~>) @_ @_ @_ @p
+
+elimTuple4TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type)
+                          (p :: (a, b, c, d) ~> Type) (t :: (a, b, c, d)).
+                   Sing t
+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d).
+                           Sing aa -> Sing bb -> Sing cc -> Sing dd
+                        -> p @@ '(aa, bb, cc, dd))
+                -> p @@ t
+elimTuple4TyFun = elimTuple4Poly @(:~>) @_ @_ @_ @_ @p
+
+elimTuple5TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type)
+                          (p :: (a, b, c, d, e) ~> Type) (t :: (a, b, c, d, e)).
+                   Sing t
+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e).
+                           Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee
+                        -> p @@ '(aa, bb, cc, dd, ee))
+                -> p @@ t
+elimTuple5TyFun = elimTuple5Poly @(:~>) @_ @_ @_ @_ @_ @p
+
+elimTuple6TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type)
+                          (p :: (a, b, c, d, e, f) ~> Type) (t :: (a, b, c, d, e, f)).
+                   Sing t
+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f).
+                           Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff
+                        -> p @@ '(aa, bb, cc, dd, ee, ff))
+                -> p @@ t
+elimTuple6TyFun = elimTuple6Poly @(:~>) @_ @_ @_ @_ @_ @_ @p
+
+elimTuple7TyFun :: forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type)
+                          (p :: (a, b, c, d, e, f, g) ~> Type) (t :: (a, b, c, d, e, f, g)).
+                   Sing t
+                -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g).
+                           Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg
+                        -> p @@ '(aa, bb, cc, dd, ee, ff, gg))
+                -> p @@ t
+elimTuple7TyFun = elimTuple7Poly @(:~>) @_ @_ @_ @_ @_ @_ @_ @p
+
+{- $eliminators-Poly
+
+Eliminators using '(->)' and eliminators using '(~>)' end up having very similar
+implementations - so similar, in fact, that they can be generalized to be polymorphic
+over the arrow kind used (as well as the application operator). The 'FunType' and
+'AppType' classes capture these notions of abstraction and application, respectively.
+
+Not all eliminators are known to work under this generalized scheme yet (for
+instance, eliminators for GADTs).
+
+Chances are, you won't want to use these eliminators directly, since their type
+signatures are pretty horrific and don't always play well with type inference.
+However, they are provided for the sake of completeness.
+-}
+
+-- | An enumeration which represents the possible choices of arrow kind for
+-- eliminator functions.
+data FunArrow = (:->) -- ^ '(->)'
+              | (:~>) -- ^ '(~>)'
+
+-- | Things which have arrow kinds.
+class FunType (arr :: FunArrow) where
+  -- | An arrow kind.
+  type Fun (k1 :: Type) arr (k2 :: Type) :: Type
+
+-- | Things which can be applied.
+class FunType arr => AppType (arr :: FunArrow) where
+  -- | An application of a 'Fun' to an argument.
+  --
+  -- Note that this can't be defined in the same class as 'Fun' due to GHC
+  -- restrictions on associated type families.
+  type App k1 arr k2 (f :: Fun k1 arr k2) (x :: k1) :: k2
+
+-- | Something which has both a 'Fun' and an 'App'.
+type FunApp arr = (FunType arr, AppType arr)
+
+instance FunType (:->) where
+  type Fun k1 (:->) k2 = k1 -> k2
+
+instance AppType (:->) where
+  type App k1 (:->) k2 (f :: k1 -> k2) x = f x
+
+instance FunType (:~>) where
+  type Fun k1 (:~>) k2 = k1 ~> k2
+
+instance AppType (:~>) where
+  type App k1 (:~>) k2 (f :: k1 ~> k2) x = f @@ x
+
+-- | An infix synonym for 'Fun'.
+infixr 0 -?>
+type (-?>) (k1 :: Type) (k2 :: Type) (arr :: FunArrow) = Fun k1 arr k2
+
+-- Note: it would be nice to have an infix synonym for 'App' as well, but
+-- the order in which the type variable dependencies occur makes this awkward
+-- to achieve.
+
+elimBoolPoly :: forall (arr :: FunArrow) (p :: (Bool -?> Type) arr) (b :: Bool).
+                FunApp arr
+             => Sing b
+             -> App Bool arr Type p False
+             -> App Bool arr Type p True
+             -> App Bool arr Type p b
+elimBoolPoly SFalse pF _  = pF
+elimBoolPoly STrue  _  pT = pT
+
+elimEitherPoly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (p :: (Either a b -?> Type) arr) (e :: Either a b).
+                  FunApp arr
+               => Sing e
+               -> (forall (l :: a). Sing l -> App (Either a b) arr Type p (Left  l))
+               -> (forall (r :: b). Sing r -> App (Either a b) arr Type p (Right r))
+               -> App (Either a b) arr Type p e
+elimEitherPoly (SLeft  sl) pLeft _  = pLeft  sl
+elimEitherPoly (SRight sr) _ pRight = pRight sr
+
+elimListPoly :: forall (arr :: FunArrow) (a :: Type) (p :: ([a] -?> Type) arr) (l :: [a]).
+                FunApp arr
+             => Sing l
+             -> App [a] arr Type p '[]
+             -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App [a] arr Type p xs -> App [a] arr Type p (x:xs))
+             -> App [a] arr Type p l
+elimListPoly SNil                      pNil _     = pNil
+elimListPoly (SCons x (xs :: Sing xs)) pNil pCons = pCons x xs (elimListPoly @arr @a @p @xs xs pNil pCons)
+
+elimMaybePoly :: forall (arr :: FunArrow) (a :: Type) (p :: (Maybe a -?> Type) arr) (m :: Maybe a).
+                 FunApp arr
+              => Sing m
+              -> App (Maybe a) arr Type p Nothing
+              -> (forall (x :: a). Sing x -> App (Maybe a) arr Type p (Just x))
+              -> App (Maybe a) arr Type p m
+elimMaybePoly SNothing pNothing _ = pNothing
+elimMaybePoly (SJust sx) _ pJust  = pJust sx
+
+elimNatPoly :: forall (arr :: FunArrow) (p :: (Nat -?> Type) arr) (n :: Nat).
+               FunApp arr
+            => Sing n
+            -> App Nat arr Type p 0
+            -> (forall (k :: Nat). Sing k -> App Nat arr Type p k -> App Nat arr Type p (k :+ 1))
+            -> App Nat arr Type p n
+elimNatPoly snat pZ pS =
+  case fromSing snat of
+    0        -> unsafeCoerce pZ
+    nPlusOne -> case toSing (pred nPlusOne) of
+                  SomeSing (sn :: Sing k) -> unsafeCoerce (pS sn (elimNatPoly @arr @p @k sn pZ pS))
+
+elimNonEmptyPoly :: forall (arr :: FunArrow) (a :: Type) (p :: (NonEmpty a -?> Type) arr) (n :: NonEmpty a).
+                    FunApp arr
+                 => Sing n
+                 -> (forall (x :: a) (xs :: [a]). Sing x -> Sing xs -> App (NonEmpty a) arr Type p (x :| xs))
+                 -> App (NonEmpty a) arr Type p n
+elimNonEmptyPoly (sx :%| sxs) pNECons = pNECons sx sxs
+
+elimOrderingPoly :: forall (arr :: FunArrow) (p :: (Ordering -?> Type) arr) (o :: Ordering).
+                    Sing o
+                 -> App Ordering arr Type p LT
+                 -> App Ordering arr Type p EQ
+                 -> App Ordering arr Type p GT
+                 -> App Ordering arr Type p o
+elimOrderingPoly SLT pLT _   _   = pLT
+elimOrderingPoly SEQ _   pEQ _   = pEQ
+elimOrderingPoly SGT _   _   pGT = pGT
+
+elimTuple0Poly :: forall (arr :: FunArrow) (p :: (() -?> Type) arr) (u :: ()).
+                  FunApp arr
+               => Sing u
+               -> App () arr Type p '()
+               -> App () arr Type p u
+elimTuple0Poly STuple0 pTuple0 = pTuple0
+
+elimTuple2Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type)
+                         (p :: ((a, b) -?> Type) arr) (t :: (a, b)).
+                  FunApp arr
+               => Sing t
+               -> (forall (aa :: a) (bb :: b).
+                          Sing aa -> Sing bb
+                       -> App (a, b) arr Type p '(aa, bb))
+               -> App (a, b) arr Type p t
+elimTuple2Poly (STuple2 sa sb) pTuple2 = pTuple2 sa sb
+
+elimTuple3Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type)
+                         (p :: ((a, b, c) -?> Type) arr) (t :: (a, b, c)).
+                  FunApp arr
+               => Sing t
+               -> (forall (aa :: a) (bb :: b) (cc :: c).
+                          Sing aa -> Sing bb -> Sing cc
+                       -> App (a, b, c) arr Type p '(aa, bb, cc))
+               -> App (a, b, c) arr Type p t
+elimTuple3Poly (STuple3 sa sb sc) pTuple3 = pTuple3 sa sb sc
+
+elimTuple4Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type)
+                         (p :: ((a, b, c, d) -?> Type) arr) (t :: (a, b, c, d)).
+                  FunApp arr
+               => Sing t
+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d).
+                          Sing aa -> Sing bb -> Sing cc -> Sing dd
+                       -> App (a, b, c, d) arr Type p '(aa, bb, cc, dd))
+               -> App (a, b, c, d) arr Type p t
+elimTuple4Poly (STuple4 sa sb sc sd) pTuple4 = pTuple4 sa sb sc sd
+
+elimTuple5Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type)
+                         (p :: ((a, b, c, d, e) -?> Type) arr) (t :: (a, b, c, d, e)).
+                  FunApp arr
+               => Sing t
+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e).
+                          Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee
+                       -> App (a, b, c, d, e) arr Type p '(aa, bb, cc, dd, ee))
+               -> App (a, b, c, d, e) arr Type p t
+elimTuple5Poly (STuple5 sa sb sc sd se) pTuple5 = pTuple5 sa sb sc sd se
+
+elimTuple6Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type)
+                         (p :: ((a, b, c, d, e, f) -?> Type) arr) (t :: (a, b, c, d, e, f)).
+                  FunApp arr
+               => Sing t
+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f).
+                          Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff
+                       -> App (a, b, c, d, e, f) arr Type p '(aa, bb, cc, dd, ee, ff))
+               -> App (a, b, c, d, e, f) arr Type p t
+elimTuple6Poly (STuple6 sa sb sc sd se sf) pTuple6 = pTuple6 sa sb sc sd se sf
+
+elimTuple7Poly :: forall (arr :: FunArrow) (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type) (f :: Type) (g :: Type)
+                         (p :: ((a, b, c, d, e, f, g) -?> Type) arr) (t :: (a, b, c, d, e, f, g)).
+                  FunApp arr
+               => Sing t
+               -> (forall (aa :: a) (bb :: b) (cc :: c) (dd :: d) (ee :: e) (ff :: f) (gg :: g).
+                          Sing aa -> Sing bb -> Sing cc -> Sing dd -> Sing ee -> Sing ff -> Sing gg
+                       -> App (a, b, c, d, e, f, g) arr Type p '(aa, bb, cc, dd, ee, ff, gg))
+               -> App (a, b, c, d, e, f, g) arr Type p t
+elimTuple7Poly (STuple7 sa sb sc sd se sf sg) pTuple7 = pTuple7 sa sb sc sd se sf sg
diff --git a/tests/EqualitySpec.hs b/tests/EqualitySpec.hs
new file mode 100644
--- /dev/null
+++ b/tests/EqualitySpec.hs
@@ -0,0 +1,198 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+module EqualitySpec where
+
+import           Data.Eliminator
+import           Data.Kind
+import           Data.Singletons
+import qualified Data.Type.Equality as DTE
+import           Data.Type.Equality ((:~:)(..), (:~~:)(..))
+
+import           Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = parallel $ do
+  describe "sym" $
+    it "behaves like the one from Data.Type.Equality" $ do
+      let boolEq :: Bool :~: Bool
+          boolEq = Refl
+      sym boolEq       `shouldBe` DTE.sym boolEq
+      sym (sym boolEq) `shouldBe` DTE.sym (DTE.sym boolEq)
+
+-----
+
+data instance Sing (z :: a :~: b) where
+  SRefl :: Sing Refl
+
+instance SingKind (a :~: b) where
+  type Demote (a :~: b) = a :~: b
+  fromSing SRefl = Refl
+  toSing Refl    = SomeSing SRefl
+
+instance SingI Refl where
+  sing = SRefl
+
+(->:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y -> Type).
+           Sing r
+        -> p Refl
+        -> p r
+(->:~:) SRefl pRefl = pRefl
+
+(~>:~:) :: forall (k :: Type) (a :: k) (b :: k) (r :: a :~: b) (p :: forall (y :: k). a :~: y ~> Type).
+           Sing r
+        -> p @@ Refl
+        -> p @@ r
+(~>:~:) SRefl pRefl = pRefl
+
+-- (-?>:~:)
+
+data instance Sing (z :: a :~~: b) where
+  SHRefl :: Sing HRefl
+
+instance SingKind (a :~~: b) where
+  type Demote (a :~~: b) = a :~~: b
+  fromSing SHRefl = HRefl
+  toSing HRefl    = SomeSing SHRefl
+
+instance SingI HRefl where
+  sing = SHRefl
+
+(->:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y -> Type).
+            Sing r
+         -> p HRefl
+         -> p r
+(->:~~:) SHRefl pHRefl = pHRefl
+
+{-
+This doesn't typecheck at the moment due to GHC Trac #13879.
+TODO: Uncomment this when the fix becomes available.
+
+(~>:~~:) :: forall (j :: Type) (k :: Type) (a :: j) (b :: k) (r :: a :~~: b) (p :: forall (z :: Type) (y :: z). a :~~: y ~> Type).
+            Sing r
+         -> p @@ HRefl
+         -> p @@ r
+(~>:~~:) SHRefl pHRefl = pHRefl
+-}
+
+-- (-?>:~~:)
+
+-----
+
+type WhySym (a :: t) (y :: t) (e :: a :~: y) = y :~: a
+data WhySymSym (a :: t) :: forall (y :: t). a :~: y ~> Type
+type instance Apply (WhySymSym z :: z :~: y ~> Type) x
+  = WhySym z y x
+
+sym :: forall (t :: Type) (a :: t) (b :: t).
+       a :~: b -> b :~: a
+sym eq = withSomeSing eq $ \(singEq :: Sing r) ->
+           (~>:~:) @t @a @b @r @(WhySymSym a) singEq Refl
+
+type family Symmetry (x :: (a :: k) :~: (b :: k)) :: b :~: a where
+  Symmetry Refl = Refl
+
+type WhySymIdempotent (a :: t) (z :: t) (r :: a :~: z)
+  = Symmetry (Symmetry r) :~: r
+data WhySymIdempotentSym (a :: t) :: forall (z :: t). a :~: z ~> Type
+type instance Apply (WhySymIdempotentSym a :: a :~: z ~> Type) r
+  = WhySymIdempotent a z r
+
+symIdempotent :: forall (t :: Type) (a :: t) (b :: t)
+                        (e :: a :~: b).
+                 Sing e -> Symmetry (Symmetry e) :~: e
+symIdempotent se = (~>:~:) @t @a @b @e @(WhySymIdempotentSym a) se Refl
+
+type WhyReplacePoly (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
+                    (y :: t) (e :: from :~: y) = App t arr Type p y
+data WhyReplacePolySym (arr :: FunArrow) (from :: t) (p :: (t -?> Type) arr)
+  :: forall (y :: t). from :~: y ~> Type
+type instance Apply (WhyReplacePolySym arr from p :: from :~: y ~> Type) x
+  = WhyReplacePoly arr from p y x
+
+replace :: forall (t :: Type) (from :: t) (to :: t) (p :: t -> Type).
+           p from
+        -> from :~: to
+        -> p to
+replace = replacePoly @(:->)
+
+replaceTyFun :: forall (t :: Type) (from :: t) (to :: t) (p :: t ~> Type).
+                p @@ from
+             -> from :~: to
+             -> p @@ to
+replaceTyFun = replacePoly @(:~>) @_ @_ @_ @p
+
+replacePoly :: forall (arr :: FunArrow) (t :: Type) (from :: t) (to :: t)
+                      (p :: (t -?> Type) arr).
+               FunApp arr
+            => App t arr Type p from
+            -> from :~: to
+            -> App t arr Type p to
+replacePoly from eq =
+  withSomeSing eq $ \(singEq :: Sing r) ->
+    (~>:~:) @t @from @to @r @(WhyReplacePolySym arr from p) singEq from
+
+type WhyLeibnizPoly (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t) (z :: t)
+  = App t arr Type f a -> App t arr Type f z
+data WhyLeibnizPolySym (arr :: FunArrow) (f :: (t -?> Type) arr) (a :: t)
+  :: t ~> Type
+type instance Apply (WhyLeibnizPolySym arr f a) z = WhyLeibnizPoly arr f a z
+
+leibniz :: forall (t :: Type) (f :: t -> Type) (a :: t) (b :: t).
+           a :~: b
+        -> f a
+        -> f b
+leibniz = leibnizPoly @(:->)
+
+leibnizTyFun :: forall (t :: Type) (f :: t ~> Type) (a :: t) (b :: t).
+                a :~: b
+             -> f @@ a
+             -> f @@ b
+leibnizTyFun = leibnizPoly @(:~>) @_ @f
+
+leibnizPoly :: forall (arr :: FunArrow) (t :: Type) (f :: (t -?> Type) arr)
+                      (a :: t) (b :: t).
+               FunApp arr
+            => a :~: b
+            -> App t arr Type f a
+            -> App t arr Type f b
+leibnizPoly = replaceTyFun @t @a @b @(WhyLeibnizPolySym arr f a) id
+
+type WhyCongPoly (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)
+                 (a :: x) (z :: x) (e :: a :~: z)
+  = App x arr y f a :~: App x arr y f z
+data WhyCongPolySym (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)
+                    (a :: x) :: forall (z :: x). a :~: z ~> Type
+type instance Apply (WhyCongPolySym arr x y f a :: a :~: z ~> Type) asdf
+  = WhyCongPoly arr x y f a z asdf
+
+cong :: forall (x :: Type) (y :: Type) (f :: x -> y)
+               (a :: x) (b :: x).
+        a :~: b
+     -> f a :~: f b
+cong = congPoly @(:->) @_ @_ @f
+
+congTyFun :: forall (x :: Type) (y :: Type) (f :: x ~> y)
+                    (a :: x) (b :: x).
+             a :~: b
+          -> f @@ a :~: f @@ b
+congTyFun = congPoly @(:~>) @_ @_ @f
+
+congPoly :: forall (arr :: FunArrow) (x :: Type) (y :: Type) (f :: (x -?> y) arr)
+                   (a :: x) (b :: x).
+            FunApp arr
+         => a :~: b
+         -> App x arr y f a :~: App x arr y f b
+congPoly eq =
+  withSomeSing eq $ \(singEq :: Sing r) ->
+    (~>:~:) @x @a @b @r @(WhyCongPolySym arr x y f a) singEq Refl
diff --git a/tests/GADTSpec.hs b/tests/GADTSpec.hs
new file mode 100644
--- /dev/null
+++ b/tests/GADTSpec.hs
@@ -0,0 +1,75 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module GADTSpec where
+
+import Data.Eliminator
+import Data.Kind
+import Data.Singletons
+
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = pure ()
+
+-----
+
+data So :: Bool -> Type where
+  Oh :: So True
+
+data instance Sing (z :: So what) where
+  SOh :: Sing Oh
+
+elimSo :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker -> Type).
+          Sing s
+       -> p Oh
+       -> p s
+elimSo SOh pOh = pOh
+
+elimSoTyFun :: forall (what :: Bool) (s :: So what) (p :: forall (long_sucker :: Bool). So long_sucker ~> Type).
+               Sing s
+            -> p @@ Oh
+            -> p @@ s
+elimSoTyFun SOh pOh = pOh
+
+{-
+I don't know how to make this kind-check :(
+elimSoPoly :: forall (arr :: FunArrow) (what :: Bool) (s :: So what)
+                     (p :: forall (long_sucker :: Bool). (So long_sucker -?> Type) arr).
+              Sing s
+           -> App (So True) arr Type p Oh
+           -> App (So what) arr Type p s
+elimSoPoly SOh pOh = pOh
+-}
+
+data Obj :: Type where
+  MkObj :: o -> Obj
+
+data instance Sing (z :: Obj) where
+  SMkObj :: forall (obj :: obiwan). Sing obj -> Sing (MkObj obj)
+
+elimObj :: forall (o :: Obj) (p :: Obj -> Type).
+           Sing o
+        -> (forall (obj :: Type) (x :: obj). Sing x -> p (MkObj x))
+        -> p o
+elimObj = elimObjPoly @(:->) @o @p
+
+elimObjTyFun :: forall (o :: Obj) (p :: Obj ~> Type).
+                Sing o
+             -> (forall (obj :: Type) (x :: obj). Sing x -> p @@ (MkObj x))
+             -> p @@ o
+elimObjTyFun = elimObjPoly @(:~>) @o @p
+
+elimObjPoly :: forall (arr :: FunArrow) (o :: Obj) (p :: (Obj -?> Type) arr).
+               Sing o
+            -> (forall (obj :: Type) (x :: obj). Sing x -> App Obj arr Type p (MkObj x))
+            -> App Obj arr Type p o
+elimObjPoly (SMkObj (x :: Sing (obj :: obiwan))) pMkObj = pMkObj @obiwan @obj x
diff --git a/tests/ListSpec.hs b/tests/ListSpec.hs
new file mode 100644
--- /dev/null
+++ b/tests/ListSpec.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+module ListSpec where
+
+import Data.Eliminator
+import Data.Kind
+import Data.Singletons.Prelude
+import Data.Singletons.Prelude.List
+import Data.Type.Equality
+
+import EqualitySpec (congTyFun)
+
+import ListTypes
+
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = pure ()
+
+-----
+
+mapPreservesLength :: forall (x :: Type) (y :: Type) (f :: x ~> y) (l :: [x]).
+                      SingI l
+                   => Length l :~: Length (Map f l)
+mapPreservesLength
+  = elimListTyFun @x @(WhyMapPreservesLengthSym1 f) @l (sing @_ @l) base step
+  where
+    base :: WhyMapPreservesLength f '[]
+    base = Refl
+
+    step :: forall (s :: x) (ss :: [x]).
+            Sing s -> Sing ss
+         -> WhyMapPreservesLength f ss
+         -> WhyMapPreservesLength f (s:ss)
+    step _ _ = congTyFun @_ @_ @((:+$$) 1)
+
+mapFusion :: forall (x :: Type) (y :: Type) (z :: Type)
+                    (f :: y ~> z) (g :: x ~> y) (l :: [x]).
+                    SingI l
+                 => Map f (Map g l) :~: Map (f :.$$$ g) l
+mapFusion
+  = elimListTyFun @x @(WhyMapFusionSym2 f g) @l (sing @_ @l) base step
+  where
+    base :: WhyMapFusion f g '[]
+    base = Refl
+
+    step :: forall (s :: x) (ss :: [x]).
+            Sing s -> Sing ss
+         -> WhyMapFusion f g ss
+         -> WhyMapFusion f g (s:ss)
+    step _ _ = congTyFun @_ @_ @((:$$) (f @@ (g @@ s)))
diff --git a/tests/ListTypes.hs b/tests/ListTypes.hs
new file mode 100644
--- /dev/null
+++ b/tests/ListTypes.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module ListTypes where
+
+import Data.Singletons.Prelude
+import Data.Singletons.Prelude.List
+import Data.Singletons.TH
+
+type WhyMapPreservesLength (f :: x ~> y) (l :: [x])
+  = Length l :~: Length (Map f l)
+$(genDefunSymbols [''WhyMapPreservesLength])
+
+type WhyMapFusion (f :: y ~> z) (g :: x ~> y) (l :: [x])
+  = Map f (Map g l) :~: Map (f :.$$$ g) l
+$(genDefunSymbols [''WhyMapFusion])
diff --git a/tests/PeanoSpec.hs b/tests/PeanoSpec.hs
new file mode 100644
--- /dev/null
+++ b/tests/PeanoSpec.hs
@@ -0,0 +1,116 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeInType #-}
+module PeanoSpec where
+
+import Data.Kind
+import Data.Singletons
+
+import PeanoTypes
+
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = parallel $ do
+  describe "replicateVec" $ do
+    it "works with empty lists" $
+      replicateVec SZ () `shouldBe` VNil
+    it "works with non-empty lists" $
+      replicateVec (SS SZ) () `shouldBe` VCons () VNil
+  describe "mapVec" $ do
+    it "maps over a Vec" $ do
+      mapVec reverse ("hello" `VCons` "world" `VCons` VNil)
+        `shouldBe` ("olleh" `VCons` "dlrow" `VCons` VNil)
+  describe "zipWithVec" $ do
+    it "zips two Vecs" $ do
+      zipWithVec (,) ((2 :: Int) `VCons` 22 `VCons` VNil)
+                     ("chicken-of-the-woods" `VCons` "hen-of-woods" `VCons` VNil)
+        `shouldBe` ((2, "chicken-of-the-woods") `VCons` (22, "hen-of-woods")
+                                                `VCons` VNil)
+  describe "appendVec" $ do
+    it "appends two Vecs" $ do
+      appendVec ("portabello" `VCons` "bay-bolete"
+                              `VCons` "funnel-chantrelle"
+                              `VCons` VNil)
+                ("sheathed-woodtuft" `VCons` "puffball" `VCons` VNil)
+        `shouldBe` ("portabello" `VCons` "bay-bolete"
+                                 `VCons` "funnel-chantrelle"
+                                 `VCons` "sheathed-woodtuft"
+                                 `VCons` "puffball"
+                                 `VCons` VNil)
+  describe "transposeVec" $ do
+    it "transposes a Vec" $ do
+      transposeVec (('a' `VCons` 'b' `VCons` 'c' `VCons` VNil)
+            `VCons` ('d' `VCons` 'e' `VCons` 'f' `VCons` VNil)
+            `VCons` VNil)
+        `shouldBe`
+                   (('a' `VCons` 'd' `VCons` VNil)
+            `VCons` ('b' `VCons` 'e' `VCons` VNil)
+            `VCons` ('c' `VCons` 'f' `VCons` VNil)
+            `VCons` VNil)
+
+-----
+
+replicateVec :: forall (e :: Type) (howMany :: Peano).
+                Sing howMany -> e -> Vec e howMany
+replicateVec s e = elimPeano @howMany @(Vec e) s VNil step
+  where
+    step :: forall (k :: Peano). Sing k -> Vec e k -> Vec e (S k)
+    step _ = VCons e
+
+mapVec :: forall (a :: Type) (b :: Type) (n :: Peano).
+          SingI n
+       => (a -> b) -> Vec a n -> Vec b n
+mapVec f = elimPeanoTyFun @n @(WhyMapVecSym2 a b) (sing @_ @n) base step
+  where
+    base :: WhyMapVec a b Z
+    base _ = VNil
+
+    step :: forall (k :: Peano). Sing k -> WhyMapVec a b k -> WhyMapVec a b (S k)
+    step _ mapK vK = VCons (f (vhead vK)) (mapK (vtail vK))
+
+zipWithVec :: forall (a :: Type) (b :: Type) (c :: Type) (n :: Peano).
+              SingI n
+           => (a -> b -> c) -> Vec a n -> Vec b n -> Vec c n
+zipWithVec f = elimPeanoTyFun @n @(WhyZipWithVecSym3 a b c) (sing @_ @n) base step
+  where
+    base :: WhyZipWithVec a b c Z
+    base _ _ = VNil
+
+    step :: forall (k :: Peano).
+            Sing k
+         -> WhyZipWithVec a b c k
+         -> WhyZipWithVec a b c (S k)
+    step _ zwK vaK vbK = VCons (f   (vhead vaK) (vhead vbK))
+                               (zwK (vtail vaK) (vtail vbK))
+
+appendVec :: forall (e :: Type) (n :: Peano) (m :: Peano).
+             SingI n
+          => Vec e n -> Vec e m -> Vec e (Plus n m)
+appendVec = elimPeanoTyFun @n @(WhyAppendVecSym2 e m) (sing @_ @n) base step
+  where
+    base :: WhyAppendVec e m Z
+    base _ = id
+
+    step :: forall (k :: Peano).
+            Sing k
+         -> WhyAppendVec e m k
+         -> WhyAppendVec e m (S k)
+    step _ avK vK1 vK2 = VCons (vhead vK1) (avK (vtail vK1) vK2)
+
+transposeVec :: forall (e :: Type) (n :: Peano) (m :: Peano).
+                (SingI n, SingI m)
+             => Vec (Vec e m) n -> Vec (Vec e n) m
+transposeVec = elimPeanoTyFun @n @(WhyTransposeVecSym2 e m) (sing @_ @n) base step
+  where
+    base :: WhyTransposeVec e m Z
+    base _ = replicateVec (sing @_ @m) VNil
+
+    step :: forall (k :: Peano).
+            Sing k
+         -> WhyTransposeVec e m k
+         -> WhyTransposeVec e m (S k)
+    step _ transK vK = zipWithVec VCons (vhead vK) (transK (vtail vK))
diff --git a/tests/PeanoTypes.hs b/tests/PeanoTypes.hs
new file mode 100644
--- /dev/null
+++ b/tests/PeanoTypes.hs
@@ -0,0 +1,124 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module PeanoTypes where
+
+import Data.Eliminator
+import Data.Kind
+import Data.Singletons.TH
+
+$(singletons [d|
+  data Peano = Z | S Peano
+
+  plus :: Peano -> Peano -> Peano
+  plus Z     m = m
+  plus (S k) m = S (plus k m)
+
+  times :: Peano -> Peano -> Peano
+  times Z     _ = Z
+  times (S k) m = plus m (times k m)
+  |])
+
+elimPeano :: forall (n :: Peano) (p :: Peano -> Type).
+             Sing n
+          -> p Z
+          -> (forall (k :: Peano). Sing k -> p k -> p (S k))
+          -> p n
+elimPeano = elimPeanoPoly @(:->) @n @p
+
+elimPeanoTyFun :: forall (n :: Peano) (p :: Peano ~> Type).
+                  Sing n
+               -> p @@ Z
+               -> (forall (k :: Peano). Sing k -> p @@ k -> p @@ (S k))
+               -> p @@ n
+elimPeanoTyFun = elimPeanoPoly @(:~>) @n @p
+
+elimPeanoPoly :: forall (arr :: FunArrow) (n :: Peano) (p :: (Peano -?> Type) arr).
+                 FunApp arr
+              => Sing n
+              -> App Peano arr Type p Z
+              -> (forall (k :: Peano). Sing k -> App Peano arr Type p k
+                                              -> App Peano arr Type p (S k))
+              -> App Peano arr Type p n
+elimPeanoPoly SZ pZ _ = pZ
+elimPeanoPoly (SS (sk :: Sing k)) pZ pS = pS sk (elimPeanoPoly @arr @k @p sk pZ pS)
+
+data Vec a (n :: Peano) where
+  VNil  :: Vec a Z
+  VCons :: { vhead :: a, vtail :: Vec a n } -> Vec a (S n)
+infixr 5 `VCons`
+deriving instance Eq a   => Eq (Vec a n)
+deriving instance Ord a  => Ord (Vec a n)
+deriving instance Show a => Show (Vec a n)
+
+data instance Sing (z :: Vec a n) where
+  SVNil  :: Sing VNil
+  SVCons :: { sVhead :: Sing x, sVtail :: Sing xs } -> Sing (VCons x xs)
+
+instance SingKind a => SingKind (Vec a n) where
+  type Demote (Vec a n) = Vec (Demote a) n
+  fromSing SVNil         = VNil
+  fromSing (SVCons x xs) = VCons (fromSing x) (fromSing xs)
+  toSing VNil = SomeSing SVNil
+  toSing (VCons x xs) =
+    withSomeSing x $ \sx ->
+      withSomeSing xs $ \sxs ->
+        SomeSing $ SVCons sx sxs
+
+instance SingI VNil where
+  sing = SVNil
+
+instance (SingI x, SingI xs) => SingI (VCons x xs) where
+  sing = SVCons sing sing
+
+elimVec :: forall (a :: Type) (n :: Peano)
+                  (p :: forall (k :: Peano). Vec a k -> Type) (v :: Vec a n).
+           Sing v
+        -> p VNil
+        -> (forall (k :: Peano) (x :: a) (xs :: Vec a k).
+                   Sing x -> Sing xs -> p xs -> p (VCons x xs))
+        -> p v
+elimVec SVNil pVNil _ = pVNil
+elimVec (SVCons sx (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =
+  pVCons sx sxs (elimVec @a @k @p @xs sxs pVNil pVCons)
+
+elimVecTyFun :: forall (a :: Type) (n :: Peano)
+                       (p :: forall (k :: Peano). Vec a k ~> Type) (v :: Vec a n).
+                Sing v
+             -> p @@ VNil
+             -> (forall (k :: Peano) (x :: a) (xs :: Vec a k).
+                        Sing x -> Sing xs -> p @@ xs -> p @@ (VCons x xs))
+             -> p @@ v
+elimVecTyFun SVNil pVNil _ = pVNil
+elimVecTyFun (SVCons sx (sxs :: Sing (xs :: Vec a k))) pVNil pVCons =
+  pVCons sx sxs (elimVecTyFun @a @k @p @xs sxs pVNil pVCons)
+
+type WhyMapVec (a :: Type) (b :: Type) (n :: Peano) = Vec a n -> Vec b n
+$(genDefunSymbols [''WhyMapVec])
+
+type WhyZipWithVec (a :: Type) (b :: Type) (c :: Type) (n :: Peano)
+  = Vec a n -> Vec b n -> Vec c n
+$(genDefunSymbols [''WhyZipWithVec])
+
+type WhyAppendVec (e :: Type) (m :: Peano) (n :: Peano)
+  = Vec e n -> Vec e m -> Vec e (Plus n m)
+$(genDefunSymbols [''WhyAppendVec])
+
+type WhyTransposeVec (e :: Type) (m :: Peano) (n :: Peano)
+  = Vec (Vec e m) n -> Vec (Vec e n) m
+$(genDefunSymbols [''WhyTransposeVec])
+
+type WhyConcatVec (e :: Type) (j :: Peano) (n :: Peano) (l :: Vec (Vec e j) n)
+  = Vec e (Times n j)
+data WhyConcatVecSym (e :: Type) (j :: Peano)
+  :: forall (n :: Peano). Vec (Vec e j) n ~> Type
+type instance Apply (WhyConcatVecSym e j :: Vec (Vec e j) n ~> Type) l
+  = WhyConcatVec e j n l
diff --git a/tests/Spec.hs b/tests/Spec.hs
new file mode 100644
--- /dev/null
+++ b/tests/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
diff --git a/tests/VecSpec.hs b/tests/VecSpec.hs
new file mode 100644
--- /dev/null
+++ b/tests/VecSpec.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeInType #-}
+module VecSpec where
+
+import Data.Kind
+import Data.Singletons
+
+import PeanoSpec (appendVec)
+import PeanoTypes
+
+import Test.Hspec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = parallel $ do
+  describe "concatVec" $ do
+    it "concats a Vec of Vecs" $ do
+      concatVec ((False `VCons` True  `VCons` False `VCons` VNil)
+         `VCons` (True  `VCons` False `VCons` True  `VCons` VNil)
+         `VCons` VNil)
+        `shouldBe` (False `VCons` True  `VCons` False `VCons` True
+                          `VCons` False `VCons` True  `VCons` VNil)
+
+-----
+
+concatVec :: forall (e :: Type) (n :: Peano) (j :: Peano).
+             (SingKind e, SingI j, e ~ Demote e)
+          => Vec (Vec e j) n -> Vec e (Times n j)
+concatVec l = withSomeSing l $ \(singL :: Sing l) ->
+                elimVecTyFun @(Vec e j) @n @(WhyConcatVecSym e j) @l singL base step
+  where
+    base :: WhyConcatVec e j Z VNil
+    base = VNil
+
+    step :: forall (k :: Peano) (x :: Vec e j) (xs :: Vec (Vec e j) k).
+                   Sing x -> Sing xs
+                -> WhyConcatVec e j k     xs
+                -> WhyConcatVec e j (S k) (VCons x xs)
+    step h _ vKJ = appendVec (fromSing h) vKJ