diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for membership
+
+## 0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2019, Fumiaki Kinoshita
+
+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 Fumiaki Kinoshita 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.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/membership.cabal b/membership.cabal
new file mode 100644
--- /dev/null
+++ b/membership.cabal
@@ -0,0 +1,36 @@
+cabal-version:       2.2
+-- Initial package description 'membership.cabal' generated by 'cabal
+-- init'.  For further documentation, see
+-- http://haskell.org/cabal/users-guide/
+
+name:                membership
+version:             0
+synopsis:            Indices for type level lists
+description:         See README
+homepage:            https://github.com/fumieval/membership
+-- bug-reports:
+license:             BSD-3-Clause
+license-file:        LICENSE
+author:              Fumiaki Kinoshita
+maintainer:          fumiexcel@gmail.com
+-- copyright:
+category:            Type
+extra-source-files:  CHANGELOG.md
+
+library
+  exposed-modules:
+    Type.Membership
+    Type.Membership.Internal
+    Type.Membership.HList
+  -- other-modules:
+  -- other-extensions:
+  build-depends:       base >=4.9.0.0 && <5
+    , deepseq
+    , constraints
+    , hashable
+    , template-haskell
+    , th-lift
+    , prettyprinter
+  hs-source-dirs:      src
+  ghc-options: -Wall -Wcompat
+  default-language:    Haskell2010
diff --git a/src/Type/Membership.hs b/src/Type/Membership.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Membership.hs
@@ -0,0 +1,136 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitNamespaces #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+module Type.Membership
+  ( -- * Membership
+  Membership
+  , getMemberId
+  , mkMembership
+  , leadership
+  , nextMembership
+  , testMembership
+  , compareMembership
+  , impossibleMembership
+  , reifyMembership
+  , Member
+  -- * Association
+  , Assoc(..)
+  , type (>:)
+  , Lookup(..)
+  , KeyOf
+  , KeyIs
+  , proxyKeyOf
+  , stringKeyOf
+  , TargetOf
+  , proxyTargetOf
+  , TargetIs
+  , KeyTargetAre
+  -- * Enumeration
+  , Generate(..)
+  , Forall(..)
+  , ForallF
+  -- * Reexports
+  , Proxy(..)
+  ) where
+
+import Data.Constraint
+import Data.Proxy
+import Data.String
+import GHC.TypeLits
+import Type.Membership.Internal
+
+-- | Every type-level list is an instance of 'Generate'.
+class Generate (xs :: [k]) where
+  -- | Enumerate all possible 'Membership's of @xs@.
+  henumerate :: (forall x. Membership xs x -> r -> r) -> r -> r
+
+  -- | Count the number of memberships.
+  hcount :: proxy xs -> Int
+
+  -- | Enumerate 'Membership's and construct an 'HList'.
+  hgenerateList :: Applicative f
+    => (forall x. Membership xs x -> f (h x)) -> f (HList h xs)
+
+instance Generate '[] where
+  henumerate _ r = r
+
+  hcount _ = 0
+
+  hgenerateList _ = pure HNil
+
+instance Generate xs => Generate (x ': xs) where
+  henumerate f r = f leadership $ henumerate (f . nextMembership) r
+
+  hcount _ = 1 + hcount (Proxy :: Proxy xs)
+
+  -- | Enumerate 'Membership's and construct an 'HList'.
+  hgenerateList f = HCons <$> f leadership <*> hgenerateList (f . nextMembership)
+
+-- | Every element in @xs@ satisfies @c@
+class (ForallF c xs, Generate xs) => Forall (c :: k -> Constraint) (xs :: [k]) where
+  -- | Enumerate all possible 'Membership's of @xs@ with an additional context.
+  henumerateFor :: proxy c -> proxy' xs -> (forall x. c x => Membership xs x -> r -> r) -> r -> r
+
+  hgenerateListFor :: Applicative f
+    => proxy c -> (forall x. c x => Membership xs x -> f (h x)) -> f (HList h xs)
+
+instance Forall c '[] where
+  henumerateFor _ _ _ r = r
+
+  hgenerateListFor _ _ = pure HNil
+
+instance (c x, Forall c xs) => Forall c (x ': xs) where
+  henumerateFor p _ f r = f leadership $ henumerateFor p (Proxy :: Proxy xs) (f . nextMembership) r
+
+  hgenerateListFor p f = HCons <$> f leadership <*> hgenerateListFor p (f . nextMembership)
+
+-- | HACK: Without this, the constraints are not propagated well.
+type family ForallF (c :: k -> Constraint) (xs :: [k]) :: Constraint where
+  ForallF c '[] = ()
+  ForallF c (x ': xs) = (c x, Forall c xs)
+
+-- | Take the type of the key
+type family KeyOf (kv :: Assoc k v) :: k where
+  KeyOf (k ':> v) = k
+
+-- | Proxy-level 'KeyOf'. This is useful when using 'symbolVal'.
+proxyKeyOf :: proxy kv -> Proxy (KeyOf kv)
+proxyKeyOf _ = Proxy
+
+-- | Get a string from a proxy of @'Assoc' 'Symbol' v@.
+stringKeyOf :: (IsString a, KnownSymbol (KeyOf kv)) => proxy kv -> a
+stringKeyOf = fromString . symbolVal . proxyKeyOf
+{-# INLINE stringKeyOf #-}
+
+-- | Constraint applied to 'KeyOf'
+class (pk (KeyOf kv)) => KeyIs pk kv where
+
+instance (pk k) => KeyIs pk (k ':> v)
+
+-- | Take the type of the value
+type family TargetOf (kv :: Assoc k v) :: v where
+  TargetOf (k ':> v) = v
+
+-- | Proxy-level 'TargetOf'.
+proxyTargetOf :: proxy kv -> Proxy (TargetOf kv)
+proxyTargetOf _ = Proxy
+
+-- | Constraint applied to 'TargetOf'
+class (pv (TargetOf kv)) => TargetIs pv kv where
+
+instance (pv v) => TargetIs pv (k ':> v)
+
+-- | Combined constraint for 'Assoc'
+class (pk (KeyOf kv), pv (TargetOf kv)) => KeyTargetAre pk pv kv where
+
+instance (pk k, pv v) => KeyTargetAre pk pv (k ':> v)
diff --git a/src/Type/Membership/HList.hs b/src/Type/Membership/HList.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Membership/HList.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+module Type.Membership.HList (HList(..)
+  , hindex
+  , hfoldrWithIndex
+  , htraverse
+  , htraverseWithIndex
+  , hlength) where
+
+import Type.Membership.Internal
+
+hindex :: HList h xs -> Membership xs x -> h x
+hindex HNil _ = error "impossible"
+hindex (HCons x xs) m = testMembership m (\Refl -> x) (hindex xs)
+
+htraverse :: forall f g h xs. Applicative f => (forall x. g x -> f (h x)) -> HList g xs -> f (HList h xs)
+htraverse f = go where
+  go :: HList g ts -> f (HList h ts)
+  go HNil = pure HNil
+  go (HCons h xs) = HCons <$> f h <*> go xs
+{-# INLINE htraverse #-}
+
+hlength :: HList h xs -> Int
+hlength = go 0 where
+  go :: Int -> HList h xs -> Int
+  go n HNil = n
+  go n (HCons _ xs) = let !n' = n + 1 in go n' xs
+{-# INLINE hlength #-}
diff --git a/src/Type/Membership/Internal.hs b/src/Type/Membership/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Membership/Internal.hs
@@ -0,0 +1,201 @@
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module Type.Membership.Internal (
+  -- * Membership
+  Membership
+  , getMemberId
+  , mkMembership
+  , leadership
+  , nextMembership
+  , testMembership
+  , compareMembership
+  , impossibleMembership
+  , reifyMembership
+  -- * Member class
+  , Member(..)
+  , type (∈)
+  , FindType
+  -- * Association
+  , Assoc(..)
+  , type (>:)
+  , Lookup(..)
+  , FindAssoc
+  -- * Sugar
+  , Elaborate
+  , Elaborated(..)
+  -- * HList
+  , HList(..)
+  , hfoldrWithIndex
+  , htraverseWithIndex
+  -- * Miscellaneous
+  , module Data.Type.Equality
+  , module Data.Proxy
+  ) where
+import Control.DeepSeq (NFData)
+import Data.Type.Equality
+import Data.Proxy
+import Control.Monad
+import Unsafe.Coerce
+import Data.Hashable
+import Data.Text.Prettyprint.Doc
+import Data.Typeable
+import Language.Haskell.TH hiding (Pred)
+import Language.Haskell.TH.Lift
+import Data.Semigroup (Semigroup(..))
+import GHC.TypeLits
+
+-- | A witness that of @x@ is a member of a type level set @xs@.
+newtype Membership (xs :: [k]) (x :: k) = Membership
+  { getMemberId :: Int -- ^ get the position as an 'Int'.
+  } deriving (Typeable, NFData)
+
+instance Show (Membership xs x) where
+  show (Membership n) = "$(mkMembership " ++ show n ++ ")"
+
+instance Pretty (Membership xs x) where
+  pretty (Membership n) = "$(mkMembership " <> pretty n <> ")"
+
+instance Eq (Membership xs x) where
+  _ == _ = True
+
+instance Ord (Membership xs x) where
+  compare _ _ = EQ
+
+instance Semigroup (Membership xs x) where
+  x <> _ = x
+
+-- | Generates a 'Membership' that corresponds to the given ordinal (0-origin).
+mkMembership :: Int -> Q Exp
+mkMembership n = do
+  let names = map mkName $ take (n + 1) $ concatMap (flip replicateM ['a'..'z']) [1..]
+  let rest = mkName "any"
+  let cons x xs = PromotedConsT `AppT` x `AppT` xs
+  let t = foldr cons (VarT rest) (map VarT names)
+  sigE (conE 'Membership `appE` litE (IntegerL $ toInteger n))
+    $ forallT (PlainTV rest : map PlainTV names) (pure [])
+    $ conT ''Membership `appT` pure t `appT` varT (names !! n)
+
+instance Lift (Membership xs x) where
+  lift (Membership i) = mkMembership i
+
+-- | @x@ is a member of @xs@
+class Member xs x where
+  membership :: Membership xs x
+
+instance (Elaborate x (FindType x xs) ~ 'Expecting pos, KnownNat pos) => Member xs x where
+  membership = Membership (fromInteger $ natVal (Proxy :: Proxy pos))
+  {-# INLINE membership #-}
+
+instance Hashable (Membership xs x) where
+  hashWithSalt s = hashWithSalt s . getMemberId
+
+-- | A readable type search result
+data Elaborated k v = Expecting v | Missing k | Duplicate k
+
+-- | Make the result more readable
+type family Elaborate (key :: k) (xs :: [v]) :: Elaborated k v where
+  Elaborate k '[] = 'Missing k
+  Elaborate k '[x] = 'Expecting x
+  Elaborate k xs = 'Duplicate k
+
+-- | Find a type associated to the specified key.
+type family FindAssoc (n :: Nat) (key :: k) (xs :: [Assoc k v]) where
+  FindAssoc n k ((k ':> v) ': xs) = (n ':> v) ': FindAssoc (1 + n) k xs
+  FindAssoc n k ((k' ':> v) ': xs) = FindAssoc (1 + n) k xs
+  FindAssoc n k '[] = '[]
+
+-- | Embodies a type equivalence to ensure that the 'Membership' points the first element.
+testMembership :: Membership (y ': xs) x -> (x :~: y -> r) -> (Membership xs x -> r) -> r
+testMembership (Membership 0) l _ = l (unsafeCoerce Refl)
+testMembership (Membership n) _ r = r (Membership (n - 1))
+{-# INLINE testMembership #-}
+
+-- | Compare two 'Membership's.
+compareMembership :: Membership xs x -> Membership xs y -> Either Ordering (x :~: y)
+compareMembership (Membership m) (Membership n) = case compare m n of
+  EQ -> Right (unsafeCoerce Refl)
+  x -> Left x
+{-# INLINE compareMembership #-}
+
+-- | There is no 'Membership' of an empty list.
+impossibleMembership :: Membership '[] x -> r
+impossibleMembership _ = error "Impossible"
+
+-- | This 'Membership' points to the first element
+leadership :: Membership (x ': xs) x
+leadership = Membership 0
+{-# INLINE leadership #-}
+
+-- | The next membership
+nextMembership :: Membership xs y -> Membership (x ': xs) y
+nextMembership (Membership n) = Membership (n + 1)
+{-# INLINE nextMembership #-}
+
+-- | Make up a 'Membership' from an integer.
+reifyMembership :: Int -> (forall x. Membership xs x -> r) -> r
+reifyMembership n k = k (Membership n)
+
+-- | Unicode flipped alias for 'Member'
+type x ∈ xs = Member xs x
+
+-- | FindType types
+type family FindType (x :: k) (xs :: [k]) :: [Nat] where
+  FindType x (x ': xs) = 0 ': MapSucc (FindType x xs)
+  FindType x (y ': ys) = MapSucc (FindType x ys)
+  FindType x '[] = '[]
+
+-- | Ideally, it will be 'Map Succ'
+type family MapSucc (xs :: [Nat]) :: [Nat] where
+  MapSucc '[] = '[]
+  MapSucc (x ': xs) = (1 + x) ': MapSucc xs
+
+-- | The kind of key-value pairs
+data Assoc k v = k :> v
+infix 0 :>
+
+-- | A synonym for (':>')
+type (>:) = '(:>)
+
+-- | @'Lookup' xs k v@ is essentially identical to @(k :> v) ∈ xs@
+-- , but the type @v@ is inferred from @k@ and @xs@.
+class Lookup xs k v | k xs -> v where
+  association :: Membership xs (k ':> v)
+
+instance (Elaborate k (FindAssoc 0 k xs) ~ 'Expecting (n ':> v), KnownNat n) => Lookup xs k v where
+  association = Membership (fromInteger $ natVal (Proxy :: Proxy n))
+
+data HList (h :: k -> *) (xs :: [k]) where
+  HNil :: HList h '[]
+  HCons :: h x -> HList h xs -> HList h (x ': xs)
+
+infixr 5 `HCons`
+
+hfoldrWithIndex :: forall h r xs. (forall x. Membership xs x -> h x -> r -> r) -> r -> HList h xs -> r
+hfoldrWithIndex f r = go 0 where
+  go :: Int -> HList h t -> r
+  go !k (HCons x xs) = f (Membership k) x $ go (k + 1) xs
+  go _ HNil = r
+{-# INLINE hfoldrWithIndex #-}
+
+htraverseWithIndex :: forall f g h xs. Applicative f
+    => (forall x. Membership xs x -> g x -> f (h x)) -> HList g xs -> f (HList h xs)
+htraverseWithIndex f = go 0 where
+  go :: Int -> HList g t -> f (HList h t)
+  go !k (HCons x xs) = HCons <$> f (Membership k) x <*> go (k + 1) xs
+  go _ HNil = pure HNil
+{-# INLINE htraverseWithIndex #-}