diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2014 Patrick Bahr
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. 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.
+
+3. Neither the name of the author nor the names of his contributors
+   may be used to endorse or promote products derived from this software
+   without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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/projection.cabal b/projection.cabal
new file mode 100644
--- /dev/null
+++ b/projection.cabal
@@ -0,0 +1,32 @@
+Name:			projection
+Version:		0.1
+Synopsis:            	Projection function for arbitrarily nested binary product types.
+Description:
+  This package implements a projection function for arbitrarily nested
+  binary product types. The implementation is based on closed type
+  families and follows the approach described in the paper /Composing
+  and Decomposing Data Types/ (Workshop on Generic Programming, 2014,
+  to appear).
+
+
+Category:               Generics
+License:                BSD3
+License-file:           LICENSE
+Author:                 Patrick Bahr
+Maintainer:             paba@di.ku.dk
+Build-Type:             Simple
+Cabal-Version:          >=1.9.2
+bug-reports:            https://github.com/pa-ba/projection/issues
+
+
+library
+  Exposed-Modules:      Data.Projection
+  Build-Depends:	base >= 4.7, base < 5
+  hs-source-dirs:	src
+  ghc-options:          -W
+
+
+source-repository head
+  type:     git
+  location: https://github.com/pa-ba/projection
+
diff --git a/src/Data/Projection.hs b/src/Data/Projection.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Projection.hs
@@ -0,0 +1,82 @@
+{-# LANGUAGE ConstraintKinds       #-}
+{-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE FlexibleContexts      #-}
+{-# LANGUAGE FlexibleInstances     #-}
+{-# LANGUAGE GADTs                 #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds             #-}
+{-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TypeFamilies          #-}
+{-# LANGUAGE TypeOperators         #-}
+{-# LANGUAGE UndecidableInstances  #-}
+
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Projection
+-- Copyright   :  (c) 2014 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@di.ku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+--
+-- This module provides a generic projection function 'pr' for
+-- arbitrary nested binary products.
+--
+--------------------------------------------------------------------------------
+
+
+module Data.Projection (pr, (:<)) where
+
+import Prelude hiding (Either (..))
+
+data Pos = Here | Left Pos | Right Pos
+
+data RPos = NotFound | Ambiguous | Found Pos
+
+type family Ch (l :: RPos) (r :: RPos) :: RPos where
+    Ch (Found x) (Found y) = Ambiguous
+    Ch Ambiguous y = Ambiguous
+    Ch x Ambiguous = Ambiguous
+    Ch (Found x) y = Found (Left x)
+    Ch x (Found y) = Found (Right y)
+    Ch x y = NotFound
+
+type family Elem (e :: *) (p :: *) :: RPos where
+    Elem e e = Found Here
+    Elem e (l,r) = Ch (Elem e l) (Elem e r)
+    Elem e p = NotFound
+
+data Pointer (pos :: RPos) e p where
+    Phere :: Pointer (Found Here) e e
+    Pleft :: Pointer (Found pos) e p -> Pointer (Found (Left pos)) e (p,p')
+    Pright :: Pointer (Found pos) e p -> Pointer (Found (Right pos)) e (p',p)
+
+class GetPointer (pos :: RPos) e p where
+    pointer :: Pointer pos e p
+
+instance GetPointer (Found Here) e e where
+    pointer = Phere
+
+instance GetPointer (Found pos) e p => GetPointer (Found (Left pos)) e (p, p') where
+    pointer = Pleft pointer
+
+instance GetPointer (Found pos) e p => GetPointer (Found (Right pos)) e (p', p) where
+    pointer = Pright pointer
+
+pr' :: Pointer pos e p -> p -> e
+pr' Phere e = e
+pr' (Pleft p) (x,_) = pr' p x
+pr' (Pright p) (_,y) = pr' p y
+
+
+-- | The constraint @e :< p@ expresses that @e@ is a component of the
+-- type @p@. That is, @p@ is formed by binary products using the type
+-- @e@. The occurrence of @e@ must be unique. For example we have @Int
+-- :< (Bool,(Int,Bool))@ but not @Bool :< (Bool,(Int,Bool))@.
+type (e :< p) = GetPointer (Elem e p) e p
+
+-- | This function projects the component of type @e@ out or the
+-- compound value of type @p@.
+
+pr :: forall e p . (e :< p) => p -> e
+pr p = pr' (pointer :: Pointer (Elem e p) e p) p