diff --git a/ChangeLog.md b/ChangeLog.md
new file mode 100644
--- /dev/null
+++ b/ChangeLog.md
@@ -0,0 +1,7 @@
+# Changelog for type-sets
+
+## 0.1.0.0 --- 2019-08-07
+
+Initial release!
+
+## Unreleased changes
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Sandy Maguire (c) 2019
+
+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 Sandy Maguire 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,53 @@
+# type-sets
+
+[![Build Status](https://api.travis-ci.org/isovector/type-sets.svg?branch=master)](https://travis-ci.org/isovector/type-sets)
+[![Hackage](https://img.shields.io/hackage/v/cmptype.svg?logo=haskell&label=cmptype)](https://hackage.haskell.org/package/cmptype)
+
+
+## Dedication
+
+> Obstacles don't have to stop you. If you run into a wall, don't turn around
+> and give up. Figure out how to climb it, go through it, or work around it.
+
+> -- Michael Jordan, on complexity analysis in Haskell
+
+
+## Overview
+
+How much do you hate programming at the type level, but only being able to use
+lists? A million? *Two* million? Some mathematicians suspect that there may be
+even larger degrees of hate.
+
+Enter `type-sets`. They're sets... at the type-level! Check this:
+
+```haskell
+{-# OPTIONS_GHC -fplugin=Type.Compare.Plugin #-}
+
+import Type.Set
+
+type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))
+
+test1 :: Proxy (Member Bool MySet) -> Proxy 'True
+test1 = id  -- Bool is a member :)
+
+test2 :: Proxy (Member Char MySet) -> Proxy 'False
+test2 = id  -- False is not a member :(
+```
+
+See the `Type.Set` module for more operations.
+
+But wait, there's more! There's also a proof-of-concept `Type.Set.Variant` for
+describing open-sums indexed by type-sets. PRs to make it better would be
+greatly appreciated!
+
+One love.
+
+
+## Acknowledgments
+
+Huge shout-outs to [Boris Rozinov][oofp] for all of his help on this library,
+including the original idea, help with the implementation, infinite amounts of
+coffee, and a couch to sleep on while it was being made.
+
+[oofp]: https://github.com/oofp
+
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/src/Type/Set.hs b/src/Type/Set.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Set.hs
@@ -0,0 +1,135 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Type.Set
+  ( -- * Core type
+    TypeSet (..)
+
+    -- * Set operations
+  , Member
+  , Insert
+  , Remove
+  , Merge
+
+    -- * Tree operations
+  , Locate
+  , Follow
+  , Side (..)
+  ) where
+
+import Type.Compare
+import GHC.TypeLits
+
+
+------------------------------------------------------------------------------
+-- | A binary search tree. When @-XDataKinds@ is turned on, this becomes the
+-- backbone of the type-level set.
+--
+-- >>> type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))
+data TypeSet a
+  = Empty
+  | Branch a (TypeSet a) (TypeSet a)
+
+
+------------------------------------------------------------------------------
+-- | Either left or right down a path.
+data Side = L | R
+  deriving (Eq, Ord, Show)
+
+------------------------------------------------------------------------------
+-- | /O(log n)/. Insert an element into the 'TypeSet'.
+type family Insert (t :: k) (bst :: TypeSet k)  :: TypeSet k where
+  Insert t 'Empty = 'Branch t 'Empty 'Empty
+  Insert t ('Branch a lbst rbst) =
+    InsertImpl (CmpType t a) t a lbst rbst
+
+type family InsertImpl (ord :: Ordering)
+                       (t :: k)
+                       (a :: k)
+                       (lbst :: TypeSet k)
+                       (rbst :: TypeSet k) :: TypeSet k where
+  InsertImpl 'EQ t a lbst rbst = 'Branch a lbst rbst
+  InsertImpl 'LT t a lbst rbst = 'Branch a (Insert t lbst) rbst
+  InsertImpl 'GT t a lbst rbst = 'Branch a lbst (Insert t rbst)
+
+
+------------------------------------------------------------------------------
+-- | /O(log n)/. Determine membership in the 'TypeSet.'
+type family Member (t :: k) (bst :: TypeSet k)  :: Bool where
+  Member t 'Empty = 'False
+  Member t ('Branch a lbst rbst) = MemberImpl (CmpType t a) t lbst rbst
+
+type family MemberImpl (ord :: Ordering)
+                       (t :: k)
+                       (lbst :: TypeSet k)
+                       (rbst :: TypeSet k) :: Bool where
+  MemberImpl 'EQ t lbst rbst = 'True
+  MemberImpl 'LT t lbst rbst = Member t lbst
+  MemberImpl 'GT t lbst rbst = Member t rbst
+
+
+------------------------------------------------------------------------------
+-- | /O(m log n)/ for @Merge m n@; put your smaller set on the left side. Merge
+-- two 'TypeSet's together.
+type family Merge (small :: TypeSet k) (big :: TypeSet k) :: TypeSet k where
+  Merge Empty big   = big
+  Merge small Empty = small
+  Merge ('Branch a lbst rbst) big = Merge rbst (Merge lbst (Insert a big))
+
+
+------------------------------------------------------------------------------
+-- | /O(log n)/. Remove an element from the 'TypeSet'.
+type family Remove (t :: k) (bst :: TypeSet k) :: TypeSet k where
+  Remove t Empty = Empty
+  Remove t ('Branch a lbst rbst) = RemoveImpl (CmpType t a) t a lbst rbst
+
+type family RemoveImpl (ord :: Ordering)
+                       (t :: k)
+                       (a :: k)
+                       (lbst :: TypeSet k)
+                       (rbst :: TypeSet k) :: TypeSet k where
+  RemoveImpl 'LT t a lbst rbst = 'Branch a (Remove t lbst) rbst
+  RemoveImpl 'EQ t a Empty rbst = rbst
+  RemoveImpl 'EQ t a lbst Empty = lbst
+  RemoveImpl 'EQ t a lbst rbst =
+    'Branch (RightMost lbst) (Remove (RightMost lbst) lbst) rbst
+  RemoveImpl 'GT t a lbst rbst = 'Branch a lbst (Remove t rbst)
+
+
+------------------------------------------------------------------------------
+-- | /O(log n)/. Get the right-most element in a tree. This function is stuck
+-- if the tree is empty.
+type family RightMost (bst :: TypeSet k) :: k where
+  RightMost ('Branch a lbst 'Empty) = a
+  RightMost ('Branch a lbst rbst) = RightMost rbst
+
+
+------------------------------------------------------------------------------
+-- | /O(log n)/. Compute a @['Side']@ which finds the desired element in the
+-- tree. The result of this can be passed to 'Follow' in order to look up the
+-- same element again later.
+type family Locate (t :: k) (bst :: TypeSet k) :: [Side] where
+  Member t ('Branch a lbst rbst) = LocateImpl (CmpType t a) t lbst rbst
+  Member t 'Empty = TypeError ('Text "Unable to locate: " ':<>: 'ShowType t)
+
+type family LocateImpl (ord :: Ordering)
+                       (t :: k)
+                       (lbst :: TypeSet k)
+                       (rbst :: TypeSet k) :: [Side] where
+  LocateImpl 'EQ t lbst rbst = '[]
+  LocateImpl 'LT t lbst rbst = 'L ': Locate t lbst
+  LocateImpl 'GT t lbst rbst = 'R ': Locate t rbst
+
+
+------------------------------------------------------------------------------
+-- | /O(log n)/. Follow the result of a 'Locate' to get a particular element in
+-- the tree.
+type family Follow (ss :: [Side]) (bst :: TypeSet k) :: k where
+  Follow '[] ('Branch t _ _) = t
+  Follow ('L ': ss) ('Branch _ l _) = Follow ss l
+  Follow ('R ': ss) ('Branch _ _ r) = Follow ss r
+  Follow ss 'Empty = TypeError ('Text "Unable to follow: " ':<>: 'ShowType ss)
+
diff --git a/src/Type/Set/Variant.hs b/src/Type/Set/Variant.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Set/Variant.hs
@@ -0,0 +1,138 @@
+{-# LANGUAGE AllowAmbiguousTypes   #-}
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE KindSignatures        #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RoleAnnotations       #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeApplications      #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+{-# OPTIONS_GHC -Wall              #-}
+
+module Type.Set.Variant
+  ( -- * Core types
+    Variant (..)
+  , Has (..)
+
+    -- * Decomposition proofs
+  , decompRoot
+  , Split (..)
+
+    -- * Weakening
+  , weaken
+
+    -- * Internal stuff
+  , proveFollowInsert
+  , SSide (..)
+  , FromSides (..)
+  ) where
+
+import Data.Type.Equality
+import Type.Set
+import Unsafe.Coerce
+
+------------------------------------------------------------------------------
+-- | Singletons for 'Side's.
+data SSide (ss :: [Side]) where
+  SNil :: SSide '[]
+  SL :: SSide ss -> SSide ('L ': ss)
+  SR :: SSide ss -> SSide ('R ': ss)
+
+------------------------------------------------------------------------------
+-- | Get a singleton for a list of 'Side's.
+class FromSides (ss :: [Side]) where
+  fromSides :: SSide ss
+
+instance FromSides '[] where
+  fromSides = SNil
+
+instance FromSides ss => FromSides ('L ': ss) where
+  fromSides = SL fromSides
+
+instance FromSides ss => FromSides ('R ': ss) where
+  fromSides = SR fromSides
+
+
+------------------------------------------------------------------------------
+-- | A 'Variant' is like an 'Either', except that it can store any of the types
+-- contained in the 'TypeSet'. You can use 'toVariant' to construct one, and
+-- 'fromVariant' to pattern match it out.
+data Variant (v :: TypeSet *) where
+  Variant :: SSide ss -> Follow ss v -> Variant v
+type role Variant nominal
+
+
+------------------------------------------------------------------------------
+-- | A proof that the set @bst@ contains type @t@.
+class Has t bst where
+  -- | Inject a @t@ into a 'Variant'.
+  toVariant :: t -> Variant bst
+  -- | Attempt to project a 'Variant' into @t@. This might fail, because there
+  -- is no guarantee that the 'Variant' /actually contains/ @t@.
+  --
+  -- You can use 'decompRoot' instead of this function if you'd like a proof
+  -- that the 'Variant' doesn't contain @t@ in the case of failure.
+  fromVariant :: Variant bst -> Maybe t
+
+instance ( Follow (Locate t bst) bst ~ t
+         , FromSides (Locate t bst)
+         ) => Has t bst where
+  toVariant = Variant (fromSides @(Locate t bst))
+  fromVariant (Variant tag res) =
+    case testEquality tag (fromSides @(Locate t bst)) of
+      Just Refl -> Just res
+      Nothing -> Nothing
+
+
+instance TestEquality SSide where
+  testEquality SNil   SNil   = Just Refl
+  testEquality (SL a) (SL b) =
+    case testEquality a b of
+      Just Refl -> Just Refl
+      Nothing -> Nothing
+  testEquality (SR a) (SR b) =
+    case testEquality a b of
+      Just Refl -> Just Refl
+      Nothing -> Nothing
+  testEquality (SL _) SNil   = Nothing
+  testEquality SNil   (SL _) = Nothing
+  testEquality (SR _) SNil   = Nothing
+  testEquality SNil   (SR _) = Nothing
+  testEquality (SR _) (SL _) = Nothing
+  testEquality (SL _) (SR _) = Nothing
+
+
+------------------------------------------------------------------------------
+-- | A proof that inserting into a @bst@ doesn't affect the position of
+-- anything already in the tree.
+proveFollowInsert :: Follow ss (Insert t bst) :~: Follow ss bst
+proveFollowInsert = unsafeCoerce Refl
+
+
+------------------------------------------------------------------------------
+-- | Weaken a 'Variant' so that it can contain something else.
+weaken :: forall t bst. Variant bst -> Variant (Insert t bst)
+weaken (Variant (tag :: SSide ss) res) = Variant tag $
+  case proveFollowInsert @ss @t @bst of
+    Refl -> res
+
+
+data Split t lbst rbst
+  = Root t
+  | LSplit (Variant lbst)
+  | RSplit (Variant rbst)
+
+
+------------------------------------------------------------------------------
+-- | Like 'fromVariant', but decomposes the 'Variant' into its left and right
+-- branches, depending on where @t@ is.
+decompRoot :: Variant ('Branch t lbst rbst) -> Split t lbst rbst
+decompRoot (Variant SNil t) = Root t
+decompRoot (Variant (SL s) t) = LSplit (Variant s t)
+decompRoot (Variant (SR s) t) = RSplit (Variant s t)
+
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,19 @@
+{-# LANGUAGE DataKinds #-}
+
+{-# OPTIONS_GHC -fplugin=Type.Compare.Plugin      #-}
+{-# OPTIONS_GHC -fconstraint-solver-iterations=10 #-}
+
+import Data.Proxy
+import Type.Set
+
+type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))
+
+test1 :: Proxy (Member Bool MySet) -> Proxy 'True
+test1 = id  -- Bool is a member :)
+
+test2 :: Proxy (Member Char MySet) -> Proxy 'False
+test2 = id  -- False is not a member :(
+
+main :: IO ()
+main = putStrLn "It compiled!"
+
diff --git a/type-sets.cabal b/type-sets.cabal
new file mode 100644
--- /dev/null
+++ b/type-sets.cabal
@@ -0,0 +1,55 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 60b368d526cc5cac3b6dd1535ea9d63df46fe48ac16f522464490b53a71a034b
+
+name:           type-sets
+version:        0.1.0.0
+synopsis:       Type-level sets
+description:    Please see the README on GitHub at <https://github.com/isovector/type-sets#readme>
+category:       Type
+homepage:       https://github.com/isovector/type-sets#readme
+bug-reports:    https://github.com/isovector/type-sets/issues
+author:         Sandy Maguire
+maintainer:     sandy@sandymaguire.me
+copyright:      2019 Sandy Maguire
+license:        BSD3
+license-file:   LICENSE
+build-type:     Simple
+extra-source-files:
+    README.md
+    ChangeLog.md
+
+source-repository head
+  type: git
+  location: https://github.com/isovector/type-sets
+
+library
+  exposed-modules:
+      Type.Set
+      Type.Set.Variant
+  other-modules:
+      Paths_type_sets
+  hs-source-dirs:
+      src
+  build-depends:
+      base >=4.7 && <5
+    , cmptype >=0.1.0.0 && <0.2
+  default-language: Haskell2010
+
+test-suite type-sets-test
+  type: exitcode-stdio-1.0
+  main-is: Spec.hs
+  other-modules:
+      Paths_type_sets
+  hs-source-dirs:
+      test
+  ghc-options: -threaded -rtsopts -with-rtsopts=-N
+  build-depends:
+      base >=4.7 && <5
+    , cmptype >=0.1.0.0 && <0.2
+    , type-sets
+  default-language: Haskell2010