diff --git a/CHANGES b/CHANGES
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,11 @@
+0.2 -> 0.4
+===============
+
+* drastic simplifications when writing the ICFP submission
+
+* I'll eventually work those older features back in --- Though it is
+  *extremely* unlikely, I apologize if you were using them.
+
 0.1 -> 0.2
 ===============
 
diff --git a/Data/Yoko.hs b/Data/Yoko.hs
--- a/Data/Yoko.hs
+++ b/Data/Yoko.hs
@@ -1,19 +1,93 @@
-{- |
+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,
+  MultiParamTypeClasses, FlexibleInstances, ConstraintKinds,
+  ScopedTypeVariables, UndecidableInstances #-}
 
-Module      :  Data.Yoko
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
+module Data.Yoko
+  (derive, Equal, module Data.Yoko.Representation,
+   module Data.Yoko.TypeSums, module Data.Yoko, encode) where
 
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
+import Data.Yoko.TypeBasics
+import Data.Yoko.Representation
+import Data.Yoko.TypeSums (Embed, Partition, (:-:))
+import qualified Data.Yoko.TypeSums as TypeSums
+import Data.Yoko.Each
 
--}
-module Data.Yoko
-  (module Type.Yoko, module Data.Yoko.Generic, module Data.Yoko.Reflect, module Data.Yoko.InDT
-  ) where
+import Control.Arrow (right, (+++))
 
-import Type.Yoko
-import Data.Yoko.Generic
-import Data.Yoko.Reflect
-import Data.Yoko.InDT
+
+
+
+one :: (dc -> a) -> DCsOf (Range dc) (N dc) -> a
+one = (. unDCsOf) . foldN
+
+infixl 9 .|.   ;   f .|. g = one f ||| one g
+infixr 8 .||   ;   f .|| g = one f ||| g
+infixl 8 ||.   ;   f ||. g = f ||| one g
+
+
+
+type family Tag dc
+
+type family Range dc
+class (Generic dc, DT (Range dc)) => DC dc where rejoin :: dc -> Range dc
+
+type family DCs t
+type Disbanded t = DCsOf t (DCs t)
+class Each IsDCOf (DCs t) => DT t where disband :: t -> Disbanded t
+
+class (Partition (DCs (Range dc)) (N dc) (DCs (Range dc) :-: N dc),
+       Embed (N dc) (DCs (Range dc))) => IsDCOf dc
+instance (Partition (DCs (Range dc)) (N dc) (DCs (Range dc) :-: N dc),
+          Embed (N dc) (DCs (Range dc))) => IsDCOf dc
+
+
+
+disbanded :: Embed (N dc) (DCs (Range dc)) => dc -> Disbanded (Range dc)
+disbanded = DCsOf . TypeSums.inject
+
+band :: forall t. Each (ConDCOf t) (DCs t) => Disbanded t -> t
+band = each (Proxy :: Proxy (ConDCOf t)) rejoin
+
+class (Range dc ~ t, DC dc) => ConDCOf t dc
+instance (Range dc ~ t, DC dc) => ConDCOf t dc
+
+
+
+inject :: Embed (N dc) sum => dc -> sum
+inject = TypeSums.inject
+
+partition :: Partition sum sub (sum :-: sub) =>
+             DCsOf t sum -> Either (DCsOf t sub) (DCsOf t (sum :-: sub))
+partition = (DCsOf +++ DCsOf) . TypeSums.partition . unDCsOf
+
+project :: Partition sum (N dc) (sum :-: N dc) =>
+           DCsOf (Range dc) sum -> Either dc (DCsOf (Range dc) (sum :-: N dc))
+project = right DCsOf . TypeSums.project . unDCsOf
+
+
+
+-- TODO need a MapSum just like MapRs, use a RPV for rep
+reps :: EachGeneric sum => DCsOf t sum -> EachRep sum
+reps = repEach . unDCsOf
+
+type family EachRep sum
+type instance EachRep (N a) = Rep a
+type instance EachRep (a :+: b) = EachRep a :+: EachRep b
+class EachGeneric sum where
+  repEach :: sum -> EachRep sum   ;   objEach :: EachRep sum -> sum
+instance Generic a => EachGeneric (N a) where
+  repEach (N x) = rep x   ;   objEach = N . obj
+instance (EachGeneric a, EachGeneric b) => EachGeneric (a :+: b) where
+  repEach = mapPlus repEach repEach
+  objEach = mapPlus objEach objEach
+
+
+
+
+
+exact_case :: (DT t, Partition (DCs t) dcs (DCs t :-: dcs)) =>
+  (DCsOf t (DCs t :-: dcs) -> a) -> t -> (DCsOf t dcs -> a) -> a
+exact_case g x f =
+  either f g $ partition $ disband x
+
+ig_from x = reps $ disband x
diff --git a/Data/Yoko/Cata.hs b/Data/Yoko/Cata.hs
deleted file mode 100644
--- a/Data/Yoko/Cata.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE QuasiQuotes, TypeOperators, TypeFamilies, GADTs #-}
-{-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
-  UndecidableInstances #-}
-
-{- |
-
-Module      :  Data.Yoko.Algebra
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Catamorphism for mutually-recursive datatypes.
-
--}
-module Data.Yoko.Cata
-  (Algebras, SiblingAlgs, algebras, CataU(..), catas, cata,
-  module Data.Yoko.Reduce) where
-    
-import Type.Yoko
-
-import Data.Yoko.Generic
-import Data.Yoko.Reflect
-import Data.Yoko.Reduce
-
-
-
-
-
-type Algebras ts m = Each ts (Algebra m)
-type SiblingAlgs t m = Algebras (Siblings t) m
-
--- | Builds an 'Each' of algebras via 'AlgebraDT'.
-algebras :: forall ts m. (ts ::: All (AlgebraU m)) => [qP|m|] -> Algebras ts m
-algebras _ = each [qP|AlgebraU m :: *->*|] $ \AlgebraU -> algebraDT
-
-
-
-
--- | @t@ inhabits @CataU ts m@ if
---
---   1. @t@ is an instance of 'DT' and @ts ~ Siblings t@
---
---   2. the recursive reduction can be mapped as a 'FromAt' function via
---   'RMMap' across all constructors of @t@ and
---
---   3. all of @t@'s siblings also inhabit the same universe.
-data CataU ts m t where
-  CataU :: (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),
-            DCs t ::: All
-              (YieldsArrowTSSU
-               (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
-            ts ::: All (CataU ts m)
-           ) => CataU ts m t
-instance (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),
-          DCs t ::: All
-            (YieldsArrowTSSU
-             (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
-          ts ::: All (CataU ts m)
-         ) => t ::: CataU ts m where inhabits = CataU
-
-catas :: forall m ts. (ts ::: All (CataU ts m)) =>
-         Algebras ts m -> Each ts (FromAt m IdM)
-catas fs = each [qP|CataU ts m :: *->*|] $ \d@CataU -> cataD d fs
-
-cataD :: forall m t. CataU (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t
-cataD CataU fs =
-  appNT fs (inhabits :: Uni (Siblings t) t) .
-  appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $
-             RMMap $ catas fs) . disband
-
--- | Uses the @m@-mediated algebras for @t@'s siblings to reduce a @t@ to @Med
--- m t@.
-cata :: (t ::: CataU (Siblings t) m) => SiblingAlgs t m -> t -> Med m t
-cata = cataD inhabits
diff --git a/Data/Yoko/Core.hs b/Data/Yoko/Core.hs
deleted file mode 100644
--- a/Data/Yoko/Core.hs
+++ /dev/null
@@ -1,83 +0,0 @@
-{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, EmptyDataDecls #-}
-
-{-# LANGUAGE TemplateHaskell #-}
-
-{- |
-
-Module      :  Data.Yoko.Core
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-The core structural types; \"sum of products\" and such.
-
--}
-
-module Data.Yoko.Core where
-
-import Type.Yoko.Type (derive)
-
---import Polarity
-
-
-
--- | Structural representations (e.g. "Data.Yoko.Generic"'s 'RM') of a @*@ type
--- can be derived as a data family indexed by the core representation (@Rep@)
--- of that type.
-type family Rep a
-
-
-
--- | void
-data V
--- | unit
-data U = U
--- | a dependency
-newtype D a = D a
--- | a recursive occurrence
-newtype R t = R t
--- | argument to a @* -> *@
-newtype F f c = F (f c)
--- | arguments to a @* -> * -> *@
-newtype FF ff c d = FF (ff c d)
--- | meta information
-newtype M i c = M c
-
--- | a named intermediate (user hook); crucially: @type instance Rep (N t) =
--- Rep t@.
-newtype N t = N t
-
-type instance Rep (N t) = Rep t   -- this is the crucial meaning of N
-
-
-
-concat `fmap` mapM derive [''V, ''U, ''D, ''R, ''F, ''FF, ''M, ''N]
-
-
-
-infixr 6 :*
-type (:*) = FF (,)
-
-
-
-
-
-{-
-type instance Polarity ([qK|*->*->*|] M) (ki :* kt :* U) = Neutral
-type instance Polarity ([qK|*->*|] (M i)) (kt :* U) = Pos
-
-type instance Polarity ([qK|*->*|] R) (ka :* U) = Pos
-
-type instance Polarity ([qK|(*->*)->*->*|] F) (kf :* kt :* U) = Pos
-type instance Polarity ([qK|*->*|] (F f)) (kt :* U) =
-  Polarity ([qK|*->*|] f) (kt :* U)
-
-type instance Polarity ([qK|(*->*->*)->*->*->*|] FF) (kff :* kt :* ks :* U) = Pos
-type instance Polarity ([qK|*->*->*|] (FF ff)) (kt :* ks :* U) =
-  Polarity ([qK|*->*->*|] ff) (kt :* ks :* U)
-type instance Polarity ([qK|*->*|] (FF ff t)) (ks :* U) =
-  Polarity ([qK|*->*|] (ff t)) (ks :* U)
--}
diff --git a/Data/Yoko/CoreTypes.hs b/Data/Yoko/CoreTypes.hs
deleted file mode 100644
--- a/Data/Yoko/CoreTypes.hs
+++ /dev/null
@@ -1,17 +0,0 @@
-{- |
-
-Module      :  Data.Yoko.CoreTypes
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Just the "Data.Yoko.Core" types -- doesn't export the constructors.
-
--}
-
-module Data.Yoko.CoreTypes (Rep, V, U, D, R, F, FF, M, N, (:*)) where
-
-import Data.Yoko.Core
diff --git a/Data/Yoko/Each.hs b/Data/Yoko/Each.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Each.hs
@@ -0,0 +1,38 @@
+{-# LANGUAGE KindSignatures, ConstraintKinds, MultiParamTypeClasses,
+  Rank2Types, FlexibleInstances, UndecidableInstances, TypeOperators #-}
+
+module Data.Yoko.Each (Each, each) where
+
+import Data.Yoko.TypeBasics
+import Data.Yoko.Representation
+
+
+
+type Each = Each_
+each :: Each cxt sum => Proxy cxt -> (forall a. cxt a => a -> b) -> sum -> b
+each = each_
+
+
+
+
+
+
+class Each_ cxt sum where
+  each_ :: Proxy cxt -> (forall a. cxt a => a -> b) -> sum -> b
+
+
+
+instance cxt a => Each_ cxt (N a) where each_ _ f (N x) = f x
+
+instance (Each_ cxt a, Each_ cxt b) => Each_ cxt (a :+: b) where
+  each_ c f = foldPlus (each c f) (each c f)
+
+instance Each_ cxt sum => Each_ cxt (DCsOf t sum) where
+  each_ c f = each c f . unDCsOf
+
+
+
+
+
+ex = putStrLn $ each (Proxy :: Proxy Show) show $
+       L (N 'n') `asTypeOf` R (N True)
diff --git a/Data/Yoko/Generic.hs b/Data/Yoko/Generic.hs
deleted file mode 100644
--- a/Data/Yoko/Generic.hs
+++ /dev/null
@@ -1,156 +0,0 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, QuasiQuotes, StandaloneDeriving,
-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,
-  MultiParamTypeClasses, TypeOperators, EmptyDataDecls  #-}
-
-{- |
-
-Module      :  Data.Yoko.Generic
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Representations of many Haskell types as compositions of "Data.Yoko.Core"
-types.
-
--}
-
-module Data.Yoko.Generic
-  (module Data.Yoko.Generic, module Data.Yoko.CoreTypes) where
-
-import Data.Yoko.CoreTypes
---import qualified Data.Yoko.Core as Core
-
-import Type.Yoko.Type
---import Type.Yoko.Universe ((:::)(..))
-
---import qualified Control.Arrow as Arrow
-                       
-
-{- | @RM@ stands is for \"recursively mediated\", and @m@ is the \"mediator (of
-recursive occurrences)\".
-
-@
-  data instance RM m V
-  data instance RM m U = U
-  newtype instance RM m (D a) = D a
-  newtype instance RM m (R t) = R (Med m t)
-  newtype instance RM m (F f c) = F (f (RM m c))
-  newtype instance RM m (FF ff c d) = FF (ff (RM m c) (RM m d))
-  newtype instance RM m (M i c) = M (RM m c)
-@
-
--}
-data family RM m c
-data instance RM m V
-data instance RM m U = U
-newtype instance RM m (D a) = D a
-newtype instance RM m (R t) = R (Med m t)
-newtype instance RM m (F f c) = F (f (RM m c))
-newtype instance RM m (FF ff c d) =
-  FF (ff (RM m c) (RM m d))
-newtype instance RM m (M i c) = M (RM m c)
-
--- | In @yoko@, the 'N' core type is used for a lightweight representation of
--- constructor types -- each will define its own instance of @RM (N _)@.
-type RMN m dc = RM m (N dc)
-
-type RMI = RM IdM
-type RMNI dc = RMN IdM dc
-
-
-
--- | @Generic@ represents a recursion-mediated type @N a@ as a
--- recursion-mediated @Rep a@. The opposite of \"representation\" is (the
--- represented) \"object\".
-class Generic a where
-  rep :: RM m (N a) -> RM m (Rep a)
-  obj :: RM m (Rep a) -> RM m (N a)
-
-{-asRep :: (Generic a, Generic b) => (RM m (Rep a) -> RM m (Rep b)) -> RM m (N a) -> RM m (N b)
-asRep f = obj . f . rep
-
-asGist :: (Gist c, Gist d) => (Gst c m -> Gst d n) -> RM m c -> RM n d
-asGist f = frip . f . gist
-
-convertR :: (Gist c, Gst c m ~ Gst c n) => RM m c -> RM n c
-convertR = asGist id-}
-
-
-{-
--- @gist@ folds the mediator @m@ into the type and forgets all the frippery of
--- the core representation. (The opposite of \"gist\" is \"frippery\".)
-type family Gst c m
-class Gist c where
-  gist :: RM m c -> Gst c m
-  frip :: Gst c m -> RM m c
-
-data AsRep u t where AsRep :: u (Rep t) -> AsRep u t
-instance (Rep t ::: u) => t ::: AsRep u where inhabits = AsRep inhabits
-
-data GistD c where GistD :: Gist c => GistD c
-instance Gist c => c ::: GistD where inhabits = GistD
-gistD :: GistD c -> RM m c -> Gst c m; gistD GistD = gist
-fripD :: GistD c -> Gst c m -> RM m c; fripD GistD = frip
-
-
-
-type instance Gst (F f c) m = f (Gst c m)
-instance (Functor f, Gist c) => Gist (F f c) where
-  gist (F x) = fmap gist x
-  frip = F . fmap frip
-type instance Gst (FF Either c d) m = Either (Gst c m) (Gst d m)
-instance (Gist c, Gist d) => Gist (FF Either c d) where
-  gist = (gist Arrow.+++ gist) . unFF
-  frip = FF . (frip Arrow.+++ frip)
-type instance Gst (FF (,) c d) m = (,) (Gst c m) (Gst d m)
-instance (Gist c, Gist d) => Gist (FF (,) c d) where
-  gist = (gist Arrow.*** gist) . unFF
-  frip = FF . (frip Arrow.*** frip)
-type instance Gst (D a) m = a
-instance Gist (D a) where gist (D x) = x; frip = D
-type instance Gst (M i c) m = Gst c m
-instance Gist c => Gist (M i c) where
-  gist = gist . unM; frip = M . frip
-type instance Gst (R t) m = Med m t
-instance Gist (R t) where gist (R x) = x; frip = R
-type instance Gst U m = ()
-instance Gist U where gist _ = (); frip _ = U
-type instance Gst V m = Core.V
-instance Gist V where gist = absurd "gist[V]"; frip _ = void "gist[V]"
-type instance Gst (N n) m = Gst (Rep n) m
-instance (Generic t, Gist (Rep t)) => Gist (N t) where
-  gist = gist . rep; frip = obj . frip
--}
-
-
-unD :: RM m (D a) -> a
-unD (D x) = x
-
-unM :: RM m (M i c) -> RM m c
-unM (M x) = x
-
-unR :: RM m (R t) -> Med m t
-unR (R x) = x
-deriving instance Eq (Med m t) => Eq (RM m (R t))
-deriving instance Show (Med m t) => Show (RM m (R t))
-
-instance Eq (RM m V) where _ == _ = True -- undefined?
-instance Show (RM m V) where show _ = "<void>"
-void :: String -> RM m V
-void n = error $ "GenericR.void: " ++ n
-absurd :: String -> RM m V -> a
-absurd n = error $ "GenericR.absurd: " ++ n
-
-unF (F x) = x
-unFF (FF x) = x
-deriving instance Eq (ff (RM m c) (RM m d)) => Eq (RM m (FF ff c d))
-deriving instance Show (ff (RM m c) (RM m d)) => Show (RM m (FF ff c d))
-
-
-
-
-
-concat `fmap` mapM derive [''RM]
diff --git a/Data/Yoko/HCompos.hs b/Data/Yoko/HCompos.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/HCompos.hs
@@ -0,0 +1,70 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses,
+  FlexibleContexts, FlexibleInstances, UndecidableInstances,
+  ScopedTypeVariables  #-}
+
+{-# OPTIONS_GHC -fcontext-stack=250 #-}
+
+module Data.Yoko.HCompos (Idiom, HCompos(..)) where
+
+import Data.Yoko.TypeBasics
+import Data.Yoko
+
+
+
+import Control.Applicative
+
+
+
+
+
+instance HCompos cnv sum t => HCompos cnv (DCsOf a sum) t where
+  hcompos cnv = hcompos cnv . unDCsOf
+
+
+
+
+
+type family Idiom cnv :: * -> *
+class Applicative (Idiom cnv) => HCompos cnv a t where
+  hcompos :: cnv -> a -> Idiom cnv t
+
+
+
+
+
+instance (HCompos cnv a t, HCompos cnv b t
+         ) => HCompos cnv (a :+: b) t where
+  hcompos cnv = foldPlus (hcompos cnv) (hcompos cnv)
+
+-- NB only works if there's exactly one matching constructor
+instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs t),
+          HComposRs cnv (Rep dc) (Rep dc'),
+          DC dc', Range dc' ~ t, DT t
+         ) => HCompos cnv (N dc) t where
+  hcompos cnv = 
+    foldN $ liftA (rejoin . (id :: dc' -> dc') . obj) . mapRs cnv . rep
+
+
+
+type family FindDCs s sum
+type instance FindDCs s (N dc) =
+  If (Equal s (Tag dc)) (Just (N dc)) Nothing
+type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)
+
+
+
+-- applies cnv to every Rec in a product; identity on other factors
+class Applicative (Idiom cnv) => HComposRs cnv prod prod' where
+  mapRs :: cnv -> prod -> Idiom cnv prod'
+
+instance HCompos cnv a b => HComposRs cnv (Rec a) (Rec b) where
+  mapRs cnv (Rec x) = Rec <$> hcompos cnv x
+
+instance Applicative (Idiom cnv) => HComposRs cnv (Dep a) (Dep a) where
+  mapRs _ = pure
+instance Applicative (Idiom cnv) => HComposRs cnv U       U       where
+  mapRs _ = pure
+
+instance (HComposRs cnv a a', HComposRs cnv b b'
+         ) => HComposRs cnv (a :*: b) (a' :*: b') where
+  mapRs cnv (a :*: b) = (:*:) <$> mapRs cnv a <*> mapRs cnv b
diff --git a/Data/Yoko/InDT.hs b/Data/Yoko/InDT.hs
deleted file mode 100644
--- a/Data/Yoko/InDT.hs
+++ /dev/null
@@ -1,78 +0,0 @@
-{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses,
-  FlexibleContexts, UndecidableInstances, Rank2Types #-}
-
-{- |
-
-Module      :  Data.Yoko.InDT
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Various universes determined by a data constructor type's suitability to be
-embedded in a data type.
-
--}
-module Data.Yoko.InDT where
-
-import Type.Yoko
-
-import Data.Yoko.Generic
-import Data.Yoko.Reflect
-
-
-
--- | A type @t@ inhabits @HasTagRepU tag c@ if @t@ is a 'DT' and there exists a @t@
--- constructor satisfying @'TagRepIs' tag c@.
-data HasTagRepU tag c t where
-  HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->
-                HasTagRepU tag c t
-instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)
-         ) => t ::: HasTagRepU tag c where inhabits = HasTagRepU inhabits
-
--- | Given @HasTagRepU tag c t@, a trivially-mediated @c@ value can be embedded into
--- @t@.
-hasTagRepU :: HasTagRepU tag c t -> RMI c -> t
-hasTagRepU (HasTagRepU d) = w d where
-  w :: Exists (DCOf t :&& TagRepIs tag c) dcs -> RMI c -> t
-  w (Here (x@(DCOf _) :&& TagRepIs)) = fr_DCOf x . obj
-  w (OnLeft u) = w u; w (OnRight u) = w u
-
-
-
-
-
--- | Often times, we're interested in the universe of types accomodating a data
--- constructor's image under some type-function.
-type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc))
-
--- | A constructor type @dc@ inhabits @ImageHasTagRepU t fn@ if
---
--- 1. @fn@ can be mapped across the recursive occurrences in @dc@, and
---
--- 2. @t@ has a constructor isomorphic to the @fn@-image of @dc@ 
-data ImageInDTU t fn dc where
-  ImageInDTU :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)
-                ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTU t fn dc
-instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc
-         ) => dc ::: ImageInDTU t fn where
-  inhabits = ImageInDTU inhabits
-
--- | Given @ImageInDTU t fn dc@, a trivially-mediated @dc@ value can be
--- embedded into @t@.
-imageInDTU :: (forall t. fn IdM t) -> ImageInDTU t fn dc -> RMNI dc -> t
-imageInDTU fn (ImageInDTU d) = hasTagRepU d . apply (CMap fn) . rep
-
--- | Same as @ImageInDTD@, but uses an implicitly applicative function.
-data ImageInDTDA t fn dc where
-  ImageInDTDA :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM)
-                 ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTDA t fn dc
-instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc
-         ) => dc ::: ImageInDTDA t fn where
-  inhabits = ImageInDTDA inhabits
-
-imageInDTAU :: Functor (Idiom (fn IdM)) =>
-               (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t
-imageInDTAU fn (ImageInDTDA d) = fmap (hasTagRepU d) . applyA (CMap fn) . rep
diff --git a/Data/Yoko/MaybeKind.hs b/Data/Yoko/MaybeKind.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/MaybeKind.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}
+
+module Data.Yoko.MaybeKind where
+
+import Type.Booleans
+
+data Nothing
+data Just (x :: *)
+
+type family IsJust (x :: *) :: * -- returns Bool, ideally
+type instance IsJust Nothing = False
+type instance IsJust (Just x) = True
+
+type family MaybePlus1 (x :: *) (y :: *) :: *
+type instance MaybePlus1 Nothing y = y
+type instance MaybePlus1 (Just x) Nothing = Just x
+
+type family MaybeMap (f :: * -> *) (x :: *) :: *
+type instance MaybeMap f (Just x) = Just (f x)
+type instance MaybeMap f Nothing = Nothing
diff --git a/Data/Yoko/Reduce.hs b/Data/Yoko/Reduce.hs
deleted file mode 100644
--- a/Data/Yoko/Reduce.hs
+++ /dev/null
@@ -1,77 +0,0 @@
-{-# LANGUAGE QuasiQuotes, ScopedTypeVariables, TypeOperators, GADTs,
-  MultiParamTypeClasses, FlexibleContexts, TypeSynonymInstances,
-  FlexibleInstances, UndecidableInstances, TypeFamilies #-}
-
-{- |
-
-Module      :  Data.Yoko.Reduce
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-A @t@-algebra reduces a disbanded @t@ into a mediation of @t@.
-
--}
-module Data.Yoko.Reduce
-  (Alg, Algebra(..), AlgebraU(..),
-   algebraFin, AlgebraDT(..), AlgebraUni, AlgebraDC(..)) where
-
-import Type.Yoko
-
-import Data.Yoko.Generic
-import Data.Yoko.Reflect
-
-
-
-
-
--- | A @t@-algebra reduces a disbanded @t@ to the same mediation of @t@.
-type Alg m t = Disbanded m t -> Med m t
-newtype Algebra m t = Alg (Alg m t)
-type instance Unwrap (Algebra m) t = Alg m t
-instance Wrapper (Algebra m) where wrap = Alg; unwrap (Alg x) = x
-
-data AlgebraU m t where
-  AlgebraU :: (DT t, AlgebraDT m t) => AlgebraU m t
-instance (DT t, AlgebraDT m t
-         ) => t ::: AlgebraU m where inhabits = AlgebraU
-
-
-
-
-
-algebraFin :: (AlgebraUni m (Inhabitants u), Finite u) =>
-             AnRMN m u -> Med m (LeftmostRange (Inhabitants u))
-algebraFin = algebraUni . finiteNP
-
-
-
--- | @algebraDT@ determines the algebra from the type and mediator.
-class DT t => AlgebraDT m t where algebraDT :: Disbanded m t -> Med m t
-
-
--- | @algebraUni@ determines the \"algebra\" from the type-sum and mediator.
-class AlgebraUni m dcs where
-  algebraUni :: AnRMN m (Uni dcs) -> Med m (LeftmostRange dcs)
-
-instance (Med m (LeftmostRange ts) ~ Med m (LeftmostRange us),
-          AlgebraUni m ts, AlgebraUni m us) => AlgebraUni m (ts :+ us) where
-  algebraUni = algebraUni `two` algebraUni
-instance AlgebraDC m dc => AlgebraUni m (N dc) where
-  algebraUni (NP (Uni (Here Refl)) x) = algebraDC x
-
--- | @algebraDC@ determines the \"alegbra\" from the constructor type and
--- mediator.
-class DC dc => AlgebraDC m dc where algebraDC :: RMN m dc -> Med m (Range dc)
-
-
-
-type OneOf ts = NP (Uni ts)
-
-two :: (OneOf ts f -> a) -> (OneOf us f -> a) -> (OneOf (ts :+ us) f -> a)
-two f g (NP (Uni tag) x) = case tag of
-  OnLeft u -> f $ NP (Uni u) x
-  OnRight v -> g $ NP (Uni v) x
diff --git a/Data/Yoko/Reflect.hs b/Data/Yoko/Reflect.hs
deleted file mode 100644
--- a/Data/Yoko/Reflect.hs
+++ /dev/null
@@ -1,121 +0,0 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs,
-  ScopedTypeVariables, FlexibleContexts, UndecidableInstances, QuasiQuotes,
-  TypeOperators, TypeSynonymInstances, Rank2Types, ViewPatterns #-}
-
-{- |
-
-Module      :  Data.Yoko.Reflect
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Definitions on top of the basic @yoko@ reflection concepts "Data.Yoko.ReflectBase".
-
--}
-
-module Data.Yoko.Reflect
-  (module Data.Yoko.Reflect, module Data.Yoko.ReflectBase) where
-
-import Type.Yoko
-
-import Data.Yoko.Generic
-import Data.Yoko.ReflectBase hiding (DCU)
-
-
-
-type instance Tag (N dc) = Tag dc
-
-
-
-type instance Recurs (D a) = V
-type instance Recurs (F f c) = Recurs c
-type instance Recurs (FF ff c d) =
-  NormW (Recurs c) (Recurs d) -- NormW avoiding duplication
-type instance Recurs (M i c) = Recurs c
-type instance Recurs (N t) = Recurs (Rep t)
-type instance Recurs (R t) = N t
-type instance Recurs U = V
-type instance Recurs V = V
-
-type SiblingsU t = Uni (Siblings t)
-
-
-
-type OnlyDC t = UnN (DCs t)
-type family UnN a
-type instance UnN (N dc) = dc
-
-uniqueDC :: (DT t, N (OnlyDC t) ~ DCs t, t ~ Range (OnlyDC t)) => t -> RMNI (OnlyDC t)
-uniqueDC = uniqueRMN . disband
-
-uniqueRMN :: (Finite u, N (UnN (Inhabitants u)) ~ Inhabitants u
-             ) => AnRMN m u -> RMN m (UnN (Inhabitants u))
-uniqueRMN x = case finiteNP x of NP (Uni (Here Refl)) x -> x
-
-uniqueRMN' :: (Finite (DCOf (Range dc)), N dc ~ DCs (Range dc)
-              ) => AnRMN m (DCOf (Range dc)) -> RMN m dc
-uniqueRMN' = uniqueRMN
-
-
-
-
-
-data IsDC dc where IsDC :: DC dc => IsDC dc
-type instance Pred IsDC t = True
-instance DC dc => dc ::: IsDC where inhabits = IsDC
-
-newtype RMNTo m b dc = RMNTo {rmnTo :: RMN m dc -> b}
-type instance Unwrap (RMNTo m b) dc = RMN m dc -> b
-instance Wrapper (RMNTo m b) where wrap = RMNTo; unwrap = rmnTo
-
-
-
-
--- | Just a specialization: @dcDispatch = (. disband) . dcDispatch'@.
-dcDispatch :: DT t => NT (DCOf t) (RMNTo IdM b) -> t -> b
-dcDispatch = (. disband) . dcDispatch'
-
--- | Just a specialization: @dcDispatch' nt ('NP' ('DCOf' tag) fds) = 'appNT'
--- nt tag fds@.
-dcDispatch' :: DT t => NT (DCOf t) (RMNTo IdM b) -> Disbanded IdM t -> b
-dcDispatch' nt (NP tag fds) = appNT nt tag fds
-
-
-
-
-{- | A fundamental notion of identity in @yoko@, the @TagRepIs tag c@ universe
-contains all constructor types @dc@ where @(Tag dc ~ tag, c ~ Rep dc)@.
-
-@
-  type instance Pred (TagRepIs tag c) dc =
-    And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))
-@
-
--}
-data TagRepIs tag c dc where
-  TagRepIs :: (Tag dc ~ tag, c ~ Rep dc) => TagRepIs tag c dc
-instance (Tag dc ~ tag, c ~ Rep dc) => dc ::: TagRepIs tag c where
-  inhabits = TagRepIs
-type instance Pred (TagRepIs tag c) dc =
-  And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))
-
-{-data TagGistEQ tag gst m dc where
-  TagGistEQ :: (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst
-               ) => TagGistEQ tag gst m dc
-instance (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst
-         ) => dc ::: TagGistEQ tag gst m where inhabits = TagGistEQ
-type instance Pred (TagGistEQ tag gst m) dc =
-  And (IsEQ (Compare (Tag dc) tag))
-      (IsEQ (Compare (Gst (N dc) m) gst))-}
-
-
-
-
-
--- | Just a specialization: @bandDCs = band@.
-bandDCs :: DT t => Disbanded IdM t -> t; bandDCs = band
-
-fr_DCOf :: DCOf t dc -> RMNI dc -> t; fr_DCOf (DCOf _) = fr
diff --git a/Data/Yoko/ReflectBase.hs b/Data/Yoko/ReflectBase.hs
deleted file mode 100644
--- a/Data/Yoko/ReflectBase.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, TypeOperators,
-  FlexibleContexts, ScopedTypeVariables, ViewPatterns, FlexibleInstances,
-  QuasiQuotes, UndecidableInstances, Rank2Types #-}
-
-{- |
-
-Module      :  Data.Yoko.ReflectBase
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-The basic @yoko@ reflection concepts.
-
--}
-module Data.Yoko.ReflectBase where
-
-import Type.Yoko
-import Data.Yoko.Generic
-
-
--- | The @Tag@ of a constructor type is a type-level reflection of its
--- constructor name.
-type family Tag dc
-
--- | The @Recurs@ of a constructor type is the type-"Type.Yoko.Sum" of types
--- that occur in this constructor. NB: @Recurs t `isSubsumedBy` Siblings (Range
--- dc)@.
-type family Recurs t
-
--- | The \"Datatype Constructor\" class.
-class (DT (Range dc), dc ::: DCU (Range dc), Generic dc) => DC dc where
-  -- | The string name of this constructor.
-  occName :: [qP|dc|] -> String 
-
-  -- | The range of this constructor.
-  type Range dc
-
-  -- | The evidence that this constructor inhabits the datatype constructor
-  -- universe of its range.
-  tag :: DCOf (Range dc) dc; tag = inhabits
-
-  -- | Project this constructor from its range.
-  to :: Range dc -> Maybe (RMNI dc)
-  to (disband -> NP tg fds) = case eqT tg (tag :: DCOf (Range dc) dc) of
-    Just Refl -> Just fds
-    _ -> Nothing
-
-  -- | Embed this constructor in its range.
-  fr :: RMNI dc -> Range dc
-
--- | Evidence that @t@ is the range of the constructor type @dc@.
-data DCOf t dc where DCOf :: (DC dc, t ~ Range dc) => DCU t dc -> DCOf t dc
-instance (DC dc, t ~ Range dc) => dc ::: DCOf t where inhabits = DCOf inhabits
-type instance Inhabitants (DCOf t) = Inhabitants (DCU t)
-instance Finite (DCU t) => Finite (DCOf t) where toUni (DCOf x) = toUni x
-type instance Pred (DCOf t) dc = Elem dc (DCs t)
-instance EqT (DCU t) => EqT (DCOf t) where eqT (DCOf x) (DCOf y) = eqT x y
-
-data SiblingOf t s where SiblingOf :: (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => Uni (Siblings t) s -> SiblingOf t s
-instance (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => s ::: SiblingOf t where inhabits = SiblingOf inhabits
-type instance Inhabitants (SiblingOf t) = Siblings t
-instance Finite (SiblingOf t) where toUni (SiblingOf x) = x
-type instance Pred (SiblingOf t) s = Elem s (Siblings t)
-instance EqT (SiblingOf t) where eqT (SiblingOf x) (SiblingOf y) = eqT x y
-
-
-
-type AnRMN m u = NP u (RM m :. N)
-type Disbanded m t = AnRMN m (DCOf t)
-
-disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)
-disbanded fds = NP tag fds
-
-band :: Disbanded IdM t -> t
-band (NP (DCOf _) fds) = fr fds
-
-
-
--- @LeftmostRange@ returns the @Range@ of the leftmost type in a type-sum.
-type family LeftmostRange dcs
-type instance LeftmostRange (N dc) = Range dc
-type instance LeftmostRange (c :+ d) = LeftmostRange c
-
-type DCs t = Inhabitants (DCOf t)
-
--- | The "DataType" class.
-class (Finite (DCU t), EqT (DCU t),
-       DCs t ::: All (DCOf t), -- DCs t ::: All (AsRep GistU),
-       Siblings t ::: All (SiblingOf t)
-      ) => DT t where
-  -- | The string name of this datatype's original package.
-  packageName :: [qP|t|] -> String
-  -- | The string name of this datatype's original module.
-  moduleName :: [qP|t|] -> String
-
-  -- | A type-sum of the types in this type's binding group, including
-  -- itself. @Siblings t@ ought to be the same for every type @t@ in the
-  -- binding group. (It also ought to be equivalent to the transitive closure
-  -- of @Recurs . DCs@, by definition.)
-  type Siblings t
- 
-  -- | The data constructor universe. 'DCOf' is to be preferred as much as
-  -- possible.
-  data DCU t :: * -> * -- universe of constructor types
-
-  -- | /Disband/ this type into one of its data constructors.
-  disband :: t -> Disbanded IdM t
diff --git a/Data/Yoko/Representation.hs b/Data/Yoko/Representation.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Representation.hs
@@ -0,0 +1,96 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, TemplateHaskell,
+  UndecidableInstances, EmptyDataDecls #-}
+
+module Data.Yoko.Representation where
+
+import Data.Yoko.TypeBasics
+
+
+
+data U = U
+newtype F a = F a
+infixr 6 :*:
+data a :*: b = a :*: b
+
+data Void
+newtype N a = N a
+infixl 6 :+:
+data a :+: b = L a | R b deriving (Eq, Show, Ord, Read)
+
+
+
+newtype Par1 f a = Par1 (f a)
+
+
+
+newtype Dep a = Dep a
+newtype Rec a = Rec a
+
+
+
+type family Rep a
+
+
+
+class Generic a where rep :: a -> Rep a; obj :: Rep a -> a
+
+
+unDep (Dep x) = x
+
+unRec (Rec x) = x
+mapRec f (Rec x) = Rec (f x)
+
+unPar1 (Par1 x) = x
+
+unN (N x) = x
+foldN f = f . unN
+
+mapN f = N . foldN f
+
+foldPlus f g x = case x of
+  L x -> f x   ;   R x -> g x
+
+mapPlus f g = foldPlus (L . f) (R . g)
+
+mapTimes f g (a :*: b) = f a :*: g b
+
+foldTimes comb f g (a :*: b) = comb (f a) (g b)
+
+
+
+type family DistMaybePlus a b
+type instance DistMaybePlus Nothing b = b
+type instance DistMaybePlus (Just a) Nothing = Just a
+type instance DistMaybePlus (Just a) (Just b) = Just (a :+: b)
+
+
+
+data Z; data S n
+type family Add n m
+type instance Add Z m = m
+type instance Add (S n) m = S (Add n m)
+
+type family CountRs rep
+type instance CountRs (Dep a) = Z
+type instance CountRs (Rec a) = S Z
+type instance CountRs U = Z
+type instance CountRs (a :*: b) = Add (CountRs a) (CountRs b)
+
+
+
+
+
+-- carrying around the original type supplants many ascriptions
+newtype DCsOf t sum = DCsOf sum   ;   unDCsOf (DCsOf x) = x
+instance Functor (DCsOf t) where fmap f = DCsOf . f . unDCsOf
+
+infixl 6 |||
+(|||) :: (DCsOf t sumL -> a) -> (DCsOf t sumR -> a) ->
+         DCsOf t (sumL :+: sumR) -> a
+(|||) f g = foldPlus f g . mapPlus DCsOf DCsOf . unDCsOf
+
+
+
+
+
+concat `fmap` mapM derive [''Dep, ''Rec, ''U, ''(:*:), ''N, ''(:+:)]
diff --git a/Data/Yoko/TypeBasics.hs b/Data/Yoko/TypeBasics.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/TypeBasics.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds, PolyKinds #-}
+
+module Data.Yoko.TypeBasics (
+  module Data.Yoko.MaybeKind,
+  module Type.Booleans,
+  Proxy(..),
+  Equal,
+  IsPrefixOf,
+  derive, encode
+  ) where
+
+import Type.Booleans
+import Data.Yoko.MaybeKind
+
+--import Data.Proxy.TH (Proxy(..))
+import Type.Spine
+import Type.Ord (IsEQ)
+import Type.Serialize
+import Type.Ord.SpineSerialize (Compare)
+
+
+
+data Proxy a = Proxy
+
+
+
+type Equal a b = IsEQ (Compare a b)
+
+
+
+type family IsPrefixOf (pre :: *) (s :: *) :: * -- emulated primitive
+
+
+
+derive n = do
+  d <- spineType n
+  (d ++) `fmap` serializeTypeAsHash n
diff --git a/Data/Yoko/TypeSums.hs b/Data/Yoko/TypeSums.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/TypeSums.hs
@@ -0,0 +1,115 @@
+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, TypeOperators,
+  NoPolyKinds, DataKinds #-}
+
+{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,
+  ScopedTypeVariables, EmptyDataDecls #-}
+
+{-# OPTIONS_GHC -fcontext-stack=250 #-}
+
+module Data.Yoko.TypeSums (DistMaybePlus, (:-:),
+                           Embed, embed, inject,
+                           Partition, project, partition) where
+
+import Data.Yoko.TypeBasics
+import Data.Yoko.Representation
+
+import Control.Arrow (left)
+
+import Data.Yoko.TypeSumsAux (Partition_N(..))
+
+
+
+
+
+class Embed sub sup where embed_ :: sub -> sup
+
+embed :: Embed sub sup => sub -> sup
+embed = embed_
+
+inject :: Embed (N a) sum => a -> sum
+inject = embed . N
+
+
+
+class Partition sup subL subR where partition_ :: sup -> Either subL subR
+
+partition :: Partition sup sub (sup :-: sub) =>
+             sup -> Either sub (sup :-: sub)
+partition = partition_
+
+project :: Partition sum (N a) (sum :-: N a) => sum -> Either a (sum :-: N a)
+project = left unN . partition_
+
+
+
+
+
+data Here a
+data TurnLeft path
+data TurnRight path
+
+type family Locate a sum
+type instance Locate a (N x) = If (Equal x a) (Just (Here a)) Nothing
+type instance Locate a (l :+: r) =
+  MaybeMap TurnLeft (Locate a l) `MaybePlus1`
+  MaybeMap TurnRight (Locate a r)
+type instance Locate a Void = Nothing
+
+type Elem a sum = IsJust (Locate a sum)
+
+
+
+
+
+class InjectAt path a sum where injectAt :: Proxy path -> a -> sum
+instance InjectAt (Here a) a (N a) where injectAt _ = N
+instance InjectAt path a l => InjectAt (TurnLeft path) a (l :+: r) where
+  injectAt _ = L . injectAt (Proxy :: Proxy path)
+instance InjectAt path a r => InjectAt (TurnRight path) a (l :+: r) where
+  injectAt _ = R . injectAt (Proxy :: Proxy path)
+
+
+
+
+
+instance (Locate x sup ~ Just path, InjectAt path x sup) => Embed (N x) sup where
+  embed_ = injectAt (Proxy :: Proxy path) . unN
+instance (Embed l sup, Embed r sup) => Embed (l :+: r) sup where
+  embed_ = foldPlus embed embed
+
+
+
+
+
+infixl 6 :-:
+type family (:-:) sum sum2
+type instance (:-:) (N x) sum2 = If (Elem x sum2) Void (N x)
+type instance (:-:) (l :+: r) sum2 = Combine (l :-: sum2) (r :-: sum2)
+
+
+type family Combine sum sum2
+type instance Combine Void x = x
+type instance Combine (N x) Void = N x
+type instance Combine (N x) (N y) = N x :+: N y 
+type instance Combine (N x) (l :+: r) = N x :+: (l :+: r)
+type instance Combine (l :+: r) Void = l :+: r
+type instance Combine (l :+: r) (N y) = (l :+: r) :+: N y
+type instance Combine (ll :+: rl) (lr :+: rr) = (ll :+: rl) :+: (lr :+: rr)
+
+
+
+
+instance (Partition_N (Elem x subL) x subL subR
+         ) => Partition (N x) subL subR where
+  partition_ = partition_N (Proxy :: Proxy (Elem x subL))
+
+instance (Partition a subL subR, Partition b subL subR
+         ) => Partition (a :+: b) subL subR where
+  partition_ = foldPlus partition_ partition_
+
+
+
+instance Embed (N x) subR => Partition_N False x subL subR where
+  partition_N _ = Right . embed
+instance Embed (N x) subL => Partition_N True  x subL subR where
+  partition_N _ = Left  . embed
diff --git a/Data/Yoko/TypeSumsAux.hs b/Data/Yoko/TypeSumsAux.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/TypeSumsAux.hs
@@ -0,0 +1,12 @@
+{-# LANGUAGE MultiParamTypeClasses, KindSignatures #-}
+
+module Data.Yoko.TypeSumsAux where
+
+import Data.Yoko.TypeBasics
+import Data.Yoko.Representation
+
+
+
+-- this * is Bool, ideally
+class Partition_N (bn :: *) x subL subR where
+  partition_N :: Proxy bn -> N x -> Either subL subR
diff --git a/Examples/Ex.hs b/Examples/Ex.hs
deleted file mode 100644
--- a/Examples/Ex.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-module Examples.Ex where
-
-data Tree1 a = Leaf a | Branch (Tree1 a) (Tree1 a)
-
-data Even a = Zero | Even a (Odd a)
-data Odd  a = Odd a (Even a)
diff --git a/Examples/ExG.hs b/Examples/ExG.hs
deleted file mode 100644
--- a/Examples/ExG.hs
+++ /dev/null
@@ -1,60 +0,0 @@
-{-# LANGUAGE EmptyDataDecls, TypeFamilies, TemplateHaskell, FlexibleInstances, TypeOperators, MultiParamTypeClasses, GADTs, UndecidableInstances #-}
-
-{-# OPTIONS_GHC -fcontext-stack=50 #-}
-
-module Examples.ExG where
-
-import qualified Examples.Ex as Ex
-import Examples.ReflectAux
-
-
-
-data Leaf a; data Branch a
-
-data Zero a; data Even a; data Odd a
-
-concat `fmap` mapM derive
-  [''Ex.Tree1, ''Leaf, ''Branch,
-   ''Ex.Even, ''Zero, ''Even,
-   ''Ex.Odd, ''Odd]
-
-type instance Tag (Leaf a) = $(return $ encode "Leaf")
-newtype instance RM m (N (Leaf a)) = Leaf a
-instance (True ~ IsEQ (Compare a a)) => DC (Leaf a) where
-  occName _ = "Leaf"
-  type Range (Leaf a) = Ex.Tree1 a
-  fr ~(Leaf a) = Ex.Leaf a
-type instance Rep (Leaf a) = D a
-instance Generic (Leaf a) where
-  rep ~(Leaf a) = D a
-  obj ~(D a) = Leaf a
-
-type instance Tag (Branch a) = $(return $ encode "Branch")
-data instance RM m (N (Branch a)) =
-  Branch (Med m (Ex.Tree1 a)) (Med m (Ex.Tree1 a))
-instance (True ~ IsEQ (Compare a a)) => DC (Branch a) where
-  occName _ = "Branch"
-  type Range (Branch a) = Ex.Tree1 a
-  fr ~(Branch a b) = Ex.Branch a b
-type instance Rep (Branch a) = R (Ex.Tree1 a) :* R (Ex.Tree1 a)
-instance Generic (Branch a) where
-  rep ~(Branch a b) = FF (R a, R b)
-  obj ~(FF (R a, R b)) = Branch a b
-
-type instance Inhabitants (DCU (Ex.Tree1 a)) = N (Leaf a) :+ N (Branch a)
-instance (True ~ IsEQ (Compare a a)) => DT (Ex.Tree1 a) where
-  packageName _ = "yoko-0.1"
-  moduleName _ = "Examples.ExG"
-  type Siblings (Ex.Tree1 a) = N (Ex.Tree1 a)
-  data DCU (Ex.Tree1 a) dc where
-    Leaf_ :: DCU (Ex.Tree1 a) (Leaf a)
-    Branch_ :: DCU (Ex.Tree1 a) (Branch a)
-  disband (Ex.Leaf a) = disbanded $ Leaf a
-  disband (Ex.Branch a b) = disbanded $ Branch a b
-instance Finite (DCU (Ex.Tree1 a)) where
-  toUni x = Uni $ case x of
-    Leaf_ -> OnLeft $ Here Refl
-    Branch_ -> OnRight $ Here Refl
-instance (a ~ b) => (Leaf b) ::: DCU (Ex.Tree1 a) where inhabits = Leaf_
-instance (a ~ b) => (Branch b) ::: DCU (Ex.Tree1 a) where inhabits = Branch_
-instance EqT (DCU (Ex.Tree1 a)) where eqT = eqTFin
diff --git a/Examples/InnerBase.hs b/Examples/InnerBase.hs
deleted file mode 100644
--- a/Examples/InnerBase.hs
+++ /dev/null
@@ -1,8 +0,0 @@
-module Examples.InnerBase where
-
-import Examples.TermBase (Type(..))
-
-data Inner = Lam Type Inner
-           | Var Int
-           | App Inner Inner
-  deriving Show
diff --git a/Examples/InnerGeneric.hs b/Examples/InnerGeneric.hs
deleted file mode 100644
--- a/Examples/InnerGeneric.hs
+++ /dev/null
@@ -1,90 +0,0 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,
-  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,
-  TypeSynonymInstances, EmptyDataDecls #-}
-
-{-# OPTIONS_GHC -fcontext-stack=250 #-}
-
-{- |
-
-Module      :  Examples.InnerGeneric
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-The declaration that hook 'Examples.InnerBase.Inner' into @yoko@. This will
-eventually be generated via Template Haskell.
-
--}
-module Examples.InnerGeneric where
-
-import qualified Examples.TermBase as B
-import Examples.InnerBase (Inner)
-import qualified Examples.InnerBase as I
-
-import Examples.ReflectAux
-
-data Lam; data Var; data App
-
-concat `fmap` mapM derive [''Inner, ''Lam, ''Var, ''App]
-
-type instance Tag Lam = $(return $ encode "Lam")
-type instance Recurs Lam = N Inner
-instance DC Lam where
-  occName _ = "Lam"
-  type Range Lam = Inner
-  fr ~(Lam ty tm) = I.Lam ty tm
-data instance RM m (N Lam) = Lam B.Type (Med m Inner)
-type instance Tag Var = $(return $ encode "Var")
-type instance Recurs Var = V
-instance DC Var where
-  occName _ = "Var"
-  type Range Var = Inner
-  fr ~(Var i) = I.Var i
-data instance RM m (N Var) = Var Int
-type instance Tag App = $(return $ encode "App")
-type instance Recurs App = N Inner
-instance DC App where
-  occName _ = "App"
-  type Range App = Inner
-  fr ~(App tm0 tm1) = I.App tm0 tm1
-data instance RM m (N App) = App (Med m Inner) (Med m Inner)
-instance DT Inner where
-  packageName _ = "datatype-reflect"
-  moduleName _ = "InnerBase"
-  type Siblings Inner = N Inner
-  data DCU Inner dc where
-    Lam_ :: DCU Inner Lam; Var_ :: DCU Inner Var
-    App_ :: DCU Inner App
-  disband (I.Lam ty tm)   = disbanded $ Lam ty tm
-  disband (I.Var i)       = disbanded $ Var i
-  disband (I.App tm0 tm1) = disbanded $ App tm0 tm1
-type instance Inhabitants (DCU Inner) = (N Lam :+ N Var) :+ N App
-instance Finite (DCU Inner) where
-  toUni Lam_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits
-instance Etinif (DCU Inner) where
-  frUni (Uni x) = case x of
-    (OnLeft  (OnLeft  (Here Refl))) -> Lam_
-    (OnLeft  (OnRight (Here Refl))) -> Var_
-    (OnRight (Here Refl))  -> App_
-instance (t ::: Uni (DCs Inner)) => t ::: DCU Inner where
-  inhabits = frUni inhabits
-instance EqT (DCU Inner) where eqT = eqTFin
-
-
-
-
-type instance Rep Var = D Int
-instance Generic Var where
-  rep ~(Var i) = D i
-  obj ~(D i) = Var i
-type instance Rep Lam = D B.Type :* R Inner
-instance Generic Lam where
-  rep ~(Lam ty tm) = FF (D ty, R tm)
-  obj ~(FF (D ty, R tm)) = Lam ty tm
-type instance Rep App = R Inner :* R Inner
-instance Generic App where
-  rep ~(App tm0 tm1) = FF (R tm0, R tm1)
-  obj ~(FF (R tm0, R tm1)) = App tm0 tm1
diff --git a/Examples/LL.hs b/Examples/LL.hs
deleted file mode 100644
--- a/Examples/LL.hs
+++ /dev/null
@@ -1,63 +0,0 @@
-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses,
-  FlexibleInstances, UndecidableInstances #-}
-
-{-# OPTIONS_GHC -fcontext-stack=200 #-}
-
-module Examples.LL where
-
-import qualified Examples.InnerBase as I
-
-import qualified Data.Set as Set
-import qualified Data.IntMap as IM
-
-import Examples.LLBasics
-
-import qualified Examples.InnerGeneric as IG
-import qualified Examples.LLGeneric ()
-
-import Data.Yoko
-
-
-
-
-
-lambdaLift :: Inner -> [Type] -> Prog
-lambdaLift x e = Prog (reverse tlds) main where
-  (main, tlds) = runMnd (ll x) (e, IM.empty, 0)
-
-llLam (IG.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where
-  updE (rho, rn) = (ty : rho, support `prepend` rn) where
-    support =
-      IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm
-llVar (IG.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i
-
----------------------------------------- default
-ll :: Inner -> Mnd Term; ll = applyA (LL :: LL IdM Inner)
-
-data LL m t = LL; type instance Idiom (LL m) = Mnd
-type instance Unwrap (LL m) t = LL m t
-instance Wrapper (LL m) where wrap = id; unwrap = id
-
-type instance Dom (LL m) t = Med m t
-type instance Rng (LL m) t = Med m (TApp (LL m) t)
-type instance TApp (LL m) Inner = Term -- instance for each type in binding group
-
-instance (IdM ~ m) => Inner ::: DomainA (LL m) where
-  inhabits = AppABy $ \_ -> dcDispatch $
-    eachOrNT (oneF (RMNTo llLam) ||. llVar) $ NT $ imageInDTAU LL
---  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAU LL
-
-
-
-
-
-env0 = [TBool, TBool, TArrow TInt TInt, TInt]
-ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0
-ex1 = ex0 `I.App` I.Var 3
-ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`
-      (I.Lam (TArrow TInt TInt) $ I.Var 0)
-
--- *LL> lambdaLift ex1 env0
--- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),
---       ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))
---      ] (App (App (DVar 0) (Var 2)) (Var 3))
diff --git a/Examples/LL0.hs b/Examples/LL0.hs
deleted file mode 100644
--- a/Examples/LL0.hs
+++ /dev/null
@@ -1,57 +0,0 @@
-
-
-
-
-
-module Examples.LL0 where
-
-import qualified Examples.InnerBase as I
-
-import qualified Data.Set as Set
-import qualified Data.IntMap as IM
-
-import Examples.LLBasics
-
-
-
-
-
-
-
-
-
-
-lambdaLift :: Inner -> [Type] -> Prog
-lambdaLift x e = Prog (reverse tlds) main where
-  (main, tlds) = runMnd (ll x) (e, IM.empty, 0)
-
-ll (I.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where
-  updE (rho, rn) = (ty : rho, support `prepend` rn) where
-    support =
-      IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm
-ll (I.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i
-
----------------------------------------- default
-ll (I.App tm1 tm2) = App <$> ll tm1 <*> ll tm2
- 
-
-
-
-
-
-
-
-
-
-
-
-env0 = [TBool, TBool, TArrow TInt TInt, TInt]
-ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0
-ex1 = ex0 `I.App` I.Var 3
-ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`
-      (I.Lam (TArrow TInt TInt) $ I.Var 0)
-
--- *LL> lambdaLift ex1 env0
--- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),
---       ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))
---      ] (App (App (DVar 0) (Var 2)) (Var 3))
diff --git a/Examples/LLBase.hs b/Examples/LLBase.hs
deleted file mode 100644
--- a/Examples/LLBase.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-module Examples.LLBase where
-
-import Examples.TermBase (Type(..))
-
-
-
-data Term = DVar Int | Var Int | App Term Term
-  deriving Show
-
-type TLD = ([Type], Type, Term)
-
-data Prog = Prog [TLD] Term
-  deriving Show
diff --git a/Examples/LLBasics.hs b/Examples/LLBasics.hs
deleted file mode 100644
--- a/Examples/LLBasics.hs
+++ /dev/null
@@ -1,71 +0,0 @@
-{-# LANGUAGE FlexibleInstances, TypeOperators, MultiParamTypeClasses,
-  TypeFamilies, UndecidableInstances #-}
-
-module Examples.LLBasics
-  (module Examples.LLBasics, module Examples.TermBase,
-   module Examples.InnerBase, module Examples.LLBase,
-   local, asks, (<$>), (<*>)) where
-
-import Examples.TermBase (Type(..))
-import Examples.InnerBase (Inner)
-import qualified Examples.InnerBase as I
-import Examples.LLBase
-
-import qualified Control.Arrow as Arrow
-import qualified Data.Set as Set; import Data.Set (Set)
-import qualified Data.IntMap as IM; import Data.IntMap (IntMap)
-import Data.Maybe (fromMaybe)
-
-import Control.Monad.Reader.Class (MonadReader(..), asks)
-import Control.Monad (ap)
-import Control.Applicative (Applicative(pure, (<*>)), (<$>))
-
-
-
-type Frees = Set Int; type Rename = IntMap Int
-
-bump :: Frees -> Frees
-bump = Set.map (subtract 1) . Set.filter (> 0)
-
-lookupRN :: Rename -> Int -> Int
-lookupRN rn i = fromMaybe i $ IM.lookup i rn
-
-prepend :: Rename -> Rename -> Rename
-prepend f = IM.unionWith const f .
-            IM.fromDistinctAscList . map ((+ 1) Arrow.*** (+ 1)) . IM.toAscList
-
-
-
-fvs :: Inner -> Frees
-fvs (I.Lam ty tm) = Set.map (subtract 1) $ Set.filter (> 0) $ fvs tm
-fvs (I.Var i) = Set.singleton i
-fvs (I.App tm1 tm2) = fvs tm1 `Set.union` fvs tm2
-
-
-
-newtype Mnd a = Mnd {runMnd :: ([Type], Rename, Int) -> (a, [TLD])}
-instance Functor Mnd where fmap f = (>>= return . f)
-instance Applicative Mnd where pure = return; (<*>) = ap
-instance Monad Mnd where
-  return a = Mnd $ \_ -> (a, [])
-  m >>= k = Mnd $ \e@(tys, rn, sh) -> case runMnd m e of
-    ~(a, w) -> Arrow.second (w ++) $ runMnd (k a) (tys, rn, sh + length w)
-instance (e ~ ([Type], Rename)) => MonadReader e Mnd where
-  ask = Mnd $ \ ~(x, y, _) -> ((x, y), []);
-  local f (Mnd g) =
-    Mnd $ \ ~(x, y, z) -> case f (x, y) of
-      ~(x', y') -> g (x', y', z)
-
-numEmissions :: Mnd Int
-numEmissions = Mnd $ \ ~(_, _, z) -> (z, [])
-
-emit :: [TLD] -> Mnd ()
-emit w = Mnd $ \_ -> ((), w)
-
-newTLD :: Type -> Frees -> Mnd Term -> Mnd Term
--- NB could check if such a TLD already exists
-newTLD ty fvs m = do
-  (rho, rn) <- ask; sh <- numEmissions
-  let fvs' = reverse $ Set.toAscList $ bump fvs
-  m >>= \tm -> emit [(map (rho !!) fvs', ty, tm)]
-  return $ foldl ((. Var . lookupRN rn) . App) (DVar sh) fvs'
diff --git a/Examples/LLDirect.hs b/Examples/LLDirect.hs
deleted file mode 100644
--- a/Examples/LLDirect.hs
+++ /dev/null
@@ -1,81 +0,0 @@
-{- |
-
-Module      :  Examples.LLDirect
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Lambda-lifts 'Examples.InnerBase.Inner' to 'Examples.LLBase.LL' without using
-@yoko@. Compare to "Examples.LL0" and "Examples.LL".
-
--}
-module Examples.LLDirect where
-
-import Examples.TermBase (Type(..))
-import Examples.InnerBase (Inner)
-import qualified Examples.InnerBase as I
-import Examples.LLBase
-
-import qualified Data.Set as Set; import Data.Set (Set)
-import qualified Data.IntMap as IM; import Data.IntMap (IntMap)
-
-
-
-fvs :: Inner -> Set Int
-fvs (I.Lam ty tm) = Set.map (subtract 1) $ Set.filter (> 0) $ fvs tm
-fvs (I.Var i) = Set.singleton i
-fvs (I.App tm1 tm2) = fvs tm1 `Set.union` fvs tm2
-
-bump :: Set Int -> Set Int
-bump = Set.map (subtract 1) . Set.filter (> 0)
-
-renm :: IntMap Int -> Int -> Term -> Term
-renm m dv tm@(Var i) = maybe tm Var $ IM.lookup i m
-renm m dv (App tm1 tm2) = App (renm m dv tm1) (renm m dv tm2)
-renm _ dv (DVar i) = DVar (i + dv)
-
-renmP :: IntMap Int -> Int -> Prog -> Prog
-renmP m dv (Prog tlds main) = Prog (map each tlds) (renm m dv main) where
-  each (tys, ty, tm) = (tys, ty, renm m dv tm)
-
-
-
-
-type Env = [Type]
-
-lambdaLift :: Inner -> Env -> Prog
-lambdaLift (I.Lam ty tm) rho = newTLD ty rho (fvs tm) $ lambdaLift tm (ty : rho)
-lambdaLift (I.Var i) rho = Prog [] $ Var i
-lambdaLift (I.App tm1 tm2) rho = Prog (tlds1 ++ tlds2) $ App main1 main2 where
-  Prog tlds1 main1 = lambdaLift tm1 rho
-  Prog tlds2 main2 = renmP IM.empty (length tlds1) $ lambdaLift tm2 rho
-
-
-
-newTLD :: Type -> Env -> Set Int -> Prog -> Prog
--- NB could check if such a TLD already exists; lambdaLift@I.App would need to handle
--- that too
-newTLD ty rho fvs (Prog tlds main) =
-  Prog ((map (rho !!) fvs', ty, renm rn 0 main) : tlds) $
-  foldl ((. Var) . App) (DVar 0) fvs'
-  where rn = IM.fromDistinctAscList $ zip (Set.toAscList fvs) [0..]
-        fvs' = reverse $ Set.toAscList $ bump fvs
-
-
-
-
-
-env0 = [TBool, TBool, TArrow TInt TInt, TInt]
-ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0
-ex1 = ex0 `I.App` I.Var 3
-ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`
-      (I.Lam (TArrow TInt TInt) $ I.Var 0)
-
-
--- *LL> ll ex1 env0
--- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),
---       ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))
---      ] (App (App (DVar 0) (Var 2)) (Var 3))
diff --git a/Examples/LLGeneric.hs b/Examples/LLGeneric.hs
deleted file mode 100644
--- a/Examples/LLGeneric.hs
+++ /dev/null
@@ -1,89 +0,0 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,
-  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,
-  TypeSynonymInstances, EmptyDataDecls #-}
-
-{-# OPTIONS_GHC -fcontext-stack=250 #-}
-
-{- |
-
-Module      :  Examples.LLGeneric
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-The declaration that hook 'Examples.LLBase.Term' into @yoko@. This will
-eventually be generated via Template Haskell.
-
--}
-module Examples.LLGeneric where
-
-import Examples.LLBase (Term)
-import qualified Examples.LLBase as B
-
-import Examples.ReflectAux
-
-data DVar; data Var; data App
-
-concat `fmap` mapM derive [''Term, ''DVar, ''Var, ''App]
-
-type instance Tag DVar = $(return $ encode "DVar")
-type instance Recurs DVar = V
-instance DC DVar where
-  occName _ = "DVar"
-  type Range DVar = Term
-  fr ~(DVar i) = B.DVar i
-data instance RM m (N DVar) = DVar Int
-type instance Tag Var = $(return $ encode "Var")
-type instance Recurs Var = V
-instance DC Var where
-  occName _ = "Var"
-  type Range Var = Term
-  fr ~(Var i) = B.Var i
-data instance RM m (N Var) = Var Int
-type instance Tag App = $(return $ encode "App")
-type instance Recurs App = N Term
-instance DC App where
-  occName _ = "App"
-  type Range App = Term
-  fr ~(App tm0 tm1) = B.App tm0 tm1
-data instance RM m (N App) = App (Med m Term) (Med m Term)
-instance DT Term where
-  packageName _ = "datatype-reflect"
-  moduleName _ = "TermBase"
-  type Siblings Term = N Term
-  data DCU Term dc where
-    DVar_ :: DCU Term DVar; Var_ :: DCU Term Var
-    App_ :: DCU Term App
-  disband (B.DVar i)      = disbanded $ DVar i
-  disband (B.Var i)       = disbanded $ Var i
-  disband (B.App tm0 tm1) = disbanded $ App tm0 tm1
-type instance Inhabitants (DCU Term) = (N DVar :+ N Var) :+ N App
-instance Finite (DCU Term) where
-  toUni DVar_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits
-instance Etinif (DCU Term) where
-  frUni (Uni x) = case x of
-    (OnLeft  (OnLeft  (Here Refl))) -> DVar_
-    (OnLeft  (OnRight (Here Refl))) -> Var_
-    (OnRight (Here Refl))  -> App_
-instance (t ::: Uni (DCs Term)) => t ::: DCU Term where
-  inhabits = frUni inhabits
-instance EqT (DCU Term) where eqT = eqTFin
-
-
-
-
-type instance Rep DVar = D Int
-instance Generic DVar where
-  rep ~(DVar i) = D i
-  obj ~(D i) = DVar i
-type instance Rep Var = D Int
-instance Generic Var where
-  rep ~(Var i) = D i
-  obj ~(D i) = Var i
-type instance Rep App = R Term :* R Term
-instance Generic App where
-  rep ~(App tm0 tm1) = FF (R tm0, R tm1)
-  obj ~(FF (R tm0, R tm1)) = App tm0 tm1
diff --git a/Examples/Main.hs b/Examples/Main.hs
deleted file mode 100644
--- a/Examples/Main.hs
+++ /dev/null
@@ -1,25 +0,0 @@
-{- |
-
-Module      :  Examples.Main
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Just bundles up the three examples.
-
--}
-module Main where
-
-import Examples.TermTest
-import Examples.TermInner
-import Examples.LL
-
-
-
-main = do
-  print $ Examples.TermTest.ex1
-  print $ Examples.TermInner.ex1
-  print $ lambdaLift Examples.LL.ex1 env0
diff --git a/Examples/ReflectAux.hs b/Examples/ReflectAux.hs
deleted file mode 100644
--- a/Examples/ReflectAux.hs
+++ /dev/null
@@ -1,19 +0,0 @@
-{- |
-
-Module      :  Examples.ReflectAux
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Just bundles up some imports for the various @*Generic@ modules.
-
--}
-module Examples.ReflectAux (encode, module Data.Yoko, DCU) where
-
-import Type.Serialize
-
-import Data.Yoko hiding (qK)
-import Data.Yoko.ReflectBase (DCU)
diff --git a/Examples/TermBase.hs b/Examples/TermBase.hs
deleted file mode 100644
--- a/Examples/TermBase.hs
+++ /dev/null
@@ -1,24 +0,0 @@
-{- |
-
-Module      :  Examples.TermBase
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
--}
-module Examples.TermBase where
-
-data Type = TBool | TInt | TArrow Type Type
-  deriving Show
-
-data Term = Lam Type Term
-          | Var Int
-          | App Term Term
-          | Let [Decl] Term
-  deriving Show
-
-data Decl = Decl Type Term
-  deriving Show
diff --git a/Examples/TermGeneric.hs b/Examples/TermGeneric.hs
deleted file mode 100644
--- a/Examples/TermGeneric.hs
+++ /dev/null
@@ -1,190 +0,0 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,
-  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,
-  TypeSynonymInstances, EmptyDataDecls #-}
-
-{-# OPTIONS_GHC -fcontext-stack=250 #-}
-
-{- |
-
-Module      :  Examples.TermGeneric
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-The declaration that hook 'Examples.TermBase.Type', 'Examples.TermBase.Term',
-and 'Examples.TermBase.Decl' into @yoko@. This will eventually be generated via
-Template Haskell.
-
--}
-module Examples.TermGeneric where
-
-import qualified Examples.TermBase as B
-
-import Examples.ReflectAux
-
-data TBool; data TInt; data TArrow
-data Lam; data Var; data App; data Let
-data Decl
-
-concat `fmap` mapM derive
-  [''B.Type, ''TBool, ''TInt, ''TArrow,
-   ''B.Term, ''Lam, ''Var, ''App, ''Let,
-   ''B.Decl, ''Decl]
-
-type instance Tag TBool = $(return $ encode "TBool")
-type instance Recurs TBool = U
-instance DC TBool where
-  occName _ = "TBool"
-  type Range TBool = B.Type
-  fr _ = B.TBool
-data instance RM m (N TBool) = TBool
-type instance Tag TInt = $(return $ encode "TInt")
-type instance Recurs TInt = U
-instance DC TInt where
-  occName _ = "TInt"
-  type Range TInt = B.Type
-  fr _ = B.TInt
-data instance RM m (N TInt) = TInt
-type instance Tag TArrow = $(return $ encode "TArrow")
-type instance Recurs TArrow = N B.Type
-instance DC TArrow where
-  occName _ = "TArrow"
-  type Range TArrow = B.Type
-  fr ~(TArrow d r) = B.TArrow d r
-data instance RM m (N TArrow) = TArrow (Med m B.Type) (Med m B.Type)
-instance DT B.Type where
-  packageName _ = "datatype-reflect"
-  moduleName _ = "TermBase"
-  type Siblings B.Type = N B.Type
-  data DCU B.Type dc where
-    TBool_ :: DCU B.Type TBool; TInt_ :: DCU B.Type TInt
-    TArrow_ :: DCU B.Type TArrow
-  disband B.TBool        = disbanded TBool
-  disband B.TInt         = disbanded TInt
-  disband (B.TArrow d r) = disbanded $ TArrow d r
-type instance Inhabitants (DCU B.Type) = N TBool :+ N TInt :+ N TArrow
-instance Finite (DCU B.Type) where
-  toUni TBool_ = inhabits; toUni TInt_ = inhabits; toUni TArrow_ = inhabits
-instance Etinif (DCU B.Type) where
-  frUni (Uni x) = case x of
-    (OnLeft          (Here Refl)) -> TBool_
-    (OnRight (OnLeft  (Here Refl))) -> TInt_
-    (OnRight (OnRight (Here Refl))) -> TArrow_
-instance (t ::: Uni (DCs B.Type)) => t ::: DCU B.Type where
-  inhabits = frUni inhabits
-instance EqT (DCU B.Type) where eqT = eqTFin
-
-type instance Tag Lam = $(return $ encode "Lam")
-type instance Recurs Lam = N B.Term
-instance DC Lam where
-  occName _ = "Lam"
-  type Range Lam = B.Term
-  fr ~(Lam ty tm) = B.Lam ty tm
-data instance RM m (N Lam) = Lam B.Type (Med m B.Term)
-type instance Tag Var = $(return $ encode "Var")
-type instance Recurs Var = U
-instance DC Var where
-  occName _ = "Var"
-  type Range Var = B.Term
-  fr ~(Var i) = B.Var i
-data instance RM m (N Var) = Var Int
-type instance Tag App = $(return $ encode "App")
-type instance Recurs App = N B.Term
-instance DC App where
-  occName _ = "App"
-  type Range App = B.Term
-  fr ~(App tm0 tm1) = B.App tm0 tm1
-data instance RM m (N App) = App (Med m B.Term) (Med m B.Term)
-type instance Tag Let = $(return $ encode "Let")
-type instance Recurs Let = N B.Decl :+ N B.Term
-instance DC Let where
-  occName _ = "Let"
-  type Range Let = B.Term
-  fr ~(Let ds tm) = B.Let ds tm
-data instance RM m (N Let) = Let [Med m B.Decl] (Med m B.Term)
-instance DT B.Term where
-  packageName _ = "datatype-reflect"
-  moduleName _ = "TermBase"
-  type Siblings B.Term = N B.Term :+ N B.Decl
-  data DCU B.Term dc where
-    Lam_ :: DCU B.Term Lam; Var_ :: DCU B.Term Var
-    App_ :: DCU B.Term App; Let_ :: DCU B.Term Let
-  disband (B.Lam ty tm)   = disbanded $ Lam ty tm
-  disband (B.Var i)       = disbanded $ Var i
-  disband (B.App tm0 tm1) = disbanded $ App tm0 tm1
-  disband (B.Let ds tm)   = disbanded $ Let ds tm
-type instance Inhabitants (DCU B.Term) = (N Lam :+ N Var) :+ (N App :+ N Let)
-instance Finite (DCU B.Term) where
-  toUni Lam_ = inhabits; toUni Var_ = inhabits
-  toUni App_ = inhabits; toUni Let_ = inhabits
-instance Etinif (DCU B.Term) where
-  frUni (Uni x) = case x of
-    (OnLeft  (OnLeft (Here Refl))) -> Lam_
-    (OnLeft  (OnRight (Here Refl))) -> Var_
-    (OnRight (OnLeft (Here Refl))) -> App_
-    (OnRight (OnRight (Here Refl))) -> Let_
-instance (t ::: Uni (DCs B.Term)) => t ::: DCU B.Term where
-  inhabits = frUni inhabits
-instance EqT (DCU B.Term) where eqT = eqTFin
-
-type instance Tag Decl = $(return $ encode "Decl")
-type instance Recurs Decl = N B.Term
-instance DC Decl where
-  occName _ = "Decl"
-  type Range Decl = B.Decl
-  to = Just . uniqueDC; fr ~(Decl ds tm) = B.Decl ds tm
-data instance RM m (N Decl) = Decl B.Type (Med m B.Term)
-instance DT B.Decl where
-  packageName _ = "datatype-reflect"
-  moduleName _ = "DeclBase"
-  type Siblings B.Decl = N B.Term :+ N B.Decl
-  data DCU B.Decl dc where Decl_ :: DCU B.Decl Decl
-  disband ~(B.Decl ty tm) = disbanded $ Decl ty tm
-type instance Inhabitants (DCU B.Decl) = N Decl
-instance Finite (DCU B.Decl) where
-  toUni Decl_ = inhabits
-instance Etinif (DCU B.Decl) where
-  frUni (Uni (Here Refl)) = Decl_
-instance (t ::: Uni (DCs B.Decl)) => t ::: DCU B.Decl where
-  inhabits = frUni inhabits
-instance EqT (DCU B.Decl) where eqT = eqTFin
-
-
-
-type instance Rep TBool = V
-instance Generic TBool where
-  rep _ = void "rep[TBool]"
-  obj _ = TBool
-type instance Rep TInt = V
-instance Generic TInt where
-  rep _ = void "rep[TInt]"
-  obj _ = TInt
-type instance Rep TArrow = R B.Type :* R B.Type
-instance Generic TArrow where
-  rep ~(TArrow ty0 ty1) = FF (R ty0, R ty1)
-  obj ~(FF (R ty0, R ty1)) = TArrow ty0 ty1
-
-type instance Rep Var = D Int
-instance Generic Var where
-  rep ~(Var i) = D i
-  obj ~(D i) = Var i
-type instance Rep Lam = D B.Type :* R B.Term
-instance Generic Lam where
-  rep ~(Lam ty tm) = FF (D ty, R tm)
-  obj ~(FF (D ty, R tm)) = Lam ty tm
-type instance Rep App = R B.Term :* R B.Term
-instance Generic App where
-  rep ~(App tm0 tm1) = FF (R tm0, R tm1)
-  obj ~(FF (R tm0, R tm1)) = App tm0 tm1
-type instance Rep Let = F [] (R B.Decl) :* R B.Term
-instance Generic Let where
-  rep ~(Let ds tm) = FF (F (map R ds), R tm)
-  obj ~(FF (F rds, R tm)) = Let (map unR rds) tm
-
-type instance Rep Decl = D B.Type :* R B.Term
-instance Generic Decl where
-  rep ~(Decl ty tm) = FF (D ty, R tm)
-  obj ~(FF (D ty, R tm)) = Decl ty tm
diff --git a/Examples/TermInner.hs b/Examples/TermInner.hs
deleted file mode 100644
--- a/Examples/TermInner.hs
+++ /dev/null
@@ -1,60 +0,0 @@
-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances #-}
-
-{-# OPTIONS_GHC -fcontext-stack=200 #-}
-
-{- |
-
-Module      :  Examples.TermInner
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-A let-elaboration via "Data.Yoko.InDT".
-
--}
-module Examples.TermInner where
-
-import Examples.TermBase
-import Examples.InnerBase (Inner)
-import qualified Examples.InnerBase as I
-import qualified Examples.TermGeneric as G
-import Examples.InnerGeneric ()
-
-import Type.Yoko
-
-import Data.Yoko.InDT
-import Data.Yoko.Reflect
-
-
-
-
-
-elaborate :: Term -> Inner; elaborate = apply (Elab :: Elab IdM Term)
-
-data Elab m t = Elab
-type instance Unwrap (Elab m) t = Elab m t
-instance Wrapper (Elab m) where wrap = id; unwrap = id
-
-type instance Dom (Elab m) t = Med m t
-type instance Rng (Elab m) t = Med m (TApp (Elab m) t)
-
-type instance TApp (Elab m) Term = Inner
-
-instance (IdM ~ m) => Term ::: Domain (Elab m) where
-  inhabits = AppBy $ \_ -> dcDispatch $
-    eachOrNT (oneF $ RMNTo elab_Let) $ NT $ imageInDTU Elab
-
-elab_Let (G.Let ds tm) =
-  foldr (\(Decl ty tm) x -> I.Lam ty x `I.App` elaborate tm) (elaborate tm) ds
-
-
-
-
-
-ex0 = Let [Decl TInt (Var 111), Decl TBool (Var 222)] (Var 0)
-
-ex1 = elaborate ex0
diff --git a/Examples/TermTest.hs b/Examples/TermTest.hs
deleted file mode 100644
--- a/Examples/TermTest.hs
+++ /dev/null
@@ -1,93 +0,0 @@
-{-# LANGUAGE QuasiQuotes, TypeFamilies, FlexibleInstances,
-  MultiParamTypeClasses, GADTs, PatternGuards #-}
-
-{-# OPTIONS_GHC -fcontext-stack=200 #-}
-
-{- |
-
-Module      :  Examples.TermTest
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-A denotational semantics for the simple-typed lambda calculus via
-"Data.Yoko.Cata".
-
--}
-module Examples.TermTest where
-
-import Examples.TermBase
-import qualified Examples.TermGeneric as G
-
-import Type.Yoko
-import Data.Yoko.Cata
-import Data.Yoko
-
-
--- | Since our family of abstract data types don't correspond to the
--- object-language types, we need a tagged universal value space.
-data Val = VBool Bool | VInt Int | VFun (Val -> Val)
-instance Show Val where
-  show (VBool b) = show b; show (VInt i) = show i; show (VFun _) = "<fun>"
-
-
-
-eLam (G.Lam _ t) e = VFun $ t . (: e)
-eVar (G.Var i) = (!! i)
-eApp (G.App t1 t2) e
-  | VFun f <- t1 e = f (t2 e)
-  | otherwise = error "failed projection in reduce[App]"
-eLet (G.Let ds t) = foldr cons t ds where cons (_, s) t e = t (s e : e)
-
-eDecl (G.Decl ty t) = (ty, t)
-
-
--- | The semantic domain of the reduction.
-type Sem = [Val] -> Val
-
--- | The recursion mediator for our denotation.
-data SemM = SemM
-type instance Med SemM Term = Sem
-type instance Med SemM Decl = (Type, Sem)
-
-instance AlgebraDT SemM Term where algebraDT = algebraFin
-instance AlgebraDC SemM G.Lam where algebraDC = eLam
-instance AlgebraDC SemM G.Var where algebraDC = eVar
-instance AlgebraDC SemM G.App where algebraDC = eApp
-instance AlgebraDC SemM G.Let where algebraDC = eLet
-
-instance AlgebraDT SemM Decl where algebraDT = eDecl . uniqueRMN
-
--- | 'eval' will work for any family of mutually recursive types that all have
--- @'AlgebraDT' SemM@ instances.
-eval x = ($ x) $ cata $ algebras [qP|SemM|]
-
-eval'     x = ($ x) $ cata $ (algebraDT  .|. algebraDT :: SiblingAlgs Term SemM)
-eval''    x = ($ x) $ cata $ (algebraDT  .|. algebraDT)
-eval'''   x = ($ x) $ cata $ (algebraFin .|. algebraDT :: SiblingAlgs Term SemM)
-eval''''  x = ($ x) $ cata $ (algebraFin .|. algebraDT)
-eval''''' x = ($ x) $ cata $ (algebraDT  .|. (eDecl . uniqueRMN'))
-
---instance AlgebraDT SemM Decl where algebraDT = algebraFin
---instance AlgebraDC SemM G.Decl where algebraDC = eDecl
---eval''''' x = ($ x) $ cata $ (algebraFin .|. algebraFin :: SiblingAlgs Term SemM)
-
-
-
-
-
-vSucc = VFun $ \(VInt i) -> VInt $ i + 1
-
-
-ex0 = eval (Var 0) [VBool True]
-ex1 = eval (Let [Decl (TInt `TArrow` TInt) $ Lam TInt (Var 0) `App` Var 0 `App` Var 1]
-                (Var 0)) [vSucc, VInt 9]
-ex2' = eval (Decl TInt (Var 0))
-ex2 = snd ex2' [VInt 3]
-
-
---ex1' = eval' (Let [Decl (TInt `TArrow` TInt) (Var 0 `App` Var 1)]
---                (Var 0)) [vSucc, VInt 9]
diff --git a/Examples/Test.hs b/Examples/Test.hs
new file mode 100644
--- /dev/null
+++ b/Examples/Test.hs
@@ -0,0 +1,21 @@
+{-# LANGUAGE TypeFamilies, TemplateHaskell #-}
+
+{-# OPTIONS_GHC -ddump-splices #-}
+
+module Test where
+
+import Data.Yoko
+import Type.Ord.SpineSerialize (Compare)
+
+
+data T a = T a
+
+data X = X
+
+
+concat `fmap` mapM derive [''T, ''X]
+
+
+
+test :: (() ~ Compare a b) => a -> b -> ()
+test _ _ = ()
diff --git a/README b/README
--- a/README
+++ b/README
@@ -1,1 +1,1 @@
-See the documentation at http://code.google.com/p/yoko
+Read the paper at http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf
diff --git a/Type/Yoko.hs b/Type/Yoko.hs
deleted file mode 100644
--- a/Type/Yoko.hs
+++ /dev/null
@@ -1,36 +0,0 @@
-{- |
-
-Module      :  Type.Yoko
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
--}
-
-module Type.Yoko (
-  module Type.Yoko.Type,
-  module Type.Yoko.Universe,
-  module Type.Yoko.Natural,
-  module Type.Yoko.BTree,
-  module Type.Yoko.Sum,
-  module Type.Yoko.TSTSS,
-  module Type.Yoko.Fun,
-  module Type.Yoko.FunA,
-  module Type.Yoko.MFun,
-  module Type.Yoko.TFunA
-  ) where
-
-import Type.Yoko.Type
-import Type.Yoko.Universe
-import Type.Yoko.Natural
-import Type.Yoko.BTree
-import Type.Yoko.Sum
-import Type.Yoko.TSTSS
-
-import Type.Yoko.Fun
-import Type.Yoko.FunA
-import Type.Yoko.MFun
-import Type.Yoko.TFunA
diff --git a/Type/Yoko/BTree.hs b/Type/Yoko/BTree.hs
deleted file mode 100644
--- a/Type/Yoko/BTree.hs
+++ /dev/null
@@ -1,194 +0,0 @@
-{-# LANGUAGE TypeFamilies, ScopedTypeVariables, QuasiQuotes, Rank2Types,
-  GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
-  UndecidableInstances, EmptyDataDecls, TypeOperators #-}
-
-{-# LANGUAGE TemplateHaskell #-}
-
-{- |
-
-Module      :  Type.Yoko.BTree
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Operators for the type-sums from "Type.Yoko.Sum".
-
--}
-
-module Type.Yoko.BTree where
-
-import Type.Yoko.Type
-import Type.Yoko.Universe
-import Type.Yoko.Natural
-import Data.Yoko.Core
-import Type.Yoko.Sum
-
-
-
-
-
--- | @Inu t@ is a universe of type-sums containing @t@.
-type Inu t = Exists ((:=:) t)
-
--- | @Uni ts@ is a universe containing the types in the type-sum @ts@.
-newtype Uni ts t = Uni (Inu t ts)
-
-instance (ts ::: Inu t) => t ::: Uni ts where inhabits = Uni inhabits
-
-type instance Pred (Uni ts) t = Elem t ts
-
-instance EqT (Uni ts) where
-  eqT (Uni u) (Uni v) = w u v where
-    w :: forall ts a b. Inu a ts -> Inu b ts -> Maybe (a :=: b)
-    w (Here Refl) (Here Refl) = Just Refl
-    w (OnLeft u) (OnLeft v) = w u v
-    w (OnRight u) (OnRight v) = w u v
-    w _ _ = Nothing 
-
-
-
-
-
--- | A @Uni ts t@ value can also be understood in terms of more primitive
--- universes, 'VoidU', @':=:'@ and @':||'@ for 'V', 'N', and @':+'@,
--- respectively.
-type family PrimUni ts :: * -> *
-type instance PrimUni V = VoidU
-type instance PrimUni (N t) = (:=:) t
-type instance PrimUni (ts :+ us) = PrimUni ts :|| PrimUni us
-
-primUni :: Uni ts t -> PrimUni ts t
-primUni (Uni u) = w u where
-  w :: Inu t ts -> PrimUni ts t
-  w (Here Refl) = Refl
-  w (OnLeft u) = LeftU $ w u
-  w (OnRight v) = RightU $ w v
-
-primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t
-primUni1 (Uni (OnLeft u)) = LeftU $ Uni u
-primUni1 (Uni (OnRight v)) = RightU $ Uni v
-
-
-
-
--- | Finite universes can be represented as type-sums.
-type family Inhabitants u
-class Finite u where
-  toUni :: u t -> Uni (Inhabitants u) t
-
-finiteNP :: Finite u => NP u f -> NP (Uni (Inhabitants u)) f
-finiteNP = firstNP toUni
-
--- | @frUni@ sometimes requires a stronger context than does @toUni@, so we
--- separate the two methods.
-class Finite u => Etinif u where frUni :: Uni (Inhabitants u) t -> u t
-
--- | Any finite universe can be used to determine type equality.
-eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v
-          ) => u a -> v b -> Maybe (a :=: b)
-eqTFin x y = eqT (toUni x) (toUni y)
-
-type instance Inhabitants (Uni ts) = ts
-instance Finite (Uni ts) where toUni = id
-instance Finite (Uni ts) => Etinif (Uni ts) where frUni = id
-
-type instance Inhabitants VoidU = V
-
-type instance Inhabitants ((:=:) t) = N t
-instance Finite ((:=:) t) where toUni Refl = Uni (Here Refl)
-instance Etinif ((:=:) t) where frUni (Uni (Here Refl)) = Refl
-
-type instance Inhabitants (u :|| v) = Inhabitants u :+ Inhabitants v
-instance (Finite u, Finite v) => Finite (u :|| v) where
-  toUni (LeftU u) = case toUni u of
-    Uni x -> Uni $ OnLeft $ x
-  toUni (RightU v) = case toUni v of
-    Uni x -> Uni $ OnRight $ x
-instance (Etinif u, Etinif v) => Etinif (u :|| v) where
-  frUni uv = case primUni1 uv of
-    LeftU u -> LeftU $ frUni u
-    RightU v -> RightU $ frUni v
-
-
--- | @Norm@ uses @NormW@ to remove duplicates from (i.e. /normalize/) a
--- type-sum.
-type family Norm c
-type instance Norm V = V
-type instance Norm (N t) = N t
-type instance Norm (ts :+ us) = NormW (ts :+ us) V
-
--- | @NormW@ combines two type-sums into a right-associated type-sum containing
--- no duplicates.
-type family NormW c acc
-type instance NormW V acc = acc
-type instance NormW (N t) acc = If (Elem t acc) acc (N t :+ acc)
-type instance NormW (ts :+ us) acc = NormW ts (NormW us acc)
-
-
-
-
--- | @Each ts f@ provides a @'NT' t f@ for each @t@ in the type-sum @ts@.
-type Each ts = NT (Uni ts)
-
-none :: String -> Each V f
-none s = NT $ error $ "TypeBTree.none: " ++ s
-
-one_ :: [qP|f :: *->*|] -> Unwrap f t -> Each (N t) f
-one_ p x = firstNT primUni $ constNT_ p x
-
-one :: Unwrap f t -> Each (N t) f
-one = one_ Proxy
-
-oneF :: Wrapper f => f t -> Each (N t) f
-oneF x = firstNT primUni $ constNTF x
-
-infixr 6 |||, .|.
-both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) f
-both f g = firstNT primUni1 $ orNT f g; (|||) = both
-
-infixl 5 ||.; infixr 5 .||
-(.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) f
-(||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) f
-(.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) f
-f .|. g = one f ||| one g; f ||. g = f ||| one g; f .|| g = one f ||| g
-
-
-
--- | @each@ is the principal means of defining an @Each@ value.
-each :: forall u v f. (Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->
-        (forall a. u a -> Unwrap f a) -> NT v f
-each _ = \fs -> firstNT toUni $ w inhabits fs where
-  w :: forall ts. All u ts ->
-       (forall a. (a ::: u) => u a -> Unwrap f a) -> Each ts f
-  w SumV _ = none "TypeBTree.each"
-  w (SumN u) fns = one $ fns u
-  w (SumS c d) fns = w c fns `both` w d fns
-  
-eachF :: forall u v f. (Wrapper f, Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->
-         (forall a. u a -> f a) -> NT v f
-eachF p f = each p (unwrap . f)
-
-eachF_ :: forall f v. (Wrapper f, Inhabitants v ::: All NoneU, Finite v) => (forall a. f a) -> NT v f
-eachF_ f = eachF Proxy ((\NoneU -> f) :: forall a. NoneU a -> f a)
-
-
-
--- | Just a specialization: @prjEach x f = 'appNT' f x@.
-prjEach :: Uni ts t -> Each ts f -> Unwrap f t
-prjEach x f = appNT f x
-
-prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f t
-prjEachF = (wrap .) . prjEach
-
-
-
-
--- | @eachOrNT fs gs@ builds an 'NT' that uses @fs@ for as many types in the
--- universe @v@ as possible, and uses @gs@ for the rest. It's an extension of
--- 'orNT' to @Each@.
-eachOrNT :: forall u v f w.
-  (Inhabitants v ::: All (u :|| w), Finite v) => NT u f -> NT w f -> NT v f
-eachOrNT fs dflt = firstNT toUni $ each Proxy $ appNT $ orNT fs dflt
diff --git a/Type/Yoko/Fun.hs b/Type/Yoko/Fun.hs
deleted file mode 100644
--- a/Type/Yoko/Fun.hs
+++ /dev/null
@@ -1,136 +0,0 @@
-{-# LANGUAGE TypeFamilies, FlexibleContexts, Rank2Types, QuasiQuotes,
-  TypeOperators, ScopedTypeVariables, GADTs, FlexibleInstances,
-  MultiParamTypeClasses, UndecidableInstances #-}
-
-{- |
-
-Module      :  Type.Yoko.Fun
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-An explicit perspective on (both parametric and ad-hoc) polymorphic
-functions. The datatype representing such a function must be of kind @* -> *@;
-the parameter is the type at which the function is to be instantiated.
-
--}
-
-module Type.Yoko.Fun
-  (Domain(..), Dom, Rng, applyU, apply,
-   YieldsArrowTSSU, DomF, RngF, eachArrow,
-   AsComp(..), WrapComp, WrapCompF
-  ) where
-
-import Type.Yoko.Type
-import Type.Yoko.Universe
-import Type.Yoko.Natural
-import Type.Yoko.Sum
-import Type.Yoko.BTree
-
-
-
-
--- | @Domain fn@ is the universe of types at which @fn@ can be applied; it's
--- the type-level domain of @fn@.
-newtype Domain fn t = AppBy (fn t -> Dom fn t -> Rng fn t)
-
--- | @Dom fn t@ is the domain of @fn@ at type @t@; it's the term-level domain
--- of @fn@ at @t@.
-type family Dom (fn :: * -> *) t
--- | @Rng fn t@ is the range of @fn@ at type @t@; it's the term-level range of
--- @fn@ at @t@.
-type family Rng (fn :: * -> *) t
-
--- | @applyD@ is analogous to '$'.
-applyU :: Domain fn t -> fn t -> Dom fn t -> Rng fn t
-applyU (AppBy f) = f
-
--- | @apply = applyU inhabits@.
-apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t
-apply = applyU inhabits
-
-
-
--- | @YieldsArrowTSSU fn@ also gaurantees that @fn@ at @t@ yields a type of the
--- shape @(DomF fn) t -> (RngF fn) t@; i.e. it guarantees that @Dom fn t@ and
--- @Rng fn t@ both don't depend on @t@ and also are an application of a @* ->
--- *@ to @t@.
-data YieldsArrowTSSU fn t where
-  YieldsArrowTSSU ::
-    (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
-    ) => Domain fn t -> YieldsArrowTSSU fn t
-instance (t ::: Domain fn, Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
-         ) => t ::: YieldsArrowTSSU fn where inhabits = YieldsArrowTSSU inhabits
-
--- | Used by @YieldsArrowTSSU fn@ to structure the domain of @fn@.
-type family DomF (fn :: * -> *) :: * -> *
--- | Used by @YieldsArrowTSSU fn@ to structure the range of @fn@.
-type family RngF (fn :: * -> *) :: * -> *
-
--- | Just a specialization: @yieldsArrowTSSU (YieldsArrowTSSU domD) fn = applyU domU fn@.
-yieldsArrowTSSU :: YieldsArrowTSSU fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t
-yieldsArrowTSSU (YieldsArrowTSSU domU) fn = applyU domU fn
-
--- | Defines an @'NT' u@ from a suitably polymorphic type-function @fn@ if @u@
--- is finite and the function yields an arrow at each type in @u@.
-eachArrow :: forall fn u.
-  (Finite u, Inhabitants u ::: All (YieldsArrowTSSU fn)
-  ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))
-eachArrow fn = each [qP|YieldsArrowTSSU fn :: *->*|] $
-  \d -> yieldsArrowTSSU d fn
-
-
-
-
-
-type instance Dom (fn :. f) a = Dom fn (f a)
-type instance Rng (fn :. f) a = Rng fn (f a)
-type instance DomF (fn :. f) = DomF fn
-type instance RngF (fn :. f) = RngF fn
-instance (f t ::: Domain fn) => t ::: Domain (fn :. f) where
-  inhabits = AppBy $ \(Compose fn) -> apply fn
-
-
-
-
-
--- | Only instance: @type instance WrapComp_ (f (g a)) = (f :. g) a@.
-type WrapComp a = WrapComp_ a
-type family WrapComp_ a
-type instance WrapComp_ (f (g a)) = (f :. g) a
-
--- | Only instance: @type instance WrapCompF_ (f (g a)) = f :. g@.
-type WrapCompF a = WrapCompF_ a
-type family WrapCompF_ a :: * -> *
-type instance WrapCompF_ (f (g a)) = f :. g
-
-
-
-
-
-{- | Defining instances:
-
-@
-  type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
-  type instance Rng (AsComp fn) t = WrapComp (Rng fn t)
-  inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap
-@
-
--}
-newtype AsComp (fn :: * -> *) t = AsComp (fn t)
-
-type instance Unwrap (AsComp fn) t = fn t
-instance Wrapper (AsComp fn) where wrap = AsComp; unwrap (AsComp x) = x
-
-type instance Dom (AsComp fn) t = WrapComp (Dom fn t)
-type instance Rng (AsComp fn) t = WrapComp (Rng fn t)
-
-type instance DomF (AsComp fn) = WrapCompF (Dom fn ())
-type instance RngF (AsComp fn) = WrapCompF (Rng fn ())
-
-instance (t ::: Domain fn, Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5)
-         ) => t ::: Domain (AsComp fn) where
-  inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap
diff --git a/Type/Yoko/FunA.hs b/Type/Yoko/FunA.hs
deleted file mode 100644
--- a/Type/Yoko/FunA.hs
+++ /dev/null
@@ -1,36 +0,0 @@
-{-# LANGUAGE TypeFamilies, FlexibleContexts #-}
-
-{- |
-
-Module      :  Type.Yoko.FunA
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-"Type.Yoko.Fun" functions that /implicitly/ return an applicative functor. The
-implicitness means that the 'Rng' type instance is not expected to include the
-applicative functor.
-
--}
-
-module Type.Yoko.FunA
-  (Idiom, DomainA(..), applyA, applyAU) where
-
-import Type.Yoko.Fun
-import Type.Yoko.Universe
-
-
-
-
-
-type family Idiom (fn :: * -> *) :: * -> *
-newtype DomainA fn t = AppABy (fn t -> Dom fn t -> Idiom fn (Rng fn t))
-
-applyA :: (t ::: DomainA fn) => fn t -> Dom fn t -> Idiom fn (Rng fn t)
-applyA = applyAU inhabits
-
-applyAU :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)
-applyAU (AppABy f) = f
diff --git a/Type/Yoko/MFun.hs b/Type/Yoko/MFun.hs
deleted file mode 100644
--- a/Type/Yoko/MFun.hs
+++ /dev/null
@@ -1,97 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,
-  ScopedTypeVariables, UndecidableInstances, QuasiQuotes, TypeFamilies,
-  GADTs, TypeOperators, Rank2Types #-}
-
-{- |
-
-Module      :  Type.Yoko.MFun
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-An enrichment of "Type.Yoko.Fun" where functions must be of kind @* -> * -> *@;
-the first parameter is a mediator and the second is (as expected by
-"Type.Yoko.Fun") the type at which the function is to be instantiated.
-
--}
-
-module Type.Yoko.MFun where
-
-import Type.Yoko.TSTSS
-
-import Type.Yoko.Type
-import Type.Yoko.Universe
-import Type.Yoko.Natural
-
-import Type.Yoko.Fun
-
-import Data.Yoko.Generic
-
-
-
-
--- | mediator-functions can be mapped across an 'RM' type/value.
-newtype RMMap u fn m c = RMMap (NT u (fn m))
-
-{- | mediator-functions can also modify the mediator; e.g.
-
-@
-  type instance 'Dom' (RMMap u fn m) c = RM m c
-  type instance 'Rng' (RMMap u fn m) c = RM (MApp fn m) c
-@
-
--}
-type family MApp (fn :: * -> * -> *) m
-
-type instance Dom (RMMap u fn m) c = RM m c
-type instance Rng (RMMap u fn m) c = RM (MApp fn m) c
-
-type instance MApp (RMMap u fn) m = MApp fn m
-
-instance (t ::: u, t ::: Domain (fn m), Wrapper (fn m),
-          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med (MApp fn m) t
-         ) => R t ::: Domain (RMMap u fn m) where
-  inhabits = AppBy $ \(RMMap fns) ->
-             R . apply (fns `appNTF` inhabitsFor [qP|t|]) . unR
-
-instance (Rep t ::: Domain (RMMap u fn m), Generic t
-         ) => N t ::: Domain (RMMap u fn m) where
-  inhabits = AppBy $ \(RMMap fn) -> obj . apply (RMMap fn) . rep
-
-instance D a ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ -> D . unD
-instance U ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ _ -> U
-instance (Functor f, c ::: Domain (RMMap u fn m)
-         ) => F f c ::: Domain (RMMap u fn m) where
-  inhabits = AppBy $ \(RMMap fn) -> F . fmap (apply (RMMap fn)) . unF
-instance (c ::: Domain (RMMap u fn m), d ::: Domain (RMMap u fn m),
-          FunctorTSTSS ff) => FF ff c d ::: Domain (RMMap u fn m) where
-  inhabits = AppBy $ \(RMMap fn) -> FF .
-             fmapTSTSS (apply (RMMap fn)) (apply (RMMap fn)) . unFF
-instance (c ::: Domain (RMMap u fn m)) => M i c ::: Domain (RMMap u fn m) where
-  inhabits = AppBy $ \(RMMap fn) -> M . apply (RMMap fn) . unM
-
-
-
-
-
-type instance DomF (RMMap u fn m) = RM m
-type instance RngF (RMMap u fn m) = RM (MApp fn m)
-
-
-
-
--- | A @FromAt@ function is applicable only at the specified mediator and type;
--- crucially @type instance MApp (FromAt m) n = m@.
-newtype FromAt m n a = FromAt {toAt :: Med n a -> Med m a}
-
-type instance Unwrap (FromAt m n) a = Med n a -> Med m a
-instance Wrapper (FromAt m n) where wrap = FromAt; unwrap (FromAt x) = x
-
-type instance Dom (FromAt m n) t = Med n t
-type instance Rng (FromAt m n) t = Med m t
-instance a ::: Domain (FromAt m n) where inhabits = AppBy toAt
-
-type instance MApp (FromAt m) n = m
diff --git a/Type/Yoko/Natural.hs b/Type/Yoko/Natural.hs
deleted file mode 100644
--- a/Type/Yoko/Natural.hs
+++ /dev/null
@@ -1,82 +0,0 @@
-{-# LANGUAGE ExistentialQuantification, QuasiQuotes, TypeOperators,
-  Rank2Types, GADTs, ScopedTypeVariables, TypeFamilies #-}
-
-{- |
-
-Module      :  Type.Yoko.Natural
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Natural transformations and pairs.
-
--}
-
-module Type.Yoko.Natural where
-
-import Type.Yoko.Type
-import Type.Yoko.Universe
-
-
-
-type NT_ u f = forall t. u t -> f t
-
--- | Natural transformations. We use 'Unwrap' to lighten the user interface at
--- the value level, though it clutters the types a little.
-newtype NT u f = NT (forall t. u t -> Unwrap f t)
-
-nt_ :: [qP|f :: *->*|] -> (forall t. u t -> Unwrap f t) -> NT u f
-nt_ p f = NT f
-
-
-appNT :: NT u f -> u t -> Unwrap f t
-appNT (NT f) x = f x
-
-appNTF :: Wrapper f => NT u f -> NT_ u f
-appNTF (NT f) x = wrap (f x)
-
-
--- | Defining an @NT@ via type-level backtracking; ':||' uses 'Pred' to
--- short-circuit, preferring inhabitation of @u@ over @v@.
-orNT :: NT u f -> NT v f -> NT (u :|| v) f
-orNT (NT f) (NT g) = NT $ \uv -> case uv of
-  LeftU  u -> f u
-  RightU v -> g v
-
-
-constNT :: Unwrap f t -> NT ((:=:) t) f
-constNT = constNT_ Proxy
-
-constNT_ :: [qP|f :: *->*|] -> Unwrap f t -> NT ((:=:) t) f
-constNT_ p x = nt_ p $ \Refl -> x
-
-constNTF :: Wrapper f => f t -> NT ((:=:) t) f
-constNTF x = NT $ \Refl -> unwrap x
-
-
-firstNT :: NT_ u g -> NT g f -> NT u f
-firstNT g (NT f) = NT $ f . g
-
-
-
-
-
--- | Natural pairs.
-data NP u f = forall t. NP (u t) (Unwrap f t)
-
--- | Analog to "Control.Arrow"@.first@.
-firstNP :: NT_ u v -> NP u f -> NP v f
-firstNP f (NP u x) = NP (f u) x
-
-
--- | @ArrowTSS@ can be partially applied, and hence occur as the second
--- argument of @NT@, where as @f _ -> g _@ cannot.
-newtype ArrowTSS f g a = ArrowTSS (f a -> g a)
-type instance Unwrap (ArrowTSS f g) a = f a -> g a
-instance Wrapper (ArrowTSS f g) where wrap = ArrowTSS; unwrap (ArrowTSS f) = f
-
-appNTtoNP :: (Wrapper f, Wrapper g) => NT u (ArrowTSS f g) -> NP u f -> NP u g
-appNTtoNP (NT f) (NP u x) = NP u $ unwrap $ f u $ wrap x
diff --git a/Type/Yoko/Sum.hs b/Type/Yoko/Sum.hs
deleted file mode 100644
--- a/Type/Yoko/Sum.hs
+++ /dev/null
@@ -1,102 +0,0 @@
-{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, EmptyDataDecls,
-  QuasiQuotes, UndecidableInstances, ScopedTypeVariables,
-  MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances,
-  FlexibleContexts #-}
-
-{-# LANGUAGE TemplateHaskell #-}
-
-{- |
-
-Module      :  Type.Yoko.Sum
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Finite sums of types.
-
--}
-
-module Type.Yoko.Sum ((:+), All(..), TSum, Exists(..), Elem) where
-
-import Type.Yoko.Type
-import Type.Yoko.Universe
-import Data.Yoko.CoreTypes
-
-
-
-infixr 5 :+
--- | Type-sum union. We re-use 'N' as type-sum singleton and 'V' as the empty
--- type-sum.
-data t :+ s
-
-
-
--- | The higher-order universe @All@. @c@ inhabits @All u@ if @c@ is a type-sum
--- and all types in it inhabit @u@.
-data All u c where
-  SumV :: All u V
-  SumN :: (t ::: u) => u t -> All u (N t)
-  SumS :: All u c -> All u d -> All u (c :+ d)
-
-instance V ::: All u where inhabits = SumV
-instance (t ::: u) => N t ::: All u where inhabits = SumN inhabits
-instance (c ::: All u, d ::: All u) => (c :+ d) ::: All u where
-  inhabits = SumS inhabits inhabits
-
--- | @All 'NoneU'@ is satisfied by any type-sum.
-type TSum = All NoneU
-
-
-
-
-
--- | The higher-order universe @Exists@. @c@ inhabits @Exists p@ if there
--- exists a type @t@ in the type-sum @c@ for which @'True' ~ 'Pred' p t@. NB
--- that @c@ is not necessarily a type-sum; i.e. there is no well-typed total
--- function from @Exists p c@ to @TSum c@.
-data Exists p c where
-  Here    :: p t        -> Exists p (N t)
-  OnLeft  :: Exists p c -> Exists p (c :+ d)
-  OnRight :: Exists p d -> Exists p (c :+ d)
-
-
-
-data Nothing; data Just path
-
-type family IsJust a
-type instance IsJust Nothing = False
-type instance IsJust (Just path) = True
-
-type family Combine l r
-type instance Combine Nothing Nothing = Nothing
-type instance Combine Nothing (Just x) = Just (OnRight x)
-type instance Combine (Just x) r = Just (OnLeft x)
-
-
-
-data Here
-data OnLeft x
-data OnRight x
-
--- | @Elem t ts@ is 'True' if @t@ occurs in the type sum @ts@.
-type Elem t ts = IsJust (Find ((:=:) t) ts)
-
-type family Find (pred :: * -> *) c
-type instance Find p (N t) = If (Pred p t) (Just Here) Nothing
-type instance Find p (c :+ d) = Combine (Find p c) (Find p d)
-type instance Find p V = Nothing
-
-
-
-instance (Just path ~ Find p c, c ::: Exists p :? path) => c ::: Exists p where
-  inhabits = inhabits_ [qP|path|]
-
-instance (t ::: p)                => N t      ::: Exists p :? Here where
-  inhabits = Anno $ Here inhabits
-instance (c ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnLeft  path where
-  inhabits = Anno $ OnLeft  (inhabits_ [qP|path|])
-instance (d ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnRight path where
-  inhabits = Anno $ OnRight (inhabits_ [qP|path|])
diff --git a/Type/Yoko/TFunA.hs b/Type/Yoko/TFunA.hs
deleted file mode 100644
--- a/Type/Yoko/TFunA.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-{-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses,
-  FlexibleInstances, UndecidableInstances, QuasiQuotes, ScopedTypeVariables,
-  Rank2Types #-}
-
-{- |
-
-Module      :  Type.Yoko.TFunA
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-The type-level functionality of "Type.Yoko.FunA" functions.
-
--}
-
-module Type.Yoko.TFunA (TApp, CMap(..), CApp) where
-
-import Type.Yoko.TSTSS
-
-import Type.Yoko.Fun
-import Type.Yoko.FunA
-
-import Type.Yoko.Type
-import Type.Yoko.Universe
-
-import Data.Yoko.CoreTypes
-import Data.Yoko.Generic
-
-import Control.Applicative (Applicative(pure))
-import Data.Traversable (Traversable(traverse))
-
-
-
-
--- | The @TApp@ type family encodes the type-level functionality of
--- "Type.Yoko.Fun" functions.
-type family TApp (fn :: * -> *) t
-
-
-
-
--- | @CMap fn m c@ applies @fn@ to all recursive occurrences (i.e. 'R') in a
--- "Data.Yoko.Core" type @c@ that's mediated by @m@. The domain ('Dom') is @RM
--- m c@ and the range ('Rng') is @RM m (CApp (fn m) c)@. The 'Idiom' is @Idiom
--- (fn m)@.
-newtype CMap fn m c = CMap (forall t. fn m t)
-
-type instance Dom (CMap fn m) c = RM m c
-type instance Rng (CMap fn m) c = RM m (CApp (fn m) c)
-type instance Idiom (CMap fn m) = Idiom (fn m)
-
--- | @CApp fn c@ applies the type-function @fn@ to all recursive occurrences
--- (i.e. 'R') in the "Data.Yoko.Core" type @c@.
-type family CApp (fn :: * -> *) c
-type instance CApp fn (D a) = D a
-type instance CApp fn (F f c) = F f (CApp fn c)
-type instance CApp fn (FF ff c d) = FF ff (CApp fn c) (CApp fn d)
-type instance CApp fn (M i c) = M i (CApp fn c)
-type instance CApp fn (R t) = R (TApp fn t)
-type instance CApp fn U = U
-type instance CApp fn V = V
-
-pureDomain :: (Dom fn t ~ Rng fn t) => Domain fn t
-pureDomain = AppBy $ \_ -> id
-
-instance D a ::: Domain (CMap fn m) where inhabits = pureDomain
-instance (c ::: Domain (CMap fn m), Traversable f
-         ) => F f c ::: Domain (CMap fn m) where
-  inhabits = AppBy $ \(CMap fn) -> F . fmap (apply (CMap fn)) . unF
-instance (c ::: Domain (CMap fn m), d ::: Domain (CMap fn m),
-          FunctorTSTSS ff
-         ) => FF ff c d ::: Domain (CMap fn m) where
-  inhabits = AppBy $ \(CMap fn) -> FF .
-               fmapTSTSS (apply (CMap fn)) (apply (CMap fn)) . unFF
-instance (c ::: Domain (CMap fn m)) => M i c ::: Domain (CMap fn m) where
-  inhabits = AppBy $ \(CMap fn) -> M . apply (CMap fn) . unM
-instance (t ::: Domain (fn m), Wrapper (fn m),
-          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)
-         ) => R t ::: Domain (CMap fn m) where
-  inhabits = AppBy $ \(CMap fn) -> R . apply (fn :: fn m t) . unR
-instance U ::: Domain (CMap fn m) where inhabits = pureDomain
-instance V ::: Domain (CMap fn m) where inhabits = pureDomain
-
-pureDomainA :: (Dom fn t ~ Rng fn t, Applicative (Idiom fn)) => DomainA fn t
-pureDomainA = AppABy $ \_ -> pure
-
-instance Applicative (Idiom (fn m)) => D a ::: DomainA (CMap fn m) where
-  inhabits = pureDomainA
-instance (c ::: DomainA (CMap fn m), Applicative (Idiom (fn m)),
-          Traversable f) => F f c ::: DomainA (CMap fn m) where
-  inhabits = AppABy $ \(CMap fn) -> fmap F . traverse (applyA (CMap fn)) . unF
-instance (c ::: DomainA (CMap fn m), d ::: DomainA (CMap fn m),
-          Applicative (Idiom (fn m)), TraversableTSTSS ff
-         ) => FF ff c d ::: DomainA (CMap fn m) where
-  inhabits = AppABy $ \(CMap fn) -> fmap FF .
-               traverseTSTSS (applyA (CMap fn)) (applyA (CMap fn)) . unFF
-instance (c ::: DomainA (CMap fn m), Functor (Idiom (fn m))
-         ) => M i c ::: DomainA (CMap fn m) where
-  inhabits = AppABy $ \(CMap fn) -> fmap M . applyA (CMap fn) . unM
-instance (t ::: DomainA (fn m), Functor (Idiom (fn m)), Wrapper (fn m),
-          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)
-         ) => R t ::: DomainA (CMap fn m) where
-  inhabits = AppABy $ \(CMap fn) -> fmap R . applyA (fn :: fn m t) . unR
-instance Applicative (Idiom (fn m)) => U ::: DomainA (CMap fn m) where
-  inhabits = pureDomainA
-instance Applicative (Idiom (fn m)) => V ::: DomainA (CMap fn m) where
-  inhabits = pureDomainA
diff --git a/Type/Yoko/TSTSS.hs b/Type/Yoko/TSTSS.hs
deleted file mode 100644
--- a/Type/Yoko/TSTSS.hs
+++ /dev/null
@@ -1,29 +0,0 @@
-{- |
-
-Module      :  Type.Yoko.TSTSS
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Classes for @* -> * -> *@ types.
-
--}
-
-module Type.Yoko.TSTSS where
-
-import Control.Applicative
-
-
-
-class FunctorTSTSS ff where
-  fmapTSTSS :: (a -> c) -> (b -> d) -> ff a b -> ff c d
-instance FunctorTSTSS Either where fmapTSTSS f g = (Left . f) `either` (Right . g)
-instance FunctorTSTSS (,) where fmapTSTSS f g ~(x, y) = (f x, g y)
-
-class TraversableTSTSS ff where
-  traverseTSTSS :: Applicative i => (a -> i c) -> (b -> i d) -> ff a b -> i (ff c d)
-instance TraversableTSTSS Either where traverseTSTSS f g = either (fmap Left . f) (fmap Right . g)
-instance TraversableTSTSS (,) where traverseTSTSS f g ~(x, y) = (,) <$> f x <*> g y
diff --git a/Type/Yoko/Type.hs b/Type/Yoko/Type.hs
deleted file mode 100644
--- a/Type/Yoko/Type.hs
+++ /dev/null
@@ -1,84 +0,0 @@
-{-# LANGUAGE TypeFamilies, FlexibleContexts, TypeOperators,
-  ScopedTypeVariables, UndecidableInstances, FlexibleInstances #-}
-
-{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, GADTs #-}
-
-{- |
-
-Module      :  Type.Yoko.Type
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Some fundamental types central to @yoko@.
-
--}
-
-module Type.Yoko.Type
-  (qK, Proxy(Proxy), module Type.Yoko.Type, module Type.Spine.Stage0,
-   module Type.Booleans, IsEQ, Compare, EqT(..), (:=:)(..)) where
-
-import Data.Proxy (Proxy(..))
-
-import Type.Spine
-import Type.Spine.Stage0 (KS, KTSS)
-import Type.Serialize
-
-import Data.Proxy.TH (qProxy)
-import Type.Booleans
---import Polarity
-import Type.Ord.SpineSerialize (IsEQ, Compare)
-
-import Data.Type.Equality
-
-
-
-qP = qProxy
-
-
-
--- | The @Med@ type family encodes the behavior of recursion mediators.
-type family Med m a
--- | @type instance Med IdM a = a@.
-data IdM = IdM; type instance Med IdM a = a
-
-
-
-
--- | The @Wrapper@ class is used to make term-level programming newtypes a
--- little more lightweight from the user perspective.
-class Wrapper f where wrap :: Unwrap f a -> f a; unwrap :: f a -> Unwrap f a
-type family Unwrap (f :: * -> *) a
-
-
-
--- | The @Pred@ type family realizes type-level predicates (over types) that
--- yield a type-level Boolean: either 'True' or 'False'. Predicates are often
--- universes.
-type family Pred (p :: * -> *) a
-
-type instance Pred ((:=:) a) b = IsEQ (Compare a b)
-
-
-
-
-
-derive n = do
-  d <- spineType n
-  (d ++) `fmap` serializeTypeAsHash n
-
-
-
-
-
--- | Composition of @* -> *@ types.
-newtype (f :. g) a = Compose (f (g a))
-type instance Unwrap (f :. g) a = f (g a)
-instance Wrapper (f :. g) where wrap = Compose; unwrap (Compose x) = x
-
--- | Explicitly takes the inner type as a proxy.
-composeWith :: [qProxy|g :: *->*|] -> f (g a) -> (f :. g) a
-composeWith _ = Compose
diff --git a/Type/Yoko/Universe.hs b/Type/Yoko/Universe.hs
deleted file mode 100644
--- a/Type/Yoko/Universe.hs
+++ /dev/null
@@ -1,87 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,
-  FlexibleContexts, ScopedTypeVariables, FlexibleInstances,
-  UndecidableInstances, GADTs, Rank2Types, EmptyDataDecls #-}
-
-{- |
-
-Module      :  Type.Yoko.Universe
-Copyright   :  (c) The University of Kansas 2011
-License     :  BSD3
-
-Maintainer  :  nicolas.frisby@gmail.com
-Stability   :  experimental
-Portability :  see LANGUAGE pragmas (... GHC)
-
-Type universes.
-
--}
-
-module Type.Yoko.Universe where
-
-import Type.Yoko.Type
-
-infix 0 :::
--- | A /universe/ determines a set of types; /open/ or /closed/. @(:::)@ is
--- comparable to the @Sat@ class (e.g. from @SYB3@).
-class a ::: u where inhabits :: u a
-
-
-
--- | @(:?)@ helps us write /guarded/ @(:::)@ instances (see
--- <http://hackage.haskell.org/trac/ghc/ticket/5590>)
-infix 1 :?
-data (u :? anno) a = Anno (u a)
-
-
--- | For use with @(:::)@ instances that use @(:?)@.
-inhabits_ :: forall a u anno. (a ::: u :? anno) => [qP|anno|] -> u a
-inhabits_ _ = i where Anno i = inhabits :: (u :? anno) a
-
--- | Sometimes it's helpful to specify which @t@ must be in the universe.
-inhabitsFor :: (t ::: u) => [qP|t|] -> u t
-inhabitsFor _ = inhabits
-
-
-
--- | The universe of all types; it has /no/ contraints.
-data NoneU a = NoneU
-instance a ::: NoneU where inhabits = NoneU
-
-type Both = (:&&)
-infixr 3 :&&
--- | Universe product.
-data (u :&& v) a where (:&&) :: (a ::: u, a ::: v) => {fstU :: u a, sndU :: v a} -> (u :&& v) a
-instance (a ::: u, a ::: v) => a ::: u :&& v where
-  inhabits = inhabits :&& inhabits
-
-type instance Pred (p :&& q) a = And (Pred p a) (Pred q a)
-
-
-
-instance (a ~ b) => b ::: (:=:) a where inhabits = Refl
-
-
-infixr 2 :||
--- | Universe sum.
-data (u :|| v) a where
-  LeftU  :: u a -> (u :|| v) a
-  RightU :: v a -> (u :|| v) a
-
-instance (anno ~ Pred u a, a ::: u :|| v :? anno) => a ::: u :|| v where
-  inhabits = inhabits_ [qP|anno|]
-instance (True  ~ Pred u a, a ::: u) => a ::: u :|| v :? True where
-  inhabits = Anno $ LeftU inhabits
-instance (False ~ Pred u a, a ::: v) => a ::: u :|| v :? False where
-  inhabits = Anno $ RightU inhabits
-
-
-type instance Pred (u :|| v) t = Or (Pred u t) (Pred v t)
-
-
-
--- | The empty universe.
-data VoidU t -- the empty universe
-
-
-
-instance (f t ::: u) => t ::: (u :. f) where inhabits = Compose inhabits
diff --git a/yoko.cabal b/yoko.cabal
--- a/yoko.cabal
+++ b/yoko.cabal
@@ -1,8 +1,11 @@
 name: yoko
-version: 0.2
-synopsis: generic programming with disbanded constructors 
+version: 0.3
+synopsis: Generic Programming with Disbanded Data Types
 
-description: @yoko@ views a nominal datatype as a /band/ of constructors, each
+description:
+  Based off of the paper \"A Pattern for Almost Compositional Functions\" at <http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf>, submitted to ICFP 2012.
+  .
+  @yoko@ views a nominal datatype as a /band/ of constructors, each
   a nominal type in its own right. Such datatypes can be disbanded via the
   @disband@ function into an anonymous sum of nominal constructors, and vice
   versa via the @band@ function. This library uses extensive type-level
@@ -19,10 +22,10 @@
   /constructor types/.
   .
   @
-    data John = John ...
-    data Paul = Paul ...
+    data John   = John   ...
+    data Paul   = Paul   ...
     data George = George ...
-    data Ringo = Ringo ...
+    data Ringo  = Ringo  ...
   @
   .
   @yoko@'s conceptual foundations start there. In particular, this allows a
@@ -30,32 +33,37 @@
   and sibling constructors.
   .
   As a generic programming library, @yoko@ extends @instant-generics@ with
-  support for constructor-centric generic programming. The @Examples/LL.hs@
+  support for constructor-centric generic programming. The @Examples/LambdaLift/@
   file distributed with the @yoko@ source demonstrates defining a
-  lambda-lifting conversion between the two types @Inner@, which has lambdas,
+  lambda-lifting conversion between the two types @ULC@, which has lambdas,
   and @Prog@, which has top-level function declarations instead.
   .
   @
-    data Inner = Lam Type Inner | Var Int | App Inner Inner
+    data ULC = Lam Type ULC | Var Int | Let [Decl] ULC | App ULC ULC
   .
-    data Term = Var Int | App Term Term | DVar Int
-    data Prog = Prog ([Type], Type, Term) Term
+    data Decl = Decl Type ULC
+  .
+  .
+  .
+    data Prog = Prog [FunDec] TLF
+    type FunDec = ([Type], [Type], Type, TLF)
+  .
+    data TLF = Top Int [Occ] | Occ Occ | App TLF TLF
+    data Occ = Par Int | Env Int
   @
   .
   These types are defined in separate modules, since they have constructors
   with the same name. Indeed, the fact that they having matching constructors
-  named @App@ is crucial for @yoko@'s automatic conversion from @Inner@'s @App@
-  to @Term@'s @App@. As written, the generic lambda-lifter would continue to
-  work for any new @Inner@ constructors (e.g. syntax for tuples or mutable
+  named @App@ is crucial for @yoko@'s automatic conversion from @ULC@'s @App@
+  to @TLF@'s @App@. As written, the generic lambda-lifter would continue to
+  work for any new @ULC@ constructors (e.g. syntax for tuples or mutable
   references) as long as constructors with the same names and analogous fields
-  were added to @Term@ and the semantics of those constructors doesn't involve
+  were added to @TLF@ and the semantics of those constructors doesn't involve
   binding. This default behavior of the lambda-lifter is specified in about ten
   lines of user code.
   .
   Existing generic libraries don't use constructor names to the degree that
-  @yoko@ does, and so cannot accomodate generic /conversions/ nearly as well.
-  .
-  See the wiki at <http://code.google.com/p/yoko> for more documentation.
+  @yoko@ does, and so cannot accomodate generic /conversions/ as well.
 
 category: Generics, Reflection
 
@@ -73,37 +81,30 @@
 
 
 library
-  build-depends: base >= 4 && < 5
-  build-depends: type-equality < 0.2, tagged >= 0.2 && < 0.3
+  build-depends: base >= 4 && < 5, template-haskell
+  build-depends: type-equality < 0.2
 
-  build-depends: type-booleans < 0.2, type-spine < 0.2, tagged-th < 0.2,
-    type-digits < 0.2, type-cereal < 0.2, type-ord < 0.2, type-ord-spine-cereal
-    < 0.2
+  build-depends:
+    type-booleans < 0.2,
+    type-spine < 0.2,
+    tagged-th < 0.2,
+    type-digits < 0.2,
+    type-cereal < 0.2,
+    type-ord < 0.2,
+    type-ord-spine-cereal < 0.2
 
-  exposed-modules: Type.Yoko,
-                   Type.Yoko.Type,
-                   Type.Yoko.Universe,
-                   Type.Yoko.Natural,
-                   Type.Yoko.Sum,
-                   Type.Yoko.BTree,
-                   Type.Yoko.TSTSS,
-                   Type.Yoko.Fun,
-                   Type.Yoko.FunA,
-                   Type.Yoko.MFun,
-                   Type.Yoko.TFunA,
+  exposed-modules:
+    Data.Yoko, Data.Yoko.HCompos,
 
-                   Data.Yoko,
-                   Data.Yoko.Core,
-                   Data.Yoko.CoreTypes,
-                   Data.Yoko.Generic,
-                   Data.Yoko.ReflectBase,
-                   Data.Yoko.Reflect,
-                   Data.Yoko.InDT,
-                   Data.Yoko.Reduce,
-                   Data.Yoko.Cata
+    Data.Yoko.TypeBasics, Data.Yoko.Each
 
---                   Examples.TermBase,
---                   Examples.TermGeneric,
---                   Examples.InnerBase,
---                   Examples.InnerGeneric,
---                   Examples.TermInner
+  other-modules:
+    Data.Yoko.MaybeKind,
+    Data.Yoko.Representation,
+    Data.Yoko.TypeSums,
+    Data.Yoko.TypeSumsAux
+
+    -- under development
+--    Data.Yoko.Fold,
+--    Data.Yoko.Map,
+--    Data.Yoko.OnRs