diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,8 @@
+# TODO
+* Add doctests
+* Add TyFun from singletons (or just depend from)?
+
+# CHANGELOG
+
+## 0.0.1
+First version
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, Aleksey Uimanov
+
+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 Aleksey Uimanov 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/example/Main.hs b/example/Main.hs
new file mode 100644
--- /dev/null
+++ b/example/Main.hs
@@ -0,0 +1,40 @@
+module Main where
+
+import Data.Proxy
+import TypeFun.Data.List
+import TypeFun.Data.Peano
+
+-- | This function has wider constraint __Int is inside l__
+elemConstr :: (Elem Int l) => proxy l -> Int
+elemConstr p = 1
+
+-- | This function has narrower constraint than 'elemConstr'
+-- __Int and Bool are contained in l__
+sublistConstr :: (SubList '[Int, Bool] l) => proxy l -> Int
+sublistConstr p = elemConstr p + 1
+
+-- | This function has narrower constraint than 'sublistConstr' (Order
+-- of elements matters)
+prefixConstr :: (IsPrefixOf '[Int, Bool] l) => proxy l -> Int
+prefixConstr p = sublistConstr p + 1
+
+-- | This function has narrower constraint
+-- __Int is inside of l and it is a first argument__
+-- and uses inside more wide function
+indexConstr :: (('Just 'Z) ~ (IndexOfMay Int l)) => proxy l -> Int
+indexConstr p = elemConstr p + 1
+
+uniqConstr :: (UniqElements l) => proxy l -> Int
+uniqConstr _ = 1
+
+main :: IO ()
+main = do
+  let
+    p2 = Proxy :: Proxy '[Int, Bool]
+    p3 = Proxy :: Proxy '[Int, Bool, Int]
+  print $ indexConstr p2
+  print $ sublistConstr p2
+  print $ prefixConstr p2
+  print $ prefixConstr p3
+  print $ uniqConstr p2
+  -- print $ uniqConstr p3 -- < ElementIsNotUniqInList Int '[Int, Bool, Int]
diff --git a/src/TypeFun/Constraint.hs b/src/TypeFun/Constraint.hs
new file mode 100644
--- /dev/null
+++ b/src/TypeFun/Constraint.hs
@@ -0,0 +1,10 @@
+module TypeFun.Constraint
+  ( AllSatisfy
+  ) where
+
+import GHC.Exts
+
+-- | Apply constraint for each element of list
+type family AllSatisfy (c :: k -> Constraint) (s :: [k]) :: Constraint where
+  AllSatisfy c '[]       = ()
+  AllSatisfy c (a ': as) = (c a, AllSatisfy c as)
diff --git a/src/TypeFun/Data/Eq.hs b/src/TypeFun/Data/Eq.hs
new file mode 100644
--- /dev/null
+++ b/src/TypeFun/Data/Eq.hs
@@ -0,0 +1,7 @@
+module TypeFun.Data.Eq
+  ( Equal
+  ) where
+
+type family Equal (a :: k) (b :: k) :: Bool where
+  Equal a a = 'True
+  Equal a b = 'False
diff --git a/src/TypeFun/Data/List.hs b/src/TypeFun/Data/List.hs
new file mode 100644
--- /dev/null
+++ b/src/TypeFun/Data/List.hs
@@ -0,0 +1,208 @@
+-- | Collection of type families on type lists. This module differs
+-- from __Data.Singletons.Prelude.List__ because works with __[*]__
+-- and relies on GHC's type equality (~). The rest of required
+-- operations like 'Reverse' or '(:++:)' you could find in singletons
+
+module TypeFun.Data.List
+  ( -- * Primitive operations on lists
+    Length
+  , Drop
+  , Take
+  , Delete
+  , Remove
+  , (:++:)
+    -- * Elements lookup
+  , IndexOf
+  , IndexOfMay
+  , IndexOfMay'
+  , IndicesOfMay
+  , IndicesOf
+  , Index
+  , IndexMay
+  , IndicesMay
+  , Indices
+  , Elem
+  , NotElem
+  , Count
+    -- * Operations with lists
+  , SubList
+  , NotSubList
+  , IsPrefixOf
+  , IsNotPrefixOf
+  , IsPrefixOfBool
+    -- * Set operations
+  , Union
+  , UnionList
+  , AppendUniq
+  , Intersect
+    -- * Uniqueness checking
+  , ElementIsUniq
+  , UniqElements
+  , UniqElements'
+  ) where
+
+import Data.Type.Bool
+import GHC.Exts
+import GHC.TypeLits
+import TypeFun.Data.Eq
+import TypeFun.Data.Maybe
+import TypeFun.Data.Peano
+
+------------------------------------------------------------------------
+-- NOTE: Errors type classes. These type classes are not in separate  --
+-- module because in this case user could import them and instantiate --
+-- by mistake. The name of typeclass is an error message in fact. We  --
+-- have not any way to fail constraint explicitly, so this hack was   --
+-- introduced.                                                        --
+------------------------------------------------------------------------
+
+class ElementNotFoundInList a s
+
+class ElementIsInList a s
+
+class ListIsNotPrefixOf a b
+
+class ListIsPrefixOf a b
+
+class ElementIsNotUniqInList a s
+
+class IndexNotFoundInList a s
+
+----------------------
+-- main module code --
+----------------------
+
+
+type family Length (a :: [k]) :: N where
+  Length '[] = 'Z
+  Length (a ': as) = 'S (Length as)
+
+type family Drop (c :: N) (s :: [k]) :: [k] where
+  Drop 'Z     s         = s
+  Drop ('S c) '[]       = '[]
+  Drop ('S c) (a ': as) = Drop c as
+
+type family Take (c :: N) (s :: [k]) :: [k] where
+  Take 'Z     s         = '[]
+  Take ('S c) '[]       = '[]
+  Take ('S c) (a ': as) = a ': (Take c as)
+
+-- | Remove first argument type from anywhere in a list.
+type family Delete (a :: k) (s :: [k]) :: [k] where
+  Delete a '[]       = '[]
+  Delete a (a ': as) = Delete a as
+  Delete a (b ': as) = b ': (Delete a as)
+
+-- | Remove index from the list
+type family Remove (i :: N) (a :: [k]) :: [k] where
+  Remove i      '[]       = '[]
+  Remove 'Z     (a ': as) = as
+  Remove ('S i) (a ': as) = a ': (Remove i as)
+
+type family (:++:) (a :: [k]) (b :: [k]) :: [k] where
+  '[] :++: b = b
+  (a ': as) :++: b = a ': (as :++: b)
+
+type IndexOf a s = FromJust (IndexOfMay a s)
+
+type IndexOfMay a s = IndexOfMay' Z a s
+
+type family IndexOfMay' (acc :: N) (a :: k) (s :: [k]) :: Maybe N where
+  IndexOfMay' acc a '[]       = 'Nothing
+  IndexOfMay' acc a (a ': as) = 'Just acc
+  IndexOfMay' acc a (b ': as) = IndexOfMay' (S acc) a as
+
+type family IndicesOfMay (a :: [k]) (b :: [k]) :: [Maybe N] where
+  IndicesOfMay '[] bs = '[]
+  IndicesOfMay (a ': as) bs = (IndexOfMay a bs) ': (IndicesOfMay as bs)
+
+type family IndicesOf (a :: [k]) (b :: [k]) :: [N] where
+  IndicesOf '[] bs = '[]
+  IndicesOf (a ': as) bs = (IndexOf a bs) ': (IndicesOf as bs)
+
+type Index idx s = FromJust (IndexMay idx s)
+
+type family IndexMay (idx :: N) (s :: [k]) :: Maybe k where
+  IndexMay idx     '[]       = 'Nothing
+  IndexMay Z       (a ': as) = 'Just a
+  IndexMay (S idx) (a ': as) = IndexMay idx as
+
+type family IndicesMay (idxs :: [N]) (a :: [k]) :: [Maybe k] where
+  IndicesMay '[] as = '[]
+  IndicesMay (i ': idxs) as = (IndexMay i as) ': (IndicesMay idxs as)
+
+type family Indices (idxs :: [N]) (a :: [k]) :: [k] where
+  Indices '[]         as = '[]
+  Indices (i ': idxs) as = (Index i as) ': (Indices idxs as)
+
+-- | Generates unresolvable constraint if fists element is not
+-- contained inside of second
+type Elem a s = NothingToConstr (IndexOfMay a s)
+                                (ElementNotFoundInList a s)
+
+-- | Reverse of 'Elem'
+type NotElem a s = JustToConstr (IndexOfMay a s)
+                                (ElementIsInList a s)
+
+-- | Count elements in a list
+type family Count (a :: k) (s :: [k]) :: N where
+  Count a '[]       = 'Z
+  Count a (a ': as) = 'S (Count a as)
+  Count a (b ': as) = Count a as
+
+-- | Constanints that first argument is a sublist of second. Reduces
+-- to __(Elem a1 b, Elem a2 b, Elem a3 b, ...)__
+type family SubList (a :: [k]) (b :: [k]) :: Constraint where
+  SubList '[]       bs = ()
+  SubList (a ': as) bs = (Elem a bs, SubList as bs)
+
+type family NotSubList (a :: [k]) (b :: [k]) :: Constraint where
+  NotSubList '[]       bs = ()
+  NotSubList (a ': as) bs = (NotElem a bs, NotSubList as bs)
+
+type IsPrefixOf a b = ( If (IsPrefixOfBool a b)
+                           (() :: Constraint)
+                           (ListIsNotPrefixOf a b)
+                      , SubList a b )
+
+type IsNotPrefixOf a b = If (IsPrefixOfBool a b)
+                            (ListIsPrefixOf a b)
+                            (() :: Constraint)
+
+-- | First argument is prefix of second
+type family IsPrefixOfBool (a :: [k]) (b :: [k]) :: Bool where
+  IsPrefixOfBool '[]       b         = 'True
+  IsPrefixOfBool (a ': as) (a ': bs) = IsPrefixOfBool as bs
+  IsPrefixOfBool as        bs        = 'False
+
+-- | Appends elements from first list to second if they are not
+-- presented in.
+type family Union (a :: [k]) (b :: [k]) :: [k] where
+  Union '[]       bs = bs
+  Union (a ': as) bs = Union as (AppendUniq a bs)
+
+type family UnionList (l :: [[k]]) :: [k] where
+  UnionList '[]       = '[]
+  UnionList (a ': as) = Union a (UnionList as)
+
+-- | Append element to list if element is not already presented in
+type family AppendUniq (a :: k) (s :: [k]) :: [k] where
+  AppendUniq a (a ': bs) = a ': bs
+  AppendUniq a (b ': bs) = b ': (AppendUniq a bs)
+  AppendUniq a '[]       = '[a]
+
+-- | Calculates intersection between two lists. Order of elements is
+-- taken from first list
+type Intersect a b = (Indices (CatMaybes (IndicesOfMay a b)) b)
+
+-- | Checks that element 'a' occurs in a list just once
+type ElementIsUniq a s = If (Equal (S Z) (Count a s))
+                            (() :: Constraint)
+                            (ElementIsNotUniqInList a s)
+
+-- | Checks that all elements in list are unique
+type UniqElements a = UniqElements' a a
+
+type family UniqElements' (a :: [k]) (self :: [k]) :: Constraint where
+  UniqElements' '[]       self = ()
+  UniqElements' (a ': as) self = (ElementIsUniq a self, UniqElements' as self)
diff --git a/src/TypeFun/Data/Maybe.hs b/src/TypeFun/Data/Maybe.hs
new file mode 100644
--- /dev/null
+++ b/src/TypeFun/Data/Maybe.hs
@@ -0,0 +1,32 @@
+module TypeFun.Data.Maybe
+  ( MaybeCase
+  , NothingToConstr
+  , JustToConstr
+  , CatMaybes
+  , FromJust
+  ) where
+
+import GHC.Exts
+
+type family MaybeCase (a :: Maybe k)
+                      (nothing :: r)
+                      (just :: k -> r) :: r where
+  MaybeCase 'Nothing nothing just  = nothing
+  MaybeCase ('Just k) nothing just = just k
+
+type family NothingToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
+  NothingToConstr 'Nothing  c = c
+  NothingToConstr ('Just a) c = ()
+
+type family JustToConstr (a :: Maybe k) (c :: Constraint) :: Constraint where
+  JustToConstr 'Nothing  c = ()
+  JustToConstr ('Just a) c = c
+
+-- | Like 'catMaybes' for type lists
+type family CatMaybes (l :: [Maybe k]) :: [k] where
+  CatMaybes '[]               = '[]
+  CatMaybes (('Just a) ': as) = a ': (CatMaybes as)
+  CatMaybes ('Nothing ': as)  = CatMaybes as
+
+type family FromJust (a :: Maybe k) :: k where
+  FromJust ('Just a) = a
diff --git a/src/TypeFun/Data/Peano.hs b/src/TypeFun/Data/Peano.hs
new file mode 100644
--- /dev/null
+++ b/src/TypeFun/Data/Peano.hs
@@ -0,0 +1,37 @@
+module TypeFun.Data.Peano
+  ( N(..)
+  , ToNat
+  , FromNat
+  , (:+:)
+  , (:-:)
+  , (:*:)
+  ) where
+
+import Data.Typeable
+import GHC.Generics (Generic)
+import GHC.TypeLits
+
+data N = Z | S N
+         deriving ( Eq, Ord, Read, Show
+                  , Generic, Typeable )
+
+type family ToNat (a :: N) :: Nat where
+  ToNat Z = 0
+  ToNat (S a) = 1 + (ToNat a)
+
+type family FromNat (a :: Nat) :: N where
+  FromNat 0 = Z
+  FromNat a = S (FromNat (a - 1))
+
+type family (:+:) (a :: N) (b :: N) :: N where
+  Z :+: b = b
+  (S a) :+: b = a :+: (S b)
+
+type family (:-:) (a :: N) (b :: N) :: N where
+  a :-: Z = a
+  (S a) :-: (S b) = a :-: b
+
+type family (:*:) (a :: N) (b :: N) :: N where
+  Z :*: b = Z
+  a :*: Z = Z
+  (S a) :*: b = b :+: (a :*: b)
diff --git a/type-fun.cabal b/type-fun.cabal
new file mode 100644
--- /dev/null
+++ b/type-fun.cabal
@@ -0,0 +1,50 @@
+name:                type-fun
+version:             0.0.1
+synopsis:            Collection of widely reimplemented type families
+license:             BSD3
+license-file:        LICENSE
+author:              Aleksey Uimanov
+maintainer:          s9gf4ult@gmail.com
+category:            Dependent Types
+build-type:          Simple
+extra-source-files:  CHANGELOG.md
+cabal-version:       >=1.10
+homepage:            https://github.com/s9gf4ult/type-fun
+source-repository head
+  type:     git
+  location: git@github.com:s9gf4ult/type-fun.git
+
+library
+  default-language:    Haskell2010
+  hs-source-dirs:      src
+  default-extensions:  ConstraintKinds
+                     , DataKinds
+                     , DeriveGeneric
+                     , FlexibleInstances
+                     , MultiParamTypeClasses
+                     , PolyKinds
+                     , TypeFamilies
+                     , TypeOperators
+                     , UndecidableInstances
+
+  exposed-modules:     TypeFun.Constraint
+                     , TypeFun.Data.Eq
+                     , TypeFun.Data.List
+                     , TypeFun.Data.Maybe
+                     , TypeFun.Data.Peano
+
+  build-depends:       base >=4.7 && <4.9
+
+
+test-suite example
+  type:               exitcode-stdio-1.0
+  default-language:   Haskell2010
+  hs-source-dirs:     example
+  main-is:            Main.hs
+  default-extensions: DataKinds
+                    , GADTs
+                    , TemplateHaskell
+                    , TypeFamilies
+                    , UndecidableInstances
+  build-depends:  base
+                , type-fun