diff --git a/DDC/Core/Transform/ANormal.hs b/DDC/Core/Transform/ANormal.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/ANormal.hs
@@ -0,0 +1,196 @@
+
+module DDC.Core.Transform.ANormal
+    (anormalise)
+where
+import DDC.Core.Exp
+import qualified DDC.Type.Exp as T
+import qualified DDC.Type.Compounds as T
+import qualified DDC.Type.Universe as U
+import qualified DDC.Core.Transform.LiftX as L
+
+import qualified Data.Map as Map
+
+-- **** Recording arities of known values
+-- So we can try to create apps to fully apply 
+
+-- I did have these as Maybe Int, but I think for our purposes 0==Nothing is fine
+type Arities n = (Map.Map n Int, [Int])
+
+arEmpty :: Ord n => Arities n
+arEmpty = (Map.empty, [])
+
+arExtends :: Ord n => Arities n -> [(Bind n, Int)] -> Arities n
+arExtends arity exts = foldl go arity exts
+ where	go (named,anon) (BNone _t,   _)    = (named,anon)
+	go (named,anon) (BAnon _t,   a)    = (named, a:anon)
+	go (named,anon) (BName n _t, a) = (Map.insert n a named, anon)
+
+arGet :: Ord n => Arities n -> Bound n -> Int
+-- TODO unsafe ix
+arGet (_named, anon) (UIx ix _)	  = anon !! ix
+arGet (named, _anon) (UName n _)  = named Map.! n
+-- Get a primitive's arity from its type.
+-- Assuming all the primitives defer effects until fully applied.
+arGet (_named,_anon) (UPrim _ t)  = arityOfType t
+
+-- **** Finding arities of expressions etc
+
+-- Count all the arrows, ignoring any effects
+arityOfType :: Ord n => Type n -> Int
+arityOfType (T.TForall _ t)
+ =  1 + arityOfType t
+arityOfType t
+ =  let (args, _) = T.takeTFunArgResult t in
+    length args
+
+arityOfExp :: Ord n => Exp a n -> Int
+arityOfExp (XLam _ b e)
+    -- only count data binders
+    | isBinderData b
+    = 1 + arityOfExp e
+arityOfExp (XLam _ _ e)
+    = 1 + arityOfExp e
+arityOfExp (XLAM _ _ e)
+    = 1 + arityOfExp e
+arityOfExp (XCon _ (UPrim _ t))
+    = arityOfType t
+arityOfExp _
+    = 0
+
+isBinderData :: Ord n => Bind n -> Bool
+isBinderData b | Just U.UniverseData <- U.universeFromType1 (T.typeOfBind b)
+ =  True
+isBinderData _ = False
+
+-- We don't know anything about their values,
+-- but we need to record them as 0 anyway (shadowing, de bruijn)
+aritiesOfPat :: Ord n => Pat n -> [(Bind n, Int)]
+aritiesOfPat PDefault = []
+aritiesOfPat (PData _b bs) = zip bs (repeat 0)
+
+
+-- **** Actually converting to a-normal form
+anormal :: Ord n => Arities n -> Exp a n -> [Exp a n] -> Exp a n
+anormal ar (XApp _ lhs rhs) args
+ =  -- normalise applicand and record arguments
+    let args' = anormal ar rhs [] : args in
+    -- descend into lhs, remembering all args
+    anormal ar lhs args'
+
+anormal ar x args
+ =  let x' = go x in
+    -- if there are no args, we're done
+    case args of
+	[] -> x'
+	_  -> -- there are arguments. we must apply them.
+	    makeLets ar x' args
+ where
+    -- helper for descent
+    down ars e = anormal (arExtends ar ars) e []
+
+    -- we know x isn't an app.
+    go (XApp{}) = error "ANormal.anormal: impossible XApp!"
+
+    -- leafy ones
+    go (XVar{}) = x
+    go (XCon{}) = x
+    go (XType{}) = x
+    go (XWitness{}) = x
+
+    go (XLAM a b e) =
+	XLAM a b (down [(b,0)] e)
+    go (XLam a b e) =
+	XLam a b (down [(b,0)] e)
+
+    -- non-recursive let
+    go (XLet a (LLet m b le) re) =
+	let le' = down [] le in
+	let re' = down [(b, arityOfExp le')] re in
+	XLet a (LLet m b le') re'
+
+    -- recursive let
+    go (XLet a (LRec lets) re) =
+	let bs = map fst lets in
+	let es = map snd lets in
+	let ars= zip bs (map arityOfExp es) in
+	let es'= map (down ars) es in
+	let re'= down ars re in
+	XLet a (LRec $ zip bs es') re' 
+
+    -- letregion, just make sure we record bindings with dummy val
+    go (XLet a (LLetRegion b bs) re) =
+	let ars = zip bs (repeat 0) in
+	XLet a (LLetRegion b bs) (down ars re)
+
+    -- I don't think a withregion should ever show up...
+    go (XLet a (LWithRegion b) re) =
+	XLet a (LWithRegion b) (down [] re)
+
+    go (XCase a e alts) =
+	let e' = down [] e in
+	let alts' = map (\(AAlt pat ae) -> AAlt pat (down (aritiesOfPat pat) ae)) alts in
+	XCase a e' alts'
+
+    go (XCast a c e) =
+	XCast a c (down [] e)
+
+
+-- | (under development)
+anormalise :: Ord n => Exp a n -> Exp a n
+anormalise x = anormal arEmpty x []
+
+-- | Check if an expression needs a binding, or if it's simple enough to just be applied
+isNormal :: Ord n => Exp a n -> Bool
+isNormal (XVar{}) = True
+isNormal (XCon{}) = True
+isNormal (XType{}) = True
+isNormal (XWitness{}) = True
+isNormal (XCast _ _ x) = isNormal x
+isNormal _ = False
+	
+makeLets ar f0 args = go 0 (findArity f0) (f0:args) []
+ where
+    tBot = T.tBot T.kData
+
+    -- sending arity of f to this is a hack because we should really be building up ar ctx?
+    go i _arf []  acc = mkApps i 0 acc
+    -- f is fully applied, and we *do* have arguments left to add
+    go i arf (x:xs) acc | length acc > arf
+     =  XLet (annotOf x) (LLet LetStrict (BAnon tBot) (mkApps i 0 acc))
+            (go i 1 (x:xs) [XVar (annotOf x) $ UIx 0 tBot])
+    -- application to variable, don't bother binding
+    go i arf (x:xs) acc | isNormal x
+     =  go i arf xs (x:acc)
+    -- create binding
+    go i arf (x:xs) acc
+     =  XLet (annotOf x) (LLet LetStrict (BAnon tBot) (L.liftX i x))
+	    (go (i+1) arf xs (x:acc))
+    
+    mkApps _ _ []
+     = error "ANormal.makeLets.mkApps: impossible empty list"
+    mkApps l _ [x] | isNormal x
+     = L.liftX l x
+    mkApps _ i [x]
+     = XVar (annotOf x) $ UIx i tBot
+
+    mkApps l i (x:xs) | isNormal x
+     = XApp (annotOf x) (mkApps l i xs) (L.liftX l x)
+    mkApps l i (x:xs)
+     = XApp (annotOf x) (mkApps l (i+1) xs) (XVar (annotOf x) $ UIx i tBot)
+
+    findArity (XVar _ b) = max (arGet ar b) 1
+    findArity x          = max (arityOfExp x) 1
+
+-- does this exist elsewhere? ought it?
+annotOf :: Exp a n -> a
+annotOf (XVar a _) = a
+annotOf (XCon a _) = a
+annotOf (XApp a _ _) = a
+annotOf (XLAM a _ _) = a
+annotOf (XLam a _ _) = a
+annotOf (XLet a _ _) = a
+annotOf (XCase a _ _) = a
+annotOf (XCast a _ _) = a
+annotOf (XType{}) = error "DDC.Core.Transform.ANormal.annotOf: XType"
+annotOf (XWitness{}) = error "DDC.Core.Transform.ANormal.annotOf: XWitness"
+
diff --git a/DDC/Core/Transform/AnonymizeX.hs b/DDC/Core/Transform/AnonymizeX.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/AnonymizeX.hs
@@ -0,0 +1,178 @@
+
+module DDC.Core.Transform.AnonymizeX
+        ( anonymizeX
+        , AnonymizeX(..))
+where
+import DDC.Core.Exp
+import DDC.Type.Transform.AnonymizeT
+import DDC.Type.Compounds
+import Control.Monad
+import Data.List
+
+
+-- | Rewrite all binders in a thing to be of anonymous form.
+anonymizeX :: (Ord n, AnonymizeX c) => c n -> c n
+anonymizeX xx
+        = anonymizeWithX [] [] xx
+
+
+-------------------------------------------------------------------------------
+class AnonymizeX (c :: * -> *) where
+
+ -- | Rewrite all binders in a thing to be anonymous.
+ --   The stacks contains existing anonymous binders that we have entered into,
+ --   and named binders that we have rewritten. All bound occurrences of variables
+ --   will be replaced by references into these stacks.
+ anonymizeWithX 
+        :: forall n. Ord n 
+        => [Bind n]     -- ^ Stack for Spec binders (level-1).
+        -> [Bind n]     -- ^ Stack for Data and Witness binders (level-0).
+        -> c n -> c n
+
+
+instance AnonymizeX (Exp a) where
+ anonymizeWithX kstack tstack xx
+  = let down = anonymizeWithX kstack tstack
+    in case xx of
+        XVar a u        -> XVar a (down u)
+        XCon a u        -> XCon a (down u)
+        XApp a x1 x2    -> XApp a (down x1) (down x2)
+
+        XLAM a b x
+         -> let (kstack', b')   = pushAnonymizeBindT kstack b
+            in  XLAM a b'   (anonymizeWithX kstack' tstack x)
+
+        XLam a b x
+         -> let (tstack', b')   = pushAnonymizeBindX kstack tstack b
+            in  XLam a b'   (anonymizeWithX kstack tstack' x)
+
+        XLet a lts x
+         -> let (kstack', tstack', lts')  
+                 = pushAnonymizeLets kstack tstack lts
+            in  XLet a lts' (anonymizeWithX kstack' tstack' x)
+
+        XCase a x alts  -> XCase a  (down x) (map down alts)
+        XCast a c x     -> XCast a  (down c) (down x)
+        XType t         -> XType    (anonymizeWithT kstack t)
+        XWitness w      -> XWitness (down w)
+
+
+instance AnonymizeX Cast where
+ anonymizeWithX kstack tstack cc
+  = case cc of
+        CastWeakenEffect eff    -> CastWeakenEffect  (anonymizeWithT kstack eff)
+        CastWeakenClosure clo   -> CastWeakenClosure (anonymizeWithT kstack clo)
+        CastPurify w            -> CastPurify   (anonymizeWithX kstack tstack w)
+        CastForget w            -> CastForget   (anonymizeWithX kstack tstack w)
+
+
+instance AnonymizeX LetMode where
+ anonymizeWithX kstack tstack lm
+  = case lm of
+        LetStrict       -> lm
+        LetLazy mw      -> LetLazy $ liftM (anonymizeWithX kstack tstack) mw
+
+
+instance AnonymizeX (Alt a) where
+ anonymizeWithX kstack tstack alt
+  = case alt of
+        AAlt PDefault x
+         -> AAlt PDefault (anonymizeWithX kstack tstack x)
+
+        AAlt (PData uCon bs) x
+         -> let (tstack', bs')  = pushAnonymizeBindXs kstack tstack bs
+                x'              = anonymizeWithX kstack tstack' x
+            in  AAlt (PData uCon bs') x'
+
+
+instance AnonymizeX Witness where
+ anonymizeWithX kstack tstack ww
+  = let down = anonymizeWithX kstack tstack 
+    in case ww of
+        WVar  u         -> WVar  (down u)
+        WCon  c         -> WCon  c
+        WApp  w1 w2     -> WApp  (down w1) (down w2)
+        WJoin w1 w2     -> WJoin (down w1) (down w2)
+        WType t         -> WType (anonymizeWithT kstack t)
+
+
+instance AnonymizeX Bind where
+ anonymizeWithX kstack _tstack bb
+  = let t'      = anonymizeWithT kstack $ typeOfBind bb
+    in  replaceTypeOfBind t' bb 
+
+
+instance AnonymizeX Bound where 
+ anonymizeWithX kstack tstack bb
+  = case bb of
+        UName _ t
+         | Just ix      <- findIndex (boundMatchesBind bb) tstack
+         -> UIx ix (anonymizeWithT kstack t)
+         
+        _ -> bb
+
+
+-- Push ----------------------------------------------------------------------
+-- Push a binding occurrence of a type variable on the stack, 
+--  returning the anonyized binding occurrence and the new stack.
+pushAnonymizeBindX 
+        :: Ord n 
+        => [Bind n]     -- ^ Stack for Spec binders (kind environment)
+        -> [Bind n]     -- ^ Stack for Value and Witness binders (type environment)
+        -> Bind n 
+        -> ([Bind n], Bind n)
+
+pushAnonymizeBindX kstack tstack b
+ = let  b'      = anonymizeWithX kstack tstack b
+        t'      = typeOfBind b'
+        tstack' = case b' of
+                        BName{} -> b' : tstack
+                        BAnon{} -> b' : tstack
+                        _       -> tstack
+   in   (tstack', BAnon t')
+
+
+-- Push a binding occurrence on the stack, 
+--  returning the anonyized binding occurrence and the new stack.
+-- Used in the definition of `anonymize`.
+pushAnonymizeBindXs 
+        :: Ord n 
+        => [Bind n]     -- ^ Stack for Spec binders (kind environment)
+        -> [Bind n]     -- ^ Stack for Value and Witness binders (type environment)
+        -> [Bind n] 
+        -> ([Bind n], [Bind n])
+
+pushAnonymizeBindXs kstack tstack bs
+  = mapAccumL   (\tstack' b -> pushAnonymizeBindX kstack tstack' b)
+                tstack bs
+
+
+pushAnonymizeLets 
+        :: Ord n 
+        => [Bind n] -> [Bind n] 
+        -> Lets a n 
+        -> ([Bind n], [Bind n], Lets a n)
+
+pushAnonymizeLets kstack tstack lts
+ = case lts of
+        LLet mode b x
+         -> let mode'           = anonymizeWithX     kstack tstack mode
+                (tstack', b')   = pushAnonymizeBindX kstack tstack b
+                x'              = anonymizeWithX     kstack tstack' x
+            in  (kstack, tstack', LLet mode' b' x')
+
+        LRec bxs 
+         -> let (bs, xs)        = unzip bxs
+                (tstack', bs')  = pushAnonymizeBindXs kstack tstack   bs
+                xs'             = map (anonymizeWithX kstack tstack') xs
+                bxs'            = zip bs' xs'
+            in  (kstack, tstack', LRec bxs')
+
+        LLetRegion b bs
+         -> let (kstack', b')   = pushAnonymizeBindT  kstack b
+                (tstack', bs')  = pushAnonymizeBindXs kstack' tstack bs
+            in  (kstack', tstack', LLetRegion b' bs')
+
+        LWithRegion{}
+         -> (kstack, tstack, lts)
+
diff --git a/DDC/Core/Transform/Beta.hs b/DDC/Core/Transform/Beta.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/Beta.hs
@@ -0,0 +1,61 @@
+
+module DDC.Core.Transform.Beta
+        (betaReduce)
+where
+import DDC.Core.Exp
+import DDC.Core.Transform.TransformX
+import DDC.Core.Transform.SubstituteTX
+import DDC.Core.Transform.SubstituteWX
+import DDC.Core.Transform.SubstituteXX
+import DDC.Type.Env             (Env)
+import qualified DDC.Type.Env   as Env
+
+
+-- | Beta-reduce applications of a explicit lambda abstractions 
+--   to variables and values.
+betaReduce  :: Ord n => Exp a n -> Exp a n
+betaReduce 
+        = transformUpX betaReduce1 Env.empty Env.empty
+
+
+betaReduce1 :: Ord n => Env n -> Env n -> Exp a n -> Exp a n
+betaReduce1 _ _ xx
+ = case xx of
+        XApp _ (XLAM _ b11 x12) (XType t2)
+         -> substituteTX b11 t2 x12
+
+        XApp _ (XLam _ b11 x12) (XWitness w2)
+         -> substituteWX b11 w2 x12
+
+        XApp _ (XLam _ b11 x12) x2
+         |  canBetaSubstX x2     
+         -> substituteXX b11 x2 x12
+
+         | otherwise
+         -> xx
+
+        _ -> xx
+
+
+-- | Check whether we can safely substitute this expression during beta
+--   evaluation. 
+-- 
+--   We allow variables, abstractions, type and witness applications.
+--   Duplicating these expressions is guaranteed not to duplicate work
+--   at runtime,
+canBetaSubstX :: Exp a n -> Bool
+canBetaSubstX xx
+ = case xx of
+        XVar{}  -> True
+        XCon{}  -> True
+        XLam{}  -> True
+        XLAM{}  -> True
+
+        XApp _ x1 (XType _)
+         -> canBetaSubstX x1
+
+        XApp _ x1 (XWitness _)
+         -> canBetaSubstX x1 
+
+        _       -> False
+
diff --git a/DDC/Core/Transform/TransformX.hs b/DDC/Core/Transform/TransformX.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Core/Transform/TransformX.hs
@@ -0,0 +1,112 @@
+
+-- | General purpose tree walking boilerplate.
+module DDC.Core.Transform.TransformX
+        ( TransformUpMX(..)
+        , transformUpX)
+where
+import DDC.Core.Exp
+import DDC.Core.Compounds
+import DDC.Type.Env             (Env)
+import Data.Functor.Identity
+import Control.Monad
+import qualified DDC.Type.Env   as Env
+
+
+-- | Bottom up rewrite of all core expressions in a thing.
+transformUpX
+        :: forall (c :: * -> * -> *) a n
+        .  (Ord n, TransformUpMX Identity c)
+        => (Env n -> Env n -> Exp a n -> Exp a n)       
+                        -- ^ The worker function is given the current kind and type environments.
+        -> Env n        -- ^ Initial kind environment.
+        -> Env n        -- ^ Initial type environment.
+        -> c a n        -- ^ Transform this thing.
+        -> c a n
+
+transformUpX f kenv tenv xx
+        = runIdentity 
+        $ transformUpMX 
+                (\kenv' tenv' x -> return (f kenv' tenv' x)) 
+                kenv tenv xx
+
+
+class TransformUpMX m (c :: * -> * -> *) where
+ -- | Bottom-up monadic rewrite of all core expressions in a thing.
+ transformUpMX
+        :: Ord n
+        => (Env n -> Env n -> Exp a n -> m (Exp a n))
+                        -- ^ The worker function is given the current kind and type environments.
+        -> Env n        -- ^ Initial kind environment.
+        -> Env n        -- ^ Initial type environment.
+        -> c a n        -- ^ Transform this thing.
+        -> m (c a n)
+
+instance Monad m => TransformUpMX m Exp where
+ transformUpMX f kenv tenv xx
+  = (f kenv tenv =<<)
+  $ case xx of
+        XVar{}          -> return xx
+        XCon{}          -> return xx
+
+        XLAM a b x1
+         -> liftM3 XLAM (return a) (return b)
+                        (transformUpMX f (Env.extend b kenv) tenv x1)
+
+        XLam a b  x1    
+         -> liftM3 XLam (return a) (return b) 
+                        (transformUpMX f kenv (Env.extend b tenv) x1)
+
+        XApp a x1 x2    
+         -> liftM3 XApp (return a) 
+                        (transformUpMX f kenv tenv x1) 
+                        (transformUpMX f kenv tenv x2)
+
+        XLet a lts x
+         -> do  lts'      <- transformUpMX f kenv tenv lts
+                let kenv' = Env.extends (specBindsOfLets lts')   kenv
+                let tenv' = Env.extends (valwitBindsOfLets lts') tenv
+                x'        <- transformUpMX f kenv' tenv' x
+                return  $ XLet a lts' x'
+                
+        XCase a x alts
+         -> liftM3 XCase (return a)
+                         (transformUpMX f kenv tenv x)
+                         (mapM (transformUpMX f kenv tenv) alts)
+
+        XCast a c x       
+         -> liftM3 XCast
+                        (return a) (return c)
+                        (transformUpMX f kenv tenv x)
+
+        XType _         -> return xx
+        XWitness _      -> return xx
+
+
+instance Monad m => TransformUpMX m Lets where
+ transformUpMX f kenv tenv xx
+  = case xx of
+        LLet m b x
+         -> liftM3 LLet (return m) (return b)
+                        (transformUpMX f kenv tenv x)
+        
+        LRec bxs
+         -> do  let (bs, xs) = unzip bxs
+                let tenv'    = Env.extends bs tenv
+                xs'          <- mapM (transformUpMX f kenv tenv') xs
+                return       $ LRec $ zip bs xs'
+
+        LLetRegion{}    -> return xx
+        LWithRegion{}    -> return xx
+
+
+instance Monad m => TransformUpMX m Alt where
+ transformUpMX f kenv tenv alt
+  = case alt of
+        AAlt p@(PData _ bsArg) x
+         -> let tenv'   = Env.extends bsArg tenv
+            in  liftM2  AAlt (return p) 
+                        (transformUpMX f kenv tenv' x)
+
+        AAlt PDefault x
+         ->     liftM2  AAlt (return PDefault)
+                        (transformUpMX f kenv tenv x) 
diff --git a/DDC/Type/Transform/AnonymizeT.hs b/DDC/Type/Transform/AnonymizeT.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Type/Transform/AnonymizeT.hs
@@ -0,0 +1,78 @@
+
+module DDC.Type.Transform.AnonymizeT
+        ( anonymizeT
+        , AnonymizeT(..)
+        , pushAnonymizeBindT)
+where
+import DDC.Type.Exp
+import DDC.Type.Compounds
+import Data.List
+import qualified DDC.Type.Sum           as T
+
+
+-- | Rewrite all binders in a thing to be of anonymous form.
+anonymizeT :: (Ord n, AnonymizeT c) => c n -> c n
+anonymizeT xx
+        = anonymizeWithT [] xx
+
+
+-------------------------------------------------------------------------------
+class AnonymizeT (c :: * -> *) where
+
+ -- | Rewrite all binders in a thing to be of anonymous form.
+ --   
+ --   The stack contains existing anonymous binders that we have entered into,
+ --   and named binders that we have rewritten. All bound occurrences of variables
+ --   will be replaced by references into this stack.
+ anonymizeWithT :: forall n. Ord n => [Bind n] -> c n -> c n
+
+
+instance AnonymizeT Type where
+ anonymizeWithT kstack tt
+  = case tt of
+        TVar u
+         -> TVar $ anonymizeWithT kstack u
+
+        TCon{}          
+         -> tt
+
+        TForall b t     
+         -> let (kstack', b') = pushAnonymizeBindT kstack b
+            in  TForall b' (anonymizeWithT kstack' t)
+
+        TApp t1 t2      
+         -> TApp (anonymizeWithT kstack t1) (anonymizeWithT kstack t2)
+
+        TSum ss 
+         -> TSum (anonymizeWithT kstack ss)
+
+
+instance AnonymizeT TypeSum where
+ anonymizeWithT kstack ss
+        = T.fromList (anonymizeWithT kstack $ T.kindOfSum ss)
+        $ map (anonymizeWithT kstack)
+        $ T.toList ss
+
+
+instance AnonymizeT Bound where 
+ anonymizeWithT kstack bb
+  = case bb of
+        UName _ t
+         | Just ix      <- findIndex (boundMatchesBind bb) kstack
+         -> UIx ix (anonymizeWithT kstack t)
+         
+        _ -> bb
+
+
+-- Push ----------------------------------------------------------------------
+-- Push a binding occurrence of a type variable on the stack, 
+--  returning the anonyized binding occurrence and the new stack.
+pushAnonymizeBindT :: Ord n => [Bind n] -> Bind n -> ([Bind n], Bind n)
+pushAnonymizeBindT kstack b
+ = let  t'      = typeOfBind b
+        kstack' = case b of
+                        BName{} -> b : kstack
+                        BAnon{} -> b : kstack
+                        _       -> kstack
+   in   (kstack', BAnon t')
+
diff --git a/DDC/Type/Transform/Rename.hs b/DDC/Type/Transform/Rename.hs
new file mode 100644
--- /dev/null
+++ b/DDC/Type/Transform/Rename.hs
@@ -0,0 +1,53 @@
+
+module DDC.Type.Transform.Rename
+        (Rename(..))
+where
+import DDC.Type.Exp
+import DDC.Type.Sum
+
+
+class Rename (c :: * -> *) where
+ -- | Apply a function to all the names in a thing.
+ rename :: forall n1 n2. Ord n2 => (n1 -> n2) -> c n1 -> c n2
+ 
+
+instance Rename Type where
+ rename f tt
+  = case tt of
+        TVar    u       -> TVar    (rename f u)
+        TCon    c       -> TCon    (rename f c)
+        TForall b t     -> TForall (rename f b)  (rename f t)
+        TApp    t1 t2   -> TApp    (rename f t1) (rename f t2)
+        TSum    ts      -> TSum    (rename f ts)
+
+
+instance Rename TypeSum where
+ rename f ts
+  = fromList (rename f $ kindOfSum ts) $ map (rename f) $ toList ts
+
+
+instance Rename Bind where
+ rename f bb
+  = case bb of
+        BName n t       -> BName (f n) (rename f t)
+        BAnon   t       -> BAnon (rename f t)
+        BNone   t       -> BNone (rename f t)
+        
+
+instance Rename Bound where
+ rename f uu
+  = case uu of
+        UIx   i k       -> UIx   i     (rename f k)
+        UName n k       -> UName (f n) (rename f k)
+        UPrim n k       -> UName (f n) (rename f k)
+
+
+instance Rename TyCon where
+ rename f cc
+  = case cc of
+        TyConSort sc    -> TyConSort    sc
+        TyConKind kc    -> TyConKind    kc
+        TyConWitness tc -> TyConWitness tc
+        TyConSpec tc    -> TyConSpec    tc
+        TyConBound u    -> TyConBound $ rename f u
+
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,20 @@
+--------------------------------------------------------------------------------
+The Disciplined Disciple Compiler License (MIT style)
+
+Copyright (c) 2008-2011 Benjamin Lippmeier
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+--------------------------------------------------------------------------------
+Redistributions of libraries in ./external are governed by their own licenses:
+
+  - TinyPTC   GNU Lesser General Public License
+  
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/ddc-core-simpl.cabal b/ddc-core-simpl.cabal
new file mode 100644
--- /dev/null
+++ b/ddc-core-simpl.cabal
@@ -0,0 +1,47 @@
+Name:           ddc-core-simpl
+Version:        0.2.0.1
+License:        MIT
+License-file:   LICENSE
+Author:         Ben Lippmeier
+Maintainer:     benl@ouroborus.net
+Build-Type:     Simple
+Cabal-Version:  >=1.6
+Stability:      experimental
+Category:       Compilers/Interpreters
+Homepage:       http://disciple.ouroborus.net
+Bug-reports:    disciple@ouroborus.net
+Synopsis:       Disciple Core language simplifying code transformations.
+Description:    Disciple Core language simplifying code transformations.
+
+Library
+  Build-Depends: 
+        base            == 4.5.*,
+        containers      == 0.4.*,
+        array           >= 0.3   && < 0.5,
+        transformers    == 0.2.*,
+        mtl             == 2.0.*,
+        ddc-base        == 0.2.0.*,
+        ddc-core        == 0.2.0.*
+
+  Exposed-modules:
+        DDC.Core.Transform.AnonymizeX
+        DDC.Core.Transform.ANormal
+        DDC.Core.Transform.Beta
+        DDC.Core.Transform.TransformX
+        DDC.Type.Transform.AnonymizeT
+        DDC.Type.Transform.Rename
+        
+  GHC-options:
+        -Wall
+        -fno-warn-orphans
+        -fno-warn-missing-signatures
+        -fno-warn-unused-do-bind
+
+  Extensions:
+        NoMonomorphismRestriction
+        ExplicitForAll
+        KindSignatures
+        PatternGuards
+        MultiParamTypeClasses
+        FlexibleContexts
+        FlexibleInstances