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/instant-zipper.cabal b/instant-zipper.cabal
new file mode 100644
--- /dev/null
+++ b/instant-zipper.cabal
@@ -0,0 +1,18 @@
+name:                instant-zipper
+version:             0.0.0
+category:            Generics
+synopsis:            Heterogenous Zipper in Instant Generics
+description:         This package contains a heterogenous Zipper and 2
+                     examples of how to use it.
+license:             GPL
+author:              Bram Schuur, Ruud Koot
+maintainer:          B.Schuur@students.uu.nl, R.Koot@students.uu.nl
+build-depends:       base >= 4.0, base < 5.0, instant-generics, mtl
+
+build-type:         Simple
+hs-source-dirs : src
+exposed-modules :    Generics.Instant.Zipper
+                     Generics.Instant.Zipper.Example.Dept
+                     Generics.Instant.Zipper.Example.Term
+
+
diff --git a/src/Generics/Instant/Zipper.hs b/src/Generics/Instant/Zipper.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Instant/Zipper.hs
@@ -0,0 +1,372 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE EmptyDataDecls     #-}
+{-# LANGUAGE FlexibleContexts   #-}
+{-# LANGUAGE GADTs              #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TupleSections      #-}
+{-# LANGUAGE TypeFamilies       #-}
+{-# LANGUAGE TypeOperators      #-}
+
+{-# OPTIONS_GHC -Wall           #-}
+
+module Generics.Instant.Zipper (
+    module Control.Monad.Error,
+    module Data.Typeable,
+    module Generics.Instant,
+--    module Generics.Instant.TH,
+--    module Generics.Instant.Zipper.TH,
+    -- *
+    Family,
+    Zipper,
+    ZipperR,
+    -- *
+    enter,
+    leave,
+    up,
+    down,
+    downR,
+    left,
+    right,
+    down',
+    downR',
+    left',
+    right',
+    get,
+    set,
+    -- *
+    PrimFam(..)
+) where
+
+import Prelude hiding (last)
+
+import Control.Applicative
+import Control.Monad.Error
+
+import Data.Maybe
+import Data.Typeable
+
+import Generics.Instant
+--import Generics.Instant.TH
+
+--import Generics.Instant.Zipper.TH
+
+-- | Type-level list
+
+data Epsilon
+data c :<: cs
+
+infixr 5 :<:
+
+-- | Loc and Context
+
+data Loc hole root c = Loc { focus :: hole, context :: Context hole root c }
+
+data Context hole root l where
+    Empty :: Context hole hole Epsilon
+    Push  :: (Zipper parent) => Derivative (Rep parent)
+                             -> Context parent root cs
+                             -> Context hole root (parent :<: cs)
+
+type ZipperR = Either String
+
+-- | Families
+
+class Family (f :: * -> *)
+
+data PrimFam a where
+    Char  ::                                  PrimFam Char
+    Int   ::                                  PrimFam Int
+    Float ::                                  PrimFam Float
+    List  :: (Family f, Show (f a)) => f a -> PrimFam [a]
+    
+deriving instance Show (PrimFam a)
+
+instance Family PrimFam
+
+-- | Zipper
+
+class ( Representable  f
+      , Typeable       f
+      , Fillable  (Rep f)
+      , Firstable (Rep f)
+      , Nextable  (Rep f)
+      , Lastable  (Rep f)
+      , Prevable  (Rep f) ) => Zipper f
+
+instance Zipper Int
+instance Zipper Char
+instance Zipper Float
+instance (Zipper a) => Zipper [a]
+
+-- | Differentiable
+
+class Differentiable f where
+    data Derivative f :: * 
+    
+instance Differentiable U where
+    data Derivative U
+    
+instance (Differentiable f, Differentiable g) => Differentiable (f :+: g) where
+    data Derivative (f :+: g) = CL (Derivative f)
+                              | CR (Derivative g)
+    
+instance (Differentiable f, Differentiable g) => Differentiable (f :*: g) where
+    data Derivative (f :*: g) = C1 (Derivative f) g
+                              | C2 f (Derivative g)
+    
+instance (Differentiable a) => Differentiable (Rec a) where
+    data Derivative (Rec a) = CRec
+    
+instance (Differentiable a) => Differentiable (Var a) where
+    data Derivative (Var a) = CVar
+    
+instance (Differentiable f) => Differentiable (C c f) where
+    data Derivative (C c f) = CC (Derivative f)
+
+-- | Fill
+
+class Fillable f where
+    fill :: (Typeable a) => Derivative f -> a -> Maybe f
+
+instance Fillable U where
+    fill = error "impossible"
+
+instance Fillable Char where
+    fill = error "impossible"
+
+instance Fillable Int where
+    fill = error "impossible"
+
+instance Fillable Float where
+    fill = error "impossible"
+            
+instance (Fillable f, Fillable g) => Fillable (f :+: g) where
+    fill (CL l) v = L <$> fill l v
+    fill (CR r) v = R <$> fill r v
+
+instance (Fillable f, Fillable g) => Fillable (f :*: g) where
+    fill (C1 c r) v = flip (:*:) r <$> fill c v
+    fill (C2 l c) v = (l :*:) <$> fill c v
+
+instance (Typeable a) => Fillable (Rec a) where
+    fill CRec v = Rec <$> cast v
+    
+instance (Typeable a) => Fillable (Var a) where
+    fill CVar v = Var <$> cast v
+
+instance (Fillable f) => Fillable (C c f) where
+    fill (CC c) v = C <$> fill c v
+    
+   
+-- | First
+
+class Firstable f where
+    first :: (Zipper a) => f -> Maybe (a, Derivative f)
+
+instance Firstable U where
+    first _ = Nothing
+
+instance Firstable Char where
+    first _ = Nothing
+
+instance Firstable Int where
+    first _ = Nothing
+    
+instance Firstable Float where
+    first _ = Nothing
+            
+instance (Firstable f, Firstable g) => Firstable (f :+: g) where
+    first (L x)     = fmap CL <$> first x
+    first (R y)     = fmap CR <$> first y
+
+instance (Firstable f, Firstable g) => Firstable (f :*: g) where
+    first (l :*: r) =  fmap (flip C1 r) <$> first l
+                   <|> fmap (     C2 l) <$> first r
+
+instance (Typeable f) => Firstable (Rec f) where
+    first (Rec v) = (, CRec) <$> cast v
+
+instance (Typeable f) => Firstable (Var f) where
+    first (Var v) = (, CVar) <$> cast v
+
+instance (Firstable f) => Firstable (C c f) where
+    first (C v)   = fmap CC <$> first v
+
+-- | Last
+
+class Lastable f where
+    last :: (Zipper a) => f -> Maybe (a, Derivative f)
+
+instance Lastable U where
+    last _ = Nothing
+
+instance Lastable Char where
+    last _ = Nothing
+
+instance Lastable Int where
+    last _ = Nothing
+    
+instance Lastable Float where
+    last _ = Nothing
+            
+instance (Lastable f, Lastable g) => Lastable (f :+: g) where
+    last (L x) = fmap CL <$> last x
+    last (R y) = fmap CR <$> last y
+
+instance (Lastable f, Lastable g) => Lastable (f :*: g) where
+    last (l :*: r) =  fmap (     C2 l) <$> last r
+                  <|> fmap (flip C1 r) <$> last l
+
+instance (Typeable f) => Lastable (Rec f) where
+    last (Rec v) = (, CRec) <$> cast v
+
+instance (Typeable f) => Lastable (Var f) where
+    last (Var v) = (, CVar) <$> cast v
+
+instance (Lastable f) => Lastable (C c f) where
+    last (C v) = fmap CC <$> last v
+    
+-- | Next
+
+class Nextable f where
+    next :: (Typeable a, Zipper b) => Derivative f -> a -> Maybe (b, Derivative f)
+    
+instance Nextable U where
+    next _ _ = Nothing
+
+instance Nextable Char where
+    next _ _ = Nothing
+
+instance Nextable Int where
+    next _ _ = Nothing
+
+instance Nextable Float where
+    next _ _ = Nothing
+
+instance (Nextable f, Nextable g) => Nextable (f :+: g) where
+    next (CL c) x = fmap CL <$> next c x
+    next (CR c) y = fmap CR <$> next c y
+
+instance (Nextable f, Nextable g, Fillable f, Firstable g) => Nextable (f :*: g) where
+    next (C1 c y) x = fmap (flip C1 y) <$> next c x
+                   <|> (\x' (y',c') -> (y', C2 x' c')) <$> fill c x <*> first y
+    next (C2 x c) y = fmap (C2 x) <$> next c y 
+
+instance Nextable (Rec f) where
+    next CRec _ = Nothing
+
+instance Nextable (Var f) where
+    next CVar _ = Nothing
+
+instance (Nextable f) => Nextable (C c f) where
+    next (CC v) x = fmap CC <$> next v x
+
+-- | Prev
+
+class Prevable f where
+    prev :: (Typeable a, Zipper b) => Derivative f -> a -> Maybe (b, Derivative f)
+    
+instance Prevable U where
+    prev _ _ = Nothing
+
+instance Prevable Char where
+    prev _ _ = Nothing
+
+instance Prevable Int where
+    prev _ _ = Nothing
+
+instance Prevable Float where
+    prev _ _ = Nothing
+
+instance (Prevable f, Prevable g) => Prevable (f :+: g) where
+    prev (CL c) x = fmap CL <$> prev c x
+    prev (CR c) y = fmap CR <$> prev c y
+
+instance (Lastable f, Fillable g, Prevable f, Prevable g) => Prevable (f :*: g) where
+    prev (C1 c y) x = fmap (flip C1 y) <$> prev c x                    
+    prev (C2 x c) y = fmap (     C2 x) <$> prev c y 
+                   <|> (\x' (y',c') -> (y', C1 c' x')) <$> fill c y <*> last x
+
+instance Prevable (Rec f) where
+    prev CRec _ = Nothing
+
+instance Prevable (Var f) where
+    prev CVar _ = Nothing
+
+instance (Prevable f) => Prevable (C c f) where
+    prev (CC v) x = fmap CC <$> prev v x
+
+-- | Navigation
+
+get :: Loc h r c -> h
+get = focus
+
+set :: h -> Loc h r c -> Loc h r c
+set v (Loc _ cs) = Loc v cs
+
+leave :: (Zipper h) => Loc h r c -> r
+leave (Loc h Empty) = h
+leave loc@(Loc _ (Push _ _)) = leave . up  $ loc
+
+enter :: Zipper h => h -> Loc h h Epsilon
+enter h = Loc h Empty
+
+
+up :: (Zipper h, Zipper h') => Loc h r (h' :<: c) -> Loc h' r c
+up (Loc h (Push c cs))   = fromJust $ (\x -> Loc (to x) cs) <$> fill c h
+
+-- | Down left
+
+downL_ :: (Zipper h, Zipper h') => Loc h r c -> ZipperR (Loc h' r (h :<: c))
+downL_ (Loc h cs) = maybe (Left "Error going down left") (\(h', c) -> Right (Loc h' (Push c cs))) $ first (from h)
+
+downL' :: (Zipper h, Zipper h') => h' -> Loc h r c -> ZipperR (Loc h' r (h :<: c))
+downL' _ = downL_
+
+downL :: (Zipper h, Zipper h', Family f, Show (f h')) => f h' -> Loc h r c -> ZipperR (Loc h' r (h :<: c))
+downL v = either (Left . (++ " with type " ++ show v)) Right . downL_
+
+-- | Down 
+
+--down_ :: (Zipper h, Zipper h') => Loc h r c -> ZipperR (Loc h' r (h :<: c))
+--down_ = downL_
+
+down' :: (Zipper h, Zipper h') => h' -> Loc h r c -> ZipperR (Loc h' r (h :<: c))
+down' = downL'
+
+down :: (Zipper h, Zipper h', Family f, Show (f h')) => f h' -> Loc h r c -> ZipperR (Loc h' r (h :<: c))
+down = downL
+
+-- | Down Right
+
+downR_ :: (Zipper h, Zipper h') => Loc h r c -> ZipperR (Loc h' r (h :<: c))
+downR_ (Loc h cs) = maybe (Left "Error going down right") (\(h', c) -> Right (Loc h' (Push c cs))) $ last (from h)
+
+downR' :: (Zipper h, Zipper h') => h' -> Loc h r c -> ZipperR (Loc h' r (h :<: c))
+downR' _ = downR_ 
+
+downR :: (Zipper h, Zipper h', Family f, Show (f h')) => f h' -> Loc h r c -> ZipperR (Loc h' r (h :<: c))
+downR v = either (Left . (++ " with type " ++ show v)) Right . downR_
+
+-- | Right
+
+right_ :: (Zipper h, Zipper h') => Loc h r (c :<: cs) -> ZipperR (Loc h' r (c :<: cs))
+right_ (Loc h (Push c cs)) = maybe (Left "Error going right") (\(h', c') -> Right (Loc h' (Push c' cs))) $ next c h
+
+right' :: (Zipper h, Zipper h') => h' -> Loc h r (c :<: cs) -> ZipperR (Loc h' r (c :<: cs))
+right' _ = right_
+
+right :: (Zipper h, Zipper h', Family f, Show (f h')) => f h' -> Loc h r (c :<: cs) -> ZipperR (Loc h' r (c :<: cs))
+right v = either (Left . (++ " with type " ++ show v)) Right . right_
+
+-- | Left
+
+left_ :: (Zipper h, Zipper h') => Loc h r (c :<: cs) -> ZipperR (Loc h' r (c :<: cs))
+left_ (Loc h (Push c cs)) = maybe (Left "Error going left") (\(h', c') -> Right (Loc h' (Push c' cs))) $ prev c h
+
+left' :: (Zipper h, Zipper h') => h' -> Loc h r (c :<: cs) -> ZipperR (Loc h' r (c :<: cs))
+left' _ = left_
+
+left :: (Zipper h, Zipper h', Family f, Show (f h')) => f h' -> Loc h r (c :<: cs) -> ZipperR (Loc h' r (c :<: cs))
+left v = either (Left . (++ " with type " ++ show v)) Right . left_
+
diff --git a/src/Generics/Instant/Zipper/Example/Dept.hs b/src/Generics/Instant/Zipper/Example/Dept.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Instant/Zipper/Example/Dept.hs
@@ -0,0 +1,76 @@
+{-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE EmptyDataDecls            #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE TemplateHaskell           #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE TypeOperators             #-}
+{-# LANGUAGE TypeSynonymInstances      #-}
+{-# LANGUAGE StandaloneDeriving        #-}
+
+module Generics.Instant.Zipper.Example.Dept where
+
+import Generics.Instant.Zipper
+import Generics.Instant.TH
+
+-- | Datatype
+
+type Salary    = Float
+type Manager   = Employee
+type Name      = String
+
+data Dept = D Manager [Employee]
+    deriving (Eq, Show, Typeable)
+
+data Employee = E Name Salary
+    deriving (Eq, Show, Typeable)
+
+-- | Representation
+
+$(deriveAll ''Dept)
+$(deriveAll ''Employee)
+
+-- | Family
+
+data DeptFam a where
+    Dept     :: DeptFam Dept
+    Employee :: DeptFam Employee
+    Salary   :: DeptFam Salary
+    Name     :: DeptFam Name
+
+deriving instance Show (DeptFam a)
+    
+instance Family DeptFam
+
+-- | Zipper
+
+instance Zipper Dept
+instance Zipper Employee
+    
+-- | Example
+
+dept :: Dept
+dept = D doaitse [johan, sean, pedro]
+    where doaitse, johan, sean, pedro :: Employee
+          doaitse  = E "Doaitse"  8000
+          johan    = E "Johan"    8000
+          sean     = E "Sean"     2600
+          pedro    = E "Pedro"    2400
+
+fixDept :: ZipperR Dept
+fixDept =  return (enter dept)
+        >>= down  Employee
+        >>= down  Name
+        >>= return . set "Prof. dr. Swierstra"
+        >>= right Salary
+        >>= return . set 9000.0
+        >>= return . up
+        >>= return . up
+        >>= downR (List Employee)
+        >>= down  (List Employee)
+        >>= down  (List Employee)
+        >>= down  Employee
+        >>= downR Salary
+        >>= return . set 100.0
+        >>= return . leave
+
diff --git a/src/Generics/Instant/Zipper/Example/Term.hs b/src/Generics/Instant/Zipper/Example/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/Instant/Zipper/Example/Term.hs
@@ -0,0 +1,86 @@
+{-# LANGUAGE EmptyDataDecls            #-}
+{-# LANGUAGE GADTs                     #-}
+{-# LANGUAGE TypeFamilies              #-}
+{-# LANGUAGE TypeOperators             #-}
+{-# LANGUAGE DeriveDataTypeable        #-}
+{-# LANGUAGE NoMonomorphismRestriction #-}
+{-# LANGUAGE StandaloneDeriving        #-}
+{-# LANGUAGE TemplateHaskell           #-}
+{-# LANGUAGE TypeSynonymInstances      #-}
+
+module Generics.Instant.Zipper.Example.Term where
+
+import Data.Maybe
+import Data.Typeable
+
+import Generics.Instant
+import Generics.Instant.TH
+import Generics.Instant.Zipper
+
+-- | Datatype
+
+data Term
+    =  Var'     String
+    |  Lambda   String  Term
+    |  App      Term    Term
+    |  If       Term    Term Term
+    deriving (Eq, Show, Typeable)
+
+-- | Representation
+
+{-
+instance Representable Term where
+    type Rep Term = (Var String)
+                :+: (Var String :*: Rec Term)
+                :+: (Rec Term :*: Rec Term)
+                :+: (Rec Term :*: Rec Term :*: Rec Term)
+
+    from (Var'  s)      =       L (Var s)
+    from (Lambda s t)  =    R (L (Var s :*: Rec t))
+    from (App t1 t2)   = R (R (L (Rec t1 :*: Rec t2)))
+    from (If t1 t2 t3) = R (R (R (Rec t1 :*: Rec t2 :*: Rec t3)))
+    
+    to (L (Var s)                               ) = Var' s
+    to (R (L (Var s :*: Rec t))                 ) = Lambda s t
+    to (R (R (L (Rec t1 :*: Rec t2)))           ) = App t1 t2
+    to (R (R (R (Rec t1 :*: Rec t2 :*: Rec t3)))) = If t1 t2 t3
+-}
+
+$(deriveAll ''Term)
+
+-- | Family
+
+data TermFam a where
+    Term   :: TermFam Term
+    String :: TermFam String
+
+deriving instance Show (TermFam a)
+    
+instance Family TermFam
+
+-- | Zipper
+
+instance Zipper Term
+    
+-- | fac
+
+fac = Lambda "n"
+     (If  (App (App (Var' "=") (Var' "n")) (Var' "0"))
+         (Var' "1")
+         (App  (App (Var' "+") (Var' "n"))
+               (App  (Var' "fac")
+                     (App (Var' "pred") (Var' "n")))))
+
+
+fixFac :: ZipperR Term 
+fixFac =  return (enter fac)
+      >>= down  Term
+      >>= down  Term
+      >>= right Term
+      >>= right Term
+      >>= down  Term
+      >>= down  Term
+      >>= down  String
+      >>= return . set "*"
+      >>= return . leave
+