diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/src/Type/Bool.hs b/src/Type/Bool.hs
--- a/src/Type/Bool.hs
+++ b/src/Type/Bool.hs
@@ -13,31 +13,45 @@
 
 -- === Basic operations ===
 
+type family Not a where
+  Not 'True  = 'False
+  Not 'False = 'True
+
 type family And a b where
-  And True True = True
-  And a    b    = False
+  And 'True 'True = 'True
+  And a      b    = 'False
 
 type family Or a b where
-  Or True b    = True
-  Or a    True = True
-  Or a    b    = False
+  Or 'True b     = 'True
+  Or a     'True = 'True
+  Or a     b     = 'False
 
 type family Xor a b where
-  Xor True True = False
-  Xor True b    = True
-  Xor a    True = True
-  Xor a    b    = False
+  Xor 'True 'True = 'False
+  Xor 'True b     = 'True
+  Xor a     'True = 'True
+  Xor a     b     = 'False
 
 type family If (cond :: Bool) (a :: k) (b :: k) :: k where
-  If cond  a a = a
-  If True  a b = a
-  If False a b = b
+  If cond   a a = a
+  If 'True  a b = a
+  If 'False a b = b
 
 type family If' (cond :: Bool) (a :: Constraint) (b :: Constraint) :: Constraint where
-  If' cond  a a = a
-  If' True  a b = a
-  If' False a b = b
+  If'  cond  a a = a
+  If' 'True  a b = a
+  If' 'False a b = b
 
-type family (:==) (a :: k) (b :: l) where
-    a :== a = True
-    a :== b = False
+type family (a :: k) == (b :: l) where
+    a == a = 'True
+    a == b = 'False
+
+
+-- === Type level queries ===
+
+class    KnownBool (b :: Bool) where boolVal :: Proxy b -> Bool
+instance KnownBool True        where boolVal _ = True
+instance KnownBool False       where boolVal _ = False
+
+
+
diff --git a/src/Type/Container.hs b/src/Type/Container.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Container.hs
@@ -0,0 +1,40 @@
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Type.Container where
+
+import Prelude
+import GHC.TypeLits
+
+
+type family In     (el :: ke) (cont :: k) :: Bool
+type family Index2 (idx :: i) (cont :: c) :: el
+type family Index  (el :: ke) (cont :: k) :: Maybe Nat
+type family Append (el :: ke) (cont :: k) :: k
+type family Insert (el :: ke) (cont :: k) :: k
+type family Remove (el :: ke) (cont :: k) :: k
+type family Empty             (cont :: k) :: Bool
+type family Size              (cont :: k) :: Nat
+type family Reverse           (cont :: k) :: k
+--type family Head              (cont :: k) :: Maybe *
+
+type family Unique            (cont :: k) :: k
+
+type family Concat (a :: k) (b :: k) :: k
+
+type family Diff  (c :: k) (c' :: k) :: k
+type family Union (c :: k) (c' :: k) :: k
+
+--infixr 6      :<>
+--type family (a :: k) :<> (b :: k) where a :<> b = Concat a b
+
+infixr 6      <>
+type family (a :: k) <> (b :: k) where a <> b = Concat a b
+
+
+
+
+--------------------------------
+
+type family FromJust a where FromJust ('Just a) = a
+type UnsafeIndex el cont = FromJust (Index el cont)
diff --git a/src/Type/Either.hs b/src/Type/Either.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Either.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE PolyKinds #-}
+
+module Type.Either where
+
+import Prelude
+
+
+type family IsLeft (a :: Either l r) :: Bool where IsLeft ('Left  l) = 'True
+                                                   IsLeft ('Right r) = 'False
+
+type family IsRight (a :: Either l r) :: Bool where IsRight ('Left  l) = 'False
+                                                    IsRight ('Right r) = 'True
+
+
+type family FromRight (a :: Either l r) where FromRight ('Right r) = r
+type family FromLeft  (a :: Either l r) where FromLeft  ('Left  l) = l
diff --git a/src/Type/List.hs b/src/Type/List.hs
--- a/src/Type/List.hs
+++ b/src/Type/List.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE ScopedTypeVariables            #-}
 
 module Type.List where
 
@@ -13,16 +14,102 @@
 import GHC.Exts (Constraint)
 import GHC.TypeLits
 import Type.Bool
+import Type.Container
+import qualified Type.Set as Set
 
+-- === Wrappers ===
+
+data Lst (l :: [k])
+
+type family FromLst a where FromLst (Lst l) = l
+
 -- === Basic operations ===
 
-type family Removed    (el :: e) (cont :: c) :: l
+type family Removed    (el :: e)    (cont :: c) :: l
 type family RemovedIdx (idx :: Nat) (cont :: c) :: l
 type family ElAt       (idx :: Nat) (cont :: c) :: l 
 
-type instance Removed (el :: e) ((l ': ls) :: [e]) = If (el :== l) ls (l ': Removed el ls)
+type instance Removed (el :: e) ((l ': ls) :: [e]) = If (el == l) ls (l ': Removed el ls)
 
 
-type instance RemovedIdx idx (l ': ls) = If (idx :== 0) ls (l ': RemovedIdx (idx - 1) ls)
+type instance RemovedIdx idx (l ': ls) = If (idx == 0) ls (l ': RemovedIdx (idx - 1) ls)
 
-type instance ElAt idx (l ': ls) = If (idx :== 0) l (ElAt (idx - 1) ls)
+type instance ElAt idx (l ': ls) = If (idx == 0) l (ElAt (idx - 1) ls)
+
+
+type instance In a (l ': ls) = If (a == l) True (In a ls)
+type instance In a '[]       = False
+
+
+type family SuccMaybe (m :: Maybe Nat) where SuccMaybe (Just n) = Just (n + 1)
+                                             SuccMaybe Nothing  = Nothing
+
+type instance Index a (l ': ls) = If (a == l) (Just 0) (SuccMaybe (Index a ls))
+type instance Index a '[]       = (Nothing :: Maybe Nat)
+
+
+data Recursive a
+
+type instance Index a (Recursive (l ': ls)) = If (a == l) (Just 0) (SuccMaybe (Index a (Recursive ls)))
+type instance Index a (Recursive '[]      ) = (Nothing :: Maybe Nat)
+
+
+--type family Index2 (idx :: i) (cont :: c) :: el
+
+type instance Index2 n (a ': as) = If (n == 0) a (Index2 (n - 1) as)
+
+
+type instance Empty '[]       = 'True
+type instance Empty (a ': as) = 'False
+
+
+type instance Append a '[]       = '[a]
+type instance Append a (l ': ls) = l ': Append a ls
+
+
+type instance Concat (lst :: [k]) ('[]       :: [k]) = lst
+type instance Concat (lst :: [k]) ((l ': ls) :: [k]) = Concat (Append l lst) ls
+
+
+type instance Remove a '[] = '[]
+type instance Remove a (l ': ls) = If (a == l) ls (l ': Remove a ls)
+
+
+type instance Diff l '[]       = l
+type instance Diff l (e ': es) = Diff (Remove e l) es
+
+type instance Size '[]       = 0
+type instance Size (a ': as) = 1 + Size as
+
+type family Head lst where
+    Head '[]       = 'Nothing
+    Head (a ': as) = 'Just a
+
+type family Head' lst where Head' (a ': as) = a
+
+--type instance Unique (lst :: [k]) = Set.ToList (Set.AsSet lst)
+
+-- FIXME[WD]: The following is just an fix for using Unique. 
+--            Due to lack of time this ugly fix has no background - probably some PolyKinded problem.
+type family UniqueFix lst where UniqueFix '[] = '[]
+                                UniqueFix lst = Unique lst
+type instance Unique (lst :: [k]) = Set.ToList (Set.AsSet lst)
+
+type instance Reverse (lst :: [k]) = Reverse' lst '[]
+
+type family Reverse' lst lst' where
+    Reverse' '[] lst = lst
+    Reverse' (l ': ls) lst = Reverse' ls (l ': lst)
+
+
+type family Take (n :: Nat) lst where
+	Take 0 lst       = '[]
+	Take n (l ': ls) = l ': Take (n - 1) ls
+
+--type instance Index (a :: *) (Recursive ((l ': ls) ::  [*] )) = If (a == l) (Just 0) (SuccMaybe (Index a (Recursive ls)))
+--type instance Index (a :: *) (Recursive ((l ': ls) :: [[*]])) = If (Index a l == 'Nothing) (SuccMaybe (Index a (Recursive ls))) ('Just 0)
+--type instance Index a '[]                                     = 'Nothing
+
+
+--type instance RecIndex a ((l ': ls) :: [[*]]) = If (RecIndex a l == 'Nothing) (SuccMaybe (RecIndex a ls)) (Just 0)
+
diff --git a/src/Type/Map.hs b/src/Type/Map.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Map.hs
@@ -0,0 +1,9 @@
+{-# LANGUAGE PolyKinds #-}
+
+module Type.Map where
+
+data Map k v = Map [(k,v)]
+
+type family MapLookup (k :: kk) (m :: Map kk kv) :: kv where
+    MapLookup k ('Map ( '(k, v) ': ms )) = v
+    MapLookup k ('Map ( '(l, v) ': ms )) = MapLookup k ('Map ms)
diff --git a/src/Type/Maybe.hs b/src/Type/Maybe.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Maybe.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE PolyKinds #-}
+
+module Type.Maybe where
+
+import Prelude
+
+type family IsJust a where IsJust ('Just a) = 'True
+                           IsJust a         = 'False
+
+
+type family CatMaybes (lst :: [Maybe k]) :: [k] where
+    CatMaybes '[]              = '[]
+    CatMaybes ('Just a  ': ms) = a ': CatMaybes ms
+    CatMaybes ('Nothing ': ms) =      CatMaybes ms
diff --git a/src/Type/Operators.hs b/src/Type/Operators.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Operators.hs
@@ -0,0 +1,25 @@
+
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE EmptyDataDecls       #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds            #-}
+
+module Type.Operators where
+
+import Data.Typeable
+import Prelude
+import GHC.Exts (Constraint)
+import GHC.TypeLits
+import Type.Bool
+import Type.Container
+import Type.Wrapped
+
+
+
+infixr 0 $
+type f $ a = f a
+
+infixl 1 &
+type a & f = f a
diff --git a/src/Type/Promotion.hs b/src/Type/Promotion.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Promotion.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE PolyKinds #-}
+
+module Type.Promotion where
+
+import Prelude
+
+import Data.Typeable
+import GHC.TypeLits
+
+
+-- === Promotion classes ===
+
+class Known (t :: k) (val :: *) where typeVal :: Proxy t -> val
+--type family TypeVal (t :: k) :: *
+--type Known' t = Known t (TypeVal t)
+
+
+
+-- === Basic instances ===
+
+-- Nat
+instance (Num i, KnownNat t) => Known (t :: Nat) i where typeVal = fromIntegral . natVal
+
+-- Bool
+--type instance TypeVal (k :: Bool) = Bool
+instance val ~ Bool => Known True  val where typeVal _ = True
+instance val ~ Bool => Known False val where typeVal _ = False
+
+-- Maybe a
+--type instance TypeVal ('Just a) = Maybe (TypeVal a)
+instance val ~ Maybe a              => Known 'Nothing  val where typeVal _ = Nothing
+instance (val ~ Maybe a, Known t a) => Known ('Just t) val where typeVal _ = Just $ typeVal (Proxy :: Proxy t)
+
+-- Either l r
+instance (val ~ Either l r, Known t l) => Known ('Left  t) val where typeVal _ = Left  $ typeVal (Proxy :: Proxy t)
+instance (val ~ Either l r, Known t r) => Known ('Right t) val where typeVal _ = Right $ typeVal (Proxy :: Proxy t)
+
+-- Lists
+instance Known ('[]) [a] where typeVal _ = []
+instance (Known t a, Known ts [a]) => Known (t ': ts) [a] where typeVal _ = typeVal (Proxy :: Proxy t) : typeVal (Proxy :: Proxy ts)
diff --git a/src/Type/Sequence.hs b/src/Type/Sequence.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Sequence.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Type.Sequence where
+
+import Prelude
+import GHC.TypeLits
+
+type family Succ (a :: k) :: k
+
+type instance Succ (a :: Nat) = a + 1
+
+
+type family Empty :: k
+
+type instance Empty = '[]
+
+
+type family Zero :: k
+
+type instance Zero = 0
+
+
+
+type family Range (begin :: k) (end :: k) :: [k] where
+    Range b b = Empty
+    Range b e = b ': Range (Succ b) e
+
+type family Enumerate end where Enumerate end = Range Zero end -- Implemented as TF because #11375
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,50 @@
+
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE EmptyDataDecls       #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds            #-}
+
+module Type.Set where
+
+import Data.Typeable
+import Prelude
+import GHC.Exts (Constraint)
+import GHC.TypeLits
+import Type.Bool
+import Type.Container
+import Type.Wrapped
+import Type.Operators
+
+
+-- === Declarations ===
+
+data Set (a :: [k])
+
+type instance Unwrapped (Set a) = a
+
+
+-- === Conversions ===
+
+type family AsSet  (a :: k)
+type family AsSet' (a :: k)
+
+type instance AsSet (lst :: [k]) = AsSet' (Reverse lst)
+type instance AsSet' '[]         = Set '[]
+type instance AsSet' (l ': ls)   = Insert l (AsSet' ls)
+
+type family ToList s where ToList (Set s) = s
+
+
+
+-- === Operations ===
+
+
+type instance Insert a (Set '[])       = Set '[a]
+type instance Insert a (Set (s ': ss)) = Set $ If (a == s) (s ': ss) (s ': Unwrapped (Insert a (Set ss)))
+
+type instance Concat (Set set) (Set '[]) = Set set
+type instance Concat (Set set) (Set (s ': ss)) = If (s `In` set) (Concat (Set set) (Set ss)) (Concat (Insert s (Set set)) (Set ss))
+
+type instance Index a (Set s) = Index a s
diff --git a/src/Type/Show.hs b/src/Type/Show.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Show.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE PolyKinds            #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Type.Show where
+
+import Prelude
+import Data.Typeable
+import Data.Monoid
+import GHC.TypeLits
+import Text.Show.Pretty (ppValue, parseValue)
+import Text.PrettyPrint (Doc, text)
+import GHC.Exts         (Constraint)
+
+--showType :: Typeable a => a -> String
+--showType (a :: a) = showProxyType (Proxy :: Proxy a)
+
+--showProxyType :: Typeable (Proxy a) => Proxy a -> String
+--showProxyType = clear . drop 6 . show . typeOf where
+--    clear = \case ('(':s)     -> init  s
+--                  ('*':' ':s) -> clear s -- PolyKinded Proxies are shown as "Proxy *"
+--                  s           -> s
+
+
+class TypeShow a where showType :: Proxy (a :: k) -> String
+
+printType :: TypeShow a => Proxy a -> IO ()
+printType = putStrLn . showType
+
+ppPrintType :: TypeShow a => Proxy a -> IO ()
+ppPrintType = putStrLn . ppShowType
+
+ppShowType :: TypeShow a => Proxy a -> String
+ppShowType = show . ppTypeDoc
+
+ppTypeDoc :: TypeShow a => Proxy a -> Doc
+ppTypeDoc a = case parseValue txt of
+            Just v  -> ppValue v
+            Nothing -> text txt
+  where txt = showType a
+
+
+
+-- === Basic Instances === --
+
+instance KnownNat n               => TypeShow (n :: Nat) where showType _ = show $ natVal (Proxy :: Proxy n)
+instance ListElemsShow a          => TypeShow (a :: [k]) where showType _ = "[" <> showListElems (Proxy :: Proxy a) <> "]"
+instance (TypeShow a, TypeShow b) => TypeShow '(a,b)     where showType _ = "(" <> showType (Proxy :: Proxy a) <> ", " <> showType (Proxy :: Proxy b) <> ")"
+
+
+-- === List Helpers === --
+
+class                                                           ListElemsShow a         where showListElems :: Proxy a -> String
+instance {-# OVERLAPPABLE #-}                                   ListElemsShow '[]       where showListElems _ = ""
+instance {-# OVERLAPPABLE #-}  TypeShow a                    => ListElemsShow '[a]      where showListElems _ = showType (Proxy :: Proxy a)
+instance {-# OVERLAPPABLE #-} (TypeShow a, ListElemsShow as) => ListElemsShow (a ': as) where showListElems _ = showType (Proxy :: Proxy a) <> ", " <> showListElems (Proxy :: Proxy as)
+
diff --git a/src/Type/Wrapped.hs b/src/Type/Wrapped.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Wrapped.hs
@@ -0,0 +1,20 @@
+
+{-# LANGUAGE DeriveDataTypeable   #-}
+{-# LANGUAGE EmptyDataDecls       #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE PolyKinds            #-}
+
+module Type.Wrapped where
+
+import Data.Typeable
+import Prelude
+import GHC.Exts (Constraint)
+import GHC.TypeLits
+import Type.Bool
+import Type.Container
+
+-- === Basic operations ===
+
+type family Unwrapped (a :: k) :: l
diff --git a/src/Type/Zip.hs b/src/Type/Zip.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Zip.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Type.Zip where
+
+
+type family Zip lst lst' where Zip lst lst' = ZipWith '(,) lst lst' -- Implemented as TF because #11375
+
+type family ZipWith f lst lst' where
+    ZipWith f '[]       lst       = '[]
+    ZipWith f lst       '[]       = '[]
+    ZipWith f (l ': ls) (n ': ns) = f l n ': ZipWith f ls ns
diff --git a/typelevel.cabal b/typelevel.cabal
--- a/typelevel.cabal
+++ b/typelevel.cabal
@@ -1,5 +1,11 @@
+---------------------------------------------------
+-- This is a generated cabal configuration file. --
+-- DO NOT EDIT!                                  --
+-- Use gencabal instead.                         --
+---------------------------------------------------
+
 name:                typelevel
-version:             1.0.2
+version:             1.0.4
 synopsis:            Useful type level operations (type families and related operators).
 -- description:         
 license:             Apache-2.0
@@ -45,8 +51,22 @@
                       ViewPatterns
                       TypeFamilies
   
-  exposed-modules:    Constraint.Container.Homo 
-                    , Type.Bool
-                    , Type.List
+  Exposed-modules: 
+        Constraint.Container.Homo,
+        Type.Bool,
+        Type.Container,
+        Type.Either,
+        Type.List,
+        Type.Map,
+        Type.Maybe,
+        Type.Operators,
+        Type.Promotion,
+        Type.Sequence,
+        Type.Set,
+        Type.Show,
+        Type.Wrapped,
+        Type.Zip
 
   build-depends:      base >=4.6 && <4.9
+                    , pretty-show
+                    , pretty