diff --git a/Data/Comp/Multi/Strategic.hs b/Data/Comp/Multi/Strategic.hs
new file mode 100644
--- /dev/null
+++ b/Data/Comp/Multi/Strategic.hs
@@ -0,0 +1,213 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeOperators #-}
+
+module Data.Comp.Multi.Strategic
+  (
+    -- * Rewrites
+    RewriteM
+  , Rewrite
+  , GRewriteM
+  , GRewrite
+  , addFail
+  , tryR
+  , promoteR
+  , promoteRF
+  , allR
+  , (>+>)
+  , (+>)
+  , anyR
+  , oneR
+  , alltdR
+  , allbuR
+  , anytdR
+  , anybuR
+  , prunetdR
+  , onetdR
+  , onebuR
+
+    -- * Translations
+  , Translate
+  , TranslateM
+  , GTranslateM
+  , promoteTF
+  , mtryM
+  , onetdT
+  , foldtdT
+  , crushtdT
+  ) where
+
+import Control.Applicative ( Applicative, (<*) )
+
+import Control.Monad ( MonadPlus(..), liftM, liftM2, (>=>) )
+import Control.Monad.Identity ( Identity )
+import Control.Monad.Trans ( lift )
+import Control.Monad.Trans.Maybe ( MaybeT, runMaybeT )
+import Control.Monad.State ( StateT, runStateT, get, put )
+import Control.Monad.Writer ( WriterT, runWriterT, tell )
+
+import Data.Comp.Multi ( Cxt(..), Term, unTerm )
+import Data.Comp.Multi.Generic ( query )
+import Data.Comp.Multi.HFoldable ( HFoldable )
+import Data.Comp.Multi.HTraversable ( HTraversable, hmapM )
+import Data.Monoid ( Monoid, mappend, mempty, Any(..) )
+import Data.Type.Equality ( (:~:)(..), sym )
+
+import Data.Comp.Multi.Strategy.Classification
+
+--------------------------------------------------------------------------------
+
+-- Porting from the old type-equality library to the new base Data.Type.Equality
+-- Haven't yet looked into rewriting with gcastWith instead
+
+subst :: (a :~: b) -> f a -> f b
+subst Refl x = x
+
+subst2 :: (a :~: b) -> f (g a) -> f (g b)
+subst2 Refl x = x
+
+--------------------------------------------------------------------------------
+
+type RewriteM m f l = f l -> m (f l)
+type Rewrite f l = RewriteM Identity f l
+type GRewriteM m f = forall l. RewriteM m f l
+type GRewrite f = GRewriteM Identity f
+
+--------------------------------------------------------------------------------
+-- Rewrites
+--------------------------------------------------------------------------------
+
+type AnyR m = WriterT Any m
+
+wrapAnyR :: (Applicative m, MonadPlus m) => RewriteM m f l -> RewriteM (AnyR m) f l
+wrapAnyR f t = (lift (f t) <* tell (Any True)) `mplus` return t
+
+unwrapAnyR :: MonadPlus m => RewriteM (AnyR m) f l -> RewriteM m f l
+unwrapAnyR f t = do (t', Any b) <- runWriterT (f t)
+                    if b then
+                      return t'
+                     else
+                      mzero
+
+--------------------------------------------------------------------------------
+
+type OneR m = StateT Bool m
+
+wrapOneR :: (Applicative m, MonadPlus m) => RewriteM m f l -> RewriteM (OneR m) f l
+wrapOneR f t = do b <- get
+                  if b then
+                    return t
+                   else
+                    (lift (f t) <* put True) `mplus` return t
+
+unwrapOneR :: MonadPlus m => RewriteM (OneR m) f l -> RewriteM m f l
+unwrapOneR f t = do (t', b) <- runStateT (f t) False
+                    if b then
+                      return t'
+                     else
+                      mzero
+
+--------------------------------------------------------------------------------
+
+dynamicR :: (DynCase f l, MonadPlus m) => RewriteM m f l -> GRewriteM m f
+dynamicR f t = case dyncase t of
+                 Just p -> subst2 (sym p) $ f (subst p t)
+                 Nothing -> mzero
+
+tryR :: (Monad m) => RewriteM (MaybeT m) f l -> RewriteM m f l
+tryR f t = liftM (maybe t id) $ runMaybeT (f t)
+
+promoteR :: (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM m f
+promoteR = tryR . dynamicR
+
+promoteRF :: (DynCase f l, Monad m) => RewriteM (MaybeT m) f l -> GRewriteM (MaybeT m) f
+promoteRF = dynamicR
+
+-- | Applies a rewrite to all immediate subterms of the current term
+allR :: (Monad m, HTraversable f) => GRewriteM m (Term f) -> RewriteM m (Term f) l
+allR f t = liftM Term $ hmapM f $ unTerm t
+
+-- | Applies two rewrites in suceesion, succeeding if one or both succeed
+(>+>) :: (Applicative m, MonadPlus m) => GRewriteM m f -> GRewriteM m f -> GRewriteM m f
+f >+> g = unwrapAnyR (wrapAnyR f >=> wrapAnyR g)
+
+-- | Left-biased choice -- (f +> g) runs f, and, if it fails, then runs g
+(+>) :: (MonadPlus m) => RewriteM m f l -> RewriteM m f l -> RewriteM m f l
+(+>) f g x = f x `mplus` g x
+
+-- | Applies a rewrite to all immediate subterms of the current term, succeeding if any succeed
+anyR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> RewriteM m (Term f) l
+anyR f = unwrapAnyR $ allR $ wrapAnyR f -- not point-free because of type inference
+
+-- | Applies a rewrite to the first immediate subterm of the current term where it can succeed
+oneR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> RewriteM m (Term f) l
+oneR f = unwrapOneR $ allR $ wrapOneR f -- not point-free because of type inference
+
+-- | Runs a rewrite in a bottom-up traversal
+allbuR :: (Monad m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
+allbuR f = allR (allbuR f) >=> f
+
+-- | Runs a rewrite in a top-down traversal
+alltdR :: (Monad m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
+alltdR f = f >=> allR (alltdR f)
+
+-- | Runs a rewrite in a bottom-up traversal, succeeding if any succeed
+anybuR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
+anybuR f = anyR (anybuR f) >+> f
+
+-- | Runs a rewrite in a top-down traversal, succeeding if any succeed
+anytdR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
+anytdR f = f >+> anyR (anytdR f)
+
+-- | Runs a rewrite in a top-down traversal, succeeding if any succeed, and pruning below successes
+prunetdR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
+prunetdR f = f +> anyR (prunetdR f)
+
+-- | Applies a rewrite to the first node where it can succeed in a bottom-up traversal
+onebuR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
+onebuR f = oneR (onebuR f) +> f
+
+-- | Applies a rewrite to the first node where it can succeed in a top-down traversal
+onetdR :: (Applicative m, MonadPlus m, HTraversable f) => GRewriteM m (Term f) -> GRewriteM m (Term f)
+onetdR f = f +> oneR (onetdR f)
+
+--------------------------------------------------------------------------------
+-- Translations
+--------------------------------------------------------------------------------
+
+-- | A single-sorted translation in the Identity monad
+type Translate f l t = TranslateM Identity f l t
+
+-- | A monadic translation for a single sort
+type TranslateM m f l t = f l -> m t
+
+-- | A monadic translation for all sorts
+type GTranslateM m f t = forall l. TranslateM m f l t
+
+-- | Allows a one-sorted translation to be applied to any sort, failing at sorts
+--   different form the original
+promoteTF :: (DynCase f l, MonadPlus m) => TranslateM m f l t -> GTranslateM m f t
+promoteTF f t = case dyncase t of
+                  Just p -> f (subst p t)
+                  Nothing -> mzero
+
+-- | Lifts a translation into the Maybe monad, allowing it to fail
+addFail :: Monad m => TranslateM m f l t -> TranslateM (MaybeT m) f l t
+addFail = (lift . )
+
+-- | Runs a failable computation, replacing failure with mempty
+mtryM :: (Monad m, Monoid a) => MaybeT m a -> m a
+mtryM = liftM (maybe mempty id) . runMaybeT
+
+-- | Runs a translation in a top-down manner, combining its
+--   When run using MaybeT, returns its result for the last node where it succeded
+onetdT :: (MonadPlus m, HFoldable f) => GTranslateM m (Term f) t -> GTranslateM m (Term f) t
+onetdT t = query t mplus
+
+-- | Fold a tree in a top-down manner
+foldtdT :: (HFoldable f, Monoid t, Monad m) => GTranslateM m (Term f) t -> GTranslateM m (Term f) t
+foldtdT t = query t (liftM2 mappend)
+
+-- | An always successful top-down fold, replacing failures with mempty.
+crushtdT :: (HFoldable f, Monoid t, Monad m) => GTranslateM (MaybeT m) (Term f) t -> GTranslateM m (Term f) t
+crushtdT f = foldtdT $ mtryM . f
diff --git a/Data/Comp/Multi/Strategy/Classification.hs b/Data/Comp/Multi/Strategy/Classification.hs
new file mode 100644
--- /dev/null
+++ b/Data/Comp/Multi/Strategy/Classification.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverlappingInstances #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators #-}
+-- | 
+-- 
+-- This module contains typeclasses and operations allowing dynamic casing on sorts.
+
+module Data.Comp.Multi.Strategy.Classification
+  (
+    DynCase(..)
+  , KDynCase(..)
+  , dynProj
+  , caseE
+  ) where
+
+import Data.Comp.Multi ( (:+:), E, K, runE, caseH, (:&:), remA, Cxt(..) )
+import Data.Type.Equality ( (:~:)(..), gcastWith )
+
+--------------------------------------------------------------------------------
+
+
+-- |
+-- This operation allows you to rediscover the label giving
+-- the sort of a term by inspecting the term. It is mainly used
+-- through the 'caseE' and 'dynProj' operators
+class DynCase f a where
+  -- | Determine whether a node has sort @a@
+  dyncase :: f b -> Maybe (b :~: a)
+
+-- | An instance @KDynCase f a@ defines an instance @DynCase (Term f) a@
+class KDynCase f a where
+  kdyncase :: forall (e :: * -> *) b. DynCase e a => f e b -> Maybe (b :~: a)
+
+instance KDynCase f a where
+  kdyncase = const Nothing
+
+instance (KDynCase f l, KDynCase g l) => KDynCase (f :+: g) l where
+  kdyncase = caseH kdyncase kdyncase
+
+instance DynCase (K a) b where
+  dyncase _ = Nothing
+
+instance (KDynCase f l, DynCase a l) => DynCase (Cxt h f a) l where
+  dyncase (Term x) = kdyncase x
+  dyncase (Hole x) = dyncase x
+
+instance (KDynCase f l) => KDynCase (f :&: a) l where
+  kdyncase = kdyncase . remA
+
+--------------------------------------------------------------------------------
+
+dynProj :: forall f l l'. (DynCase f l) => f l' -> Maybe (f l)
+dynProj x = case (dyncase x :: Maybe (l' :~: l)) of
+              Just p -> Just (gcastWith p x)
+              Nothing -> Nothing
+
+-- | Inspect an existentially-quantified sort
+caseE :: (DynCase f a) => E f -> Maybe (f a)
+caseE = runE dynProj
diff --git a/Data/Comp/Multi/Strategy/Derive.hs b/Data/Comp/Multi/Strategy/Derive.hs
new file mode 100644
--- /dev/null
+++ b/Data/Comp/Multi/Strategy/Derive.hs
@@ -0,0 +1,101 @@
+{-# LANGUAGE TemplateHaskell #-}
+
+module Data.Comp.Multi.Strategy.Derive (
+    makeDynCase
+  ) where
+
+import Control.Arrow ( (&&&) )
+import Control.Monad
+
+import Data.Comp.Multi.Sum
+import Data.Comp.Multi.Term
+import Data.List ( nub )
+import Data.Maybe ( catMaybes )
+import Data.Type.Equality ( (:~:)(..) )
+
+import Language.Haskell.TH hiding ( Cxt )
+import Language.Haskell.TH.ExpandSyns
+import Language.Haskell.TH.Lib
+import Language.Haskell.TH.Syntax hiding ( Cxt )
+
+import Data.Comp.Multi.Strategy.Classification ( KDynCase, kdyncase )
+
+
+makeDynCase :: Name -> Q [Dec]
+makeDynCase fname = do
+          TyConI (DataD _cxt tname targs constrs _deriving) <- abstractNewtypeQ $ reify fname
+          let iVar = tyVarBndrName $ last targs
+          let labs = nub $ catMaybes $ map (iTp iVar) constrs
+          let cons = map (abstractConType &&& iTp iVar) constrs
+          mapM (genDyn tname cons) labs
+     where
+       iTp :: Name -> Con -> Maybe Type
+       iTp iVar (ForallC _ cxt _) =
+         -- Check if the GADT phantom type is constrained
+         case [y | EqualP x y <- cxt, x == VarT iVar] of
+           [] -> Nothing
+           tp:_ -> Just tp
+       iTp _ _ = Nothing
+  
+       genDyn :: Name -> [((Name, Int), Maybe Type)] -> Type -> Q Dec
+       genDyn tname cons tp = do
+           clauses <- liftM concat $ mapM (mkClause tp) cons
+           let body = [FunD 'kdyncase clauses]
+           instTp  <- forallT []
+                              (return [])
+                              (foldl appT (conT ''KDynCase) [conT tname, return tp])
+           return $ InstanceD [] instTp body
+  
+       mkClause :: Type -> ((Name, Int), Maybe Type) -> Q [Clause]
+       mkClause tp (con, Just tp')
+                   | tp == tp' = return [Clause [conPat con] 
+                                                (NormalB (AppE (ConE 'Just) (ConE 'Refl)))
+                                                []]
+       mkClause _ (con, _) = return [Clause [conPat con]
+                                            (NormalB (ConE 'Nothing))
+                                            []]
+  
+       conPat :: (Name, Int) -> Pat
+       conPat (con, n) = ConP con (replicate n WildP)
+
+
+{-|
+  This is the @Q@-lifted version of 'abstractNewtypeQ.
+-}
+abstractNewtypeQ :: Q Info -> Q Info
+abstractNewtypeQ = liftM abstractNewtype
+
+{-|
+  This function abstracts away @newtype@ declaration, it turns them into
+  @data@ declarations.
+-}
+abstractNewtype :: Info -> Info
+abstractNewtype (TyConI (NewtypeD cxt name args constr derive))
+    = TyConI (DataD cxt name args [constr] derive)
+abstractNewtype owise = owise
+
+
+{-|
+  This function provides the name and the arity of the given data constructor.
+-}
+abstractConType :: Con -> (Name,Int)
+abstractConType (NormalC constr args) = (constr, length args)
+abstractConType (RecC constr args) = (constr, length args)
+abstractConType (InfixC _ constr _) = (constr, 2)
+abstractConType (ForallC _ _ constr) = abstractConType constr
+
+{-|
+  This function returns the name of a bound type variable
+-}
+tyVarBndrName (PlainTV n) = n
+tyVarBndrName (KindedTV n _) = n
+
+
+
+{-|
+  This function provides a list (of the given length) of new names based
+  on the given string.
+-}
+newNames :: Int -> String -> Q [Name]
+newNames n name = replicateM n (newName name)
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2015, James Koppel
+
+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 James Koppel 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/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,2 @@
+# compstrat
+Strategy combinators for compositional data types
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/compstrat.cabal b/compstrat.cabal
new file mode 100644
--- /dev/null
+++ b/compstrat.cabal
@@ -0,0 +1,49 @@
+Name:                compstrat
+Version:             0.1.0.0
+Synopsis:            Strategy combinators for compositional data types
+Description:         
+
+    A library for strategic programming on compositional data types. See
+    /The Essence of Strategic Programming/, <http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.104.5296&rep=rep1&type=pdf>,
+    by Ralf Laemmel et al.
+    
+    Strategic programming is a way of allowing traversals to be written in a highly
+    generic and composable fashion.
+    
+    The names and general interface are modeled on the KURE library,
+    but this library tries to be as composable as the lens library.
+    
+    The type of a
+    strategy combinator is the same as the /Vertical/ type
+    that ekmett proposed and rejected as an extension to the current
+    lens library. A /Vertical/ is essentially a monadic traversal. This hence
+    could potentially be merged with the lens library.
+License:             BSD3
+License-File:        LICENSE
+Author:              James Koppel
+Maintainer:          jkoppel@mit.edu
+Category:            Language, Generics
+build-type:          Simple
+extra-source-files:  README.md
+Cabal-version:       >=1.9.2
+
+Source-Repository head
+  Type: git
+  Location: https://github.com/jkoppel/compstrat
+
+Library
+
+  Exposed-Modules:     
+                     Data.Comp.Multi.Strategic
+                     Data.Comp.Multi.Strategy.Classification
+                     Data.Comp.Multi.Strategy.Derive
+
+  Build-Depends:
+
+                     base >=4.7 && <4.8
+                   , compdata < 1
+                   , mtl < 2.3
+                   , template-haskell
+                   , th-expand-syns <= 0.4
+                   , transformers < 0.5
+