diff --git a/CHANGES b/CHANGES
new file mode 100644
--- /dev/null
+++ b/CHANGES
@@ -0,0 +1,9 @@
+0.1 -> 0.2
+===============
+
+* improved the treatment of automatically generating algebras
+* emphasizing DCOf over DCU
+* moved all of the documentation from README to http://code.google.com/p/yoko
+* still obsessively tweaking names throughout the library
+* improved the treatment of unique constructors
+* added SiblingOf and a corresponding superclass constraint to DT
diff --git a/Data/Yoko/Algebra.hs b/Data/Yoko/Algebra.hs
deleted file mode 100644
--- a/Data/Yoko/Algebra.hs
+++ /dev/null
@@ -1,86 +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)
-
-Algebras and catamorphisms for mutually-recursive datatypes.
-
--}
-module Data.Yoko.Algebra
-  (Alg, Algebra(..), Algebras, SiblingAlgs, algebras, CataD(..), catas, cata,
-  module Data.Yoko.Reduce) where
-    
-import Type.Yoko
-
-import Data.Yoko.Generic
-import Data.Yoko.Reflect
-import Data.Yoko.Reduce
-
-
--- | A @t@-algebra maps a sum of a @t@'s constructors into a mediation of @t@.
-type Alg m t = AnRMNUni m (DCs 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 ReduceD m t where
-  ReduceD :: (Reduce m (DCs t), t ~ LeftmostRange (DCs t)) => ReduceD m t
-instance (Reduce m (DCs t), t ~ LeftmostRange (DCs t)
-         ) => t ::: ReduceD m where inhabits = ReduceD
-
-type Algebras ts m = Each ts (Algebra m)
-type SiblingAlgs t m = Algebras (Siblings t) m
-
--- | Builds an 'Each' of algebras via 'Reduce'.
-algebras :: forall ts m. (ts ::: All (ReduceD m)) => [qP|m|] -> Algebras ts m
-algebras _ = each [qP|ReduceD m :: *->*|] $ \ReduceD -> reduce
-
-
-
-
--- | @t@ inhabits @CataD 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 CataD ts m t where
-  CataD :: (DT t, ts ~ Siblings t, t ::: Uni ts,
-            DCs t ::: All
-              (YieldsArrowTSSD
-               (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
-            ts ::: All (CataD ts m)
-           ) => CataD ts m t
-instance (DT t, ts ~ Siblings t, t ::: Uni ts,
-          DCs t ::: All
-            (YieldsArrowTSSD
-             (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),
-          ts ::: All (CataD ts m)
-         ) => t ::: CataD ts m where inhabits = CataD
-
-catas :: forall m ts. (ts ::: All (CataD ts m)) =>
-         Algebras ts m -> Each ts (FromAt m IdM)
-catas fs = each [qP|CataD ts m :: *->*|] $ \d@CataD -> cataD d fs
-
-cataD :: forall m t. CataD (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t
-cataD CataD fs =
-  prjEach (inhabitsFor [qP|t|]) fs .
-  appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $
-             RMMap $ catas fs) . firstNP toUni . disband
-
--- | Uses the @m@-mediated algebras for @t@'s siblings to reduce a @t@ to @Med
--- m t@.
-cata :: (t ::: CataD (Siblings t) m) => SiblingAlgs t m -> t -> Med m t
-cata = cataD inhabits
diff --git a/Data/Yoko/Cata.hs b/Data/Yoko/Cata.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Cata.hs
@@ -0,0 +1,78 @@
+{-# 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/InDT.hs b/Data/Yoko/InDT.hs
--- a/Data/Yoko/InDT.hs
+++ b/Data/Yoko/InDT.hs
@@ -24,18 +24,18 @@
 
 
 
--- | A type @t@ inhabits @HasTagRepDCD tag c@ if @t@ is a 'DT' and there exists a @t@
+-- | A type @t@ inhabits @HasTagRepU tag c@ if @t@ is a 'DT' and there exists a @t@
 -- constructor satisfying @'TagRepIs' tag c@.
-data HasTagRepDCD tag c t where
-  HasTagRepDCD :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->
-           HasTagRepDCD tag c t
+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 ::: HasTagRepDCD tag c where inhabits = HasTagRepDCD inhabits
+         ) => t ::: HasTagRepU tag c where inhabits = HasTagRepU inhabits
 
--- | Given @HasTagRepDCD tag c t@, a trivially-mediated @c@ value can be embedded into
+-- | Given @HasTagRepU tag c t@, a trivially-mediated @c@ value can be embedded into
 -- @t@.
-hasTagRepDCD :: HasTagRepDCD tag c t -> RMI c -> t
-hasTagRepDCD (HasTagRepDCD d) = w d where
+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
@@ -46,33 +46,33 @@
 
 -- | Often times, we're interested in the universe of types accomodating a data
 -- constructor's image under some type-function.
-type HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc))
+type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc))
 
--- | A constructor type @dc@ inhabits @ImageHasTagRepDCD t fn@ if
+-- | 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 ImageInDTD t fn dc where
-  ImageInDTD :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)
-                ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTD t fn dc
-instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc
-         ) => dc ::: ImageInDTD t fn where
-  inhabits = ImageInDTD inhabits
+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 @ImageInDTD t fn dc@, a trivially-mediated @dc@ value can be
+-- | Given @ImageInDTU t fn dc@, a trivially-mediated @dc@ value can be
 -- embedded into @t@.
-imageInDTD :: (forall t. fn IdM t) -> ImageInDTD t fn dc -> RMNI dc -> t
-imageInDTD fn (ImageInDTD d) = hasTagRepDCD d . apply (CMap fn) . rep
+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)
-                 ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTDA t fn dc
-instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc
+                 ) => 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
 
-imageInDTAD :: Functor (Idiom (fn IdM)) =>
+imageInDTAU :: Functor (Idiom (fn IdM)) =>
                (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t
-imageInDTAD fn (ImageInDTDA d) = fmap (hasTagRepDCD d) . applyA (CMap fn) . rep
+imageInDTAU fn (ImageInDTDA d) = fmap (hasTagRepU d) . applyA (CMap fn) . rep
diff --git a/Data/Yoko/Reduce.hs b/Data/Yoko/Reduce.hs
--- a/Data/Yoko/Reduce.hs
+++ b/Data/Yoko/Reduce.hs
@@ -12,10 +12,12 @@
 Stability   :  experimental
 Portability :  see LANGUAGE pragmas (... GHC)
 
-Reduction of a band of constructors into a mediation of their range.
+A @t@-algebra reduces a disbanded @t@ into a mediation of @t@.
 
 -}
-module Data.Yoko.Reduce (AnRMNUni, Reduce(..), ReduceDC(..)) where
+module Data.Yoko.Reduce
+  (Alg, Algebra(..), AlgebraU(..),
+   algebraFin, AlgebraDT(..), AlgebraUni, AlgebraDC(..)) where
 
 import Type.Yoko
 
@@ -24,25 +26,46 @@
 
 
 
-type AnRMNUni m ts = AnRMN m (Uni ts)
 
 
+-- | 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
 
--- | @reduce@ embeds a mediated sum of constructors into a mediation of their
--- range.
-class (dcs ::: All IsDC) => Reduce m dcs where
-  reduce :: AnRMNUni m dcs -> Med m (LeftmostRange dcs)
+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),
-          Reduce m ts, Reduce m us) => Reduce m (ts :+ us) where
-  reduce = reduce `two` reduce
-instance ReduceDC m dc => Reduce m (N dc) where
-  reduce = reduceDC . unRMNUni where
-    unRMNUni :: AnRMNUni m (N dc) -> RMN m dc
-    unRMNUni (NP (Uni (Here Refl)) x) = x
+          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
 
--- | @reduceDC@ embeds a mediated constructor into a mediation of its range.
-class DC dc => ReduceDC m dc where reduceDC :: RMN m dc -> Med m (Range dc)
+-- | @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)
 
 
 
diff --git a/Data/Yoko/Reflect.hs b/Data/Yoko/Reflect.hs
--- a/Data/Yoko/Reflect.hs
+++ b/Data/Yoko/Reflect.hs
@@ -22,7 +22,7 @@
 import Type.Yoko
 
 import Data.Yoko.Generic
-import Data.Yoko.ReflectBase
+import Data.Yoko.ReflectBase hiding (DCU)
 
 
 
@@ -44,7 +44,25 @@
 
 
 
+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
@@ -57,13 +75,13 @@
 
 
 -- | Just a specialization: @dcDispatch = (. disband) . dcDispatch'@.
-dcDispatch :: DT t => NT (DCU t) (RMNTo IdM b) -> t -> b
+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 (DCU t) (RMNTo IdM b) -> Disbanded IdM t -> b
-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
 
 
 
diff --git a/Data/Yoko/ReflectBase.hs b/Data/Yoko/ReflectBase.hs
--- a/Data/Yoko/ReflectBase.hs
+++ b/Data/Yoko/ReflectBase.hs
@@ -40,12 +40,12 @@
 
   -- | The evidence that this constructor inhabits the datatype constructor
   -- universe of its range.
-  tag :: DCU (Range dc) dc; tag = inhabits
+  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 tg of
-    DCOf (eqT (tag :: DCU (Range dc) dc) -> Just Refl) -> Just fds
+  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.
@@ -57,11 +57,14 @@
 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)
-
--- | @UniqueDC@ is for newtypes and GADT constructors where the type @dc@
--- determines the constructor.
-class UniqueDC dc where uniqueTo :: Range dc -> RMNI dc
+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
 
 
 
@@ -69,7 +72,7 @@
 type Disbanded m t = AnRMN m (DCOf t)
 
 disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)
-disbanded fds = NP (DCOf tag) fds
+disbanded fds = NP tag fds
 
 band :: Disbanded IdM t -> t
 band (NP (DCOf _) fds) = fr fds
@@ -81,12 +84,12 @@
 type instance LeftmostRange (N dc) = Range dc
 type instance LeftmostRange (c :+ d) = LeftmostRange c
 
-type DCs t = Inhabitants (DCU t)
+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 GistD),
-       Siblings t ::: TSum -- need GHC 7.2: , t ~ LeftmostRange (DCs 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
@@ -99,7 +102,8 @@
   -- of @Recurs . DCs@, by definition.)
   type Siblings t
  
-  -- | The data constructor universe.
+  -- | 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.
diff --git a/Examples/Ex.hs b/Examples/Ex.hs
new file mode 100644
--- /dev/null
+++ b/Examples/Ex.hs
@@ -0,0 +1,6 @@
+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
new file mode 100644
--- /dev/null
+++ b/Examples/ExG.hs
@@ -0,0 +1,60 @@
+{-# 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/InnerGeneric.hs b/Examples/InnerGeneric.hs
--- a/Examples/InnerGeneric.hs
+++ b/Examples/InnerGeneric.hs
@@ -65,12 +65,12 @@
 instance Finite (DCU Inner) where
   toUni Lam_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits
 instance Etinif (DCU Inner) where
-  fromUni (Uni x) = case x of
+  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 = fromUni inhabits
+  inhabits = frUni inhabits
 instance EqT (DCU Inner) where eqT = eqTFin
 
 
diff --git a/Examples/LL.hs b/Examples/LL.hs
--- a/Examples/LL.hs
+++ b/Examples/LL.hs
@@ -44,8 +44,8 @@
 
 instance (IdM ~ m) => Inner ::: DomainA (LL m) where
   inhabits = AppABy $ \_ -> dcDispatch $
-    eachOrNT (oneF (RMNTo llLam) ||. llVar) $ NT $ imageInDTAD LL
---  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAD LL
+    eachOrNT (oneF (RMNTo llLam) ||. llVar) $ NT $ imageInDTAU LL
+--  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAU LL
 
 
 
diff --git a/Examples/LLGeneric.hs b/Examples/LLGeneric.hs
--- a/Examples/LLGeneric.hs
+++ b/Examples/LLGeneric.hs
@@ -64,12 +64,12 @@
 instance Finite (DCU Term) where
   toUni DVar_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits
 instance Etinif (DCU Term) where
-  fromUni (Uni x) = case x of
+  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 = fromUni inhabits
+  inhabits = frUni inhabits
 instance EqT (DCU Term) where eqT = eqTFin
 
 
diff --git a/Examples/ReflectAux.hs b/Examples/ReflectAux.hs
--- a/Examples/ReflectAux.hs
+++ b/Examples/ReflectAux.hs
@@ -11,8 +11,9 @@
 Just bundles up some imports for the various @*Generic@ modules.
 
 -}
-module Examples.ReflectAux (encode, module Data.Yoko) where
+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/TermGeneric.hs b/Examples/TermGeneric.hs
--- a/Examples/TermGeneric.hs
+++ b/Examples/TermGeneric.hs
@@ -69,12 +69,12 @@
 instance Finite (DCU B.Type) where
   toUni TBool_ = inhabits; toUni TInt_ = inhabits; toUni TArrow_ = inhabits
 instance Etinif (DCU B.Type) where
-  fromUni (Uni x) = case x of
+  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 = fromUni inhabits
+  inhabits = frUni inhabits
 instance EqT (DCU B.Type) where eqT = eqTFin
 
 type instance Tag Lam = $(return $ encode "Lam")
@@ -121,13 +121,13 @@
   toUni Lam_ = inhabits; toUni Var_ = inhabits
   toUni App_ = inhabits; toUni Let_ = inhabits
 instance Etinif (DCU B.Term) where
-  fromUni (Uni x) = case x of
+  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 = fromUni inhabits
+  inhabits = frUni inhabits
 instance EqT (DCU B.Term) where eqT = eqTFin
 
 type instance Tag Decl = $(return $ encode "Decl")
@@ -135,9 +135,8 @@
 instance DC Decl where
   occName _ = "Decl"
   type Range Decl = B.Decl
-  to = Just . uniqueTo; fr ~(Decl ds tm) = B.Decl ds tm
+  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 UniqueDC Decl where uniqueTo ~(B.Decl ds tm) = Decl ds tm
 instance DT B.Decl where
   packageName _ = "datatype-reflect"
   moduleName _ = "DeclBase"
@@ -148,9 +147,9 @@
 instance Finite (DCU B.Decl) where
   toUni Decl_ = inhabits
 instance Etinif (DCU B.Decl) where
-  fromUni (Uni (Here Refl)) = Decl_
+  frUni (Uni (Here Refl)) = Decl_
 instance (t ::: Uni (DCs B.Decl)) => t ::: DCU B.Decl where
-  inhabits = fromUni inhabits
+  inhabits = frUni inhabits
 instance EqT (DCU B.Decl) where eqT = eqTFin
 
 
diff --git a/Examples/TermInner.hs b/Examples/TermInner.hs
--- a/Examples/TermInner.hs
+++ b/Examples/TermInner.hs
@@ -46,7 +46,7 @@
 
 instance (IdM ~ m) => Term ::: Domain (Elab m) where
   inhabits = AppBy $ \_ -> dcDispatch $
-    eachOrNT (oneF $ RMNTo elab_Let) $ NT $ imageInDTD Elab
+    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
diff --git a/Examples/TermTest.hs b/Examples/TermTest.hs
--- a/Examples/TermTest.hs
+++ b/Examples/TermTest.hs
@@ -14,7 +14,7 @@
 Portability :  see LANGUAGE pragmas (... GHC)
 
 A denotational semantics for the simple-typed lambda calculus via
-"Data.Yoko.Algebra".
+"Data.Yoko.Cata".
 
 -}
 module Examples.TermTest where
@@ -23,7 +23,8 @@
 import qualified Examples.TermGeneric as G
 
 import Type.Yoko
-import Data.Yoko.Algebra
+import Data.Yoko.Cata
+import Data.Yoko
 
 
 -- | Since our family of abstract data types don't correspond to the
@@ -52,17 +53,27 @@
 type instance Med SemM Term = Sem
 type instance Med SemM Decl = (Type, Sem)
 
-instance ReduceDC SemM G.Lam where reduceDC = eLam
-instance ReduceDC SemM G.Var where reduceDC = eVar
-instance ReduceDC SemM G.App where reduceDC = eApp
-instance ReduceDC SemM G.Let where reduceDC = eLet
+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 ReduceDC SemM G.Decl where reduceDC = eDecl
+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|]
 
--- NB equivalent
-eval' x = ($ x) $ cata $ (reduce .|. reduce) -- :: AlgebraFam Term 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)
 
 
 
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,1 +1,24 @@
-BSD3
+Copyright (c) 2011, University of Kansas
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+  * Redistributions of source code must retain the above copyright notice, this
+    list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright notice,
+    this list of conditions and the following disclaimer in the documentation
+    and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
diff --git a/README b/README
--- a/README
+++ b/README
@@ -1,249 +1,1 @@
-drex (read "dee-recks")
-
-While the "d" is just for "datatype", "rex" is bit of a double entendre.
-
-The representation classes (DT, Generic, Gist) each disinvest their parameter
-of its nominality, similar to how a king disinvests nobles of their titles.
-
-Each class also dismantles, or "wrecks", its parameter: DT takes a single type
-to a sum of its constructors, Generic maps a constructor to its underlying
-shape, and Gist forgets the shape and mediation.
-
-... Also, it sounds like "T-rex".
-
-===================
-
-See http://j.mp/tNLx40 for a Google spreadsheet cataloging the various d-rex
-concepts and components.
-
-====================
-
-#1 Basic Universes
-
-The @:::@ class in the @Universe@ module is pervasive in d-rex. The constraint
-@t ::: u@ is read "t inhabits u" (or "t satisfies u", if you must). @u@ is a
-/universe/, a type that represents a possibly finite, possibly paradoxical
-collection of types. Universes can be /open/ or /closed/. @Lit@, for example,
-is closed.
-
-  in module Ex
-    data Lit t where IntLit :: Lit Int; CharLit :: Lit Char
-
-@ShowD@ is open, since new instances of @Show@ can be declared anywhere.
-
-  in module Ex
-    data ShowD t where ShowD :: Show t => ShowD t
-
-(The "D" suffix is for "dictionary", since this GADT operationally reifies the
-@Show@ dictionary. @(\ShowD x -> show x) :: ShowD t -> t -> String@ -- note
-that there's no @Show t@ constraint in that type.
-
-Some closed universes are also finite. There exists an isomorphism between such
-a universes and a finite set of types (#4 below).
-
-#2 Constructor Universes
-
-d-rex's principle novelty is its support of the finite closed universe of a
-datatype's constructors, codifed as the indexed data family @DCU@. The @open@
-method of the @DT@ type class converts from a type to its universe of
-constructors. @close@ goes back the other way.
-
-As d-rex breaks a datatype into its universe of constructors, it also generates
-a new void type per constructor. For example, d-rex breaks @Either a b@ into
-
-  in module G
-    data Left a b; data Right a b
-
-With these types, d-rex declares the constructor universe of @Either a b@.
-
-  in module G
-    data instance DCU (Either a b) where
-      Left_  :: DCU (Either a b) (Left  a b)
-      Right_ :: DCU (Either a b) (Right a b)
-
-Note that each constructor type inherits the original type's parameters. d-rex
-also declares an instance of the data family @RM@ for each constructor -- the
-resulting types are called /fields types/.
-
-  in module G
-    newtype instance RM (N (Left  a b)) m = Left a
-    newtype instance RM (N (Right a b)) m = Right b
-
-  in module ReflectBaseR
-    type Fields dc = RM (N dc)
-
-(Clearly, d-rex re-uses the constructor names. Hence, the generic declarations
-must always generated in a separate module to enable namespace management.)
-
-The data family @RM@, the @m@ parameter, type family @App@, and @N@ are
-explained in the next section. In the interim, we'll make do with a couple
-brief declarations.
-
-  in module Type
-    data IdT; type instance App IdT a = a
-
-There now exists an isomorphism between @Either a b@ and
-@forall dc. (DCU (Either a b) dc, Fields dc IdT).
-
-  Left x    =~= (Left_, G.Left x)
-  Right x   =~= (Right_, G.Right x)
-
-The @DCU@ tag is a crucial part of this pair -- without it, G.Left and G.Right
-would have inequal types!
-
-#3 Recursion-mediated types
-
-The data family @RM@ stands for "recursion-mediated". The idea is that the @m@
-parameter is applied to all recursive type occurences in a constructor's
-fields.
-
-  in module T
-    data Even a = Zero | Even a (Odd a)
-    data Odd  a = Odd a (Even a) 
-
-  in module G
-    data Zero a; data Even a; data Odd a
-    data instance RM (N (Zero   a)) m
-    data instance RM (N (G.Even a)) m = Even a (App m (T.Odd  a))
-    data instance RM (N (G.Odd  a)) m = Odd  a (App m (T.Even a))
-
-  in module Type
-    data True = True; data False = False
-
-  in module Ex
-    data ParityM
-    type instance App ParityM (T.Even a) = False
-    type instance App ParityM (T.Odd  a) = True
-
-    ex0 = Even 'e' True :: Fields (G.Even Char) ParityM
-    ex1 = Odd 'o' False :: Fields (G.Odd  Char) ParityM
-
-The recursion-mediated representation of the fields types enables their
-re-use. For example, the same fields type can be used to define a bottom-up
-reducer, where the recursive occurrences have been replaced with the result of
-the catamorphism.
-
-  in module Ex
-    data LengthM
-    type instance App LengthM (T.Even a) = Int
-    type instance App LengthM (T.Odd  a) = Int
-
-    type Reducer m dc = Fields dc m -> App m dc
-
-    ex2 :: Reducer Len (G.Even a)
-    ex2 (G.Even _ i) = 1 + i 
-
-Since @App@ is a type family, it's not necessarily injective. @LengthM@
-demonstrates where injectivity would not be desirable. Indeed, d-rex relies on
-this as discussed in #6 below. Unfortunately, non-injectivity can muddle type
-inference. For example, the inferred type of @G.Even 'c' 3@ involves a type
-variable: @(Num i, App m (T.Even Char) ~ i) => Fields (G.Even Char) m@. We
-provide the function @mediated@ for directly specifying the mediator.
-
-  in module Util
-    mediated :: [qP|m|] -> RM c m -> RM c m
-    mediated = const id
-
-  in module Ex
-    -- inferred ex3 :: Fields (G.Even Char) LengthM
-    ex3 = mediated [qP|LengthM|] $ G.Even 'c' 3
-
-(@qP@ is just a quasiquoter for proxies -- useful for passing types as values.)
-
-The data family @RM@ is indexed by the core representational types. Most of
-these are common to many representation-based generic programming
-libraries. They indeed compromise a closed universe @Core@; that particular
-universe per se is not codified in d-rex, but its closedness is the crux of all
-representational generic programming.
-
-  in module Core
-    type family Rep a
-    data V                            -- void
-    data U = U                        -- unit
-    newtype D a = D a                 -- a dependency
-    newtype R t = R t                 -- a recursive occurrence
-    newtype F f c = F (f c)           -- argument to a *->*
-    newtype FF ff c d = FF (ff c d)   -- arguments to a *->*->*
-    newtype M i c = M c               -- meta information
-
-    newtype N t = N t                 -- a named type (user hook)
-
-    type (:+) = FF Either
-    type (:*) = FF (,)
-    type (:->) = FF (->)
-
-The structure of many constructors' fields, like T.Even can be codified in
-terms of these basic types.
-
-  in module G
-    type Rep (G.Even a) = FF (,) (D a) (R a)
-
-The recursion-mediated types are indexed by these core types. Note that the
-following declarations are in a separate module, so the constructor names don't
-actually clash.
-
-  in module GenericR
-    data family RM c m
-    data instance RM V m
-    data instance RM U m = U
-    newtype instance RM (D a) m = D a
-    newtype instance RM (R t) m = R (App m t)
-    newtype instance RM (F f c) m = F (f (RM c m))
-    newtype instance RM (FF ff c d) m = FF (ff (RM c m) (RM d m))
-    newtype instance RM (M i c) m = M (RM c m)
-
-These just follow the semantics of recusiion-mediated types.
-
-The only core type without an @RM@ instance is @N@. @N@ is crucial to d-rex's
-usability. It is the interface boundary between the d-rex kernel and the user
-datatype. As demonstrated earlier in this section and in section #2, @RM (N -)@
-instances are provided for each fields type. There is also a corresponding
-instance of @Rep@ and @Generic@.
-
-  in module GenericR
-    class Generic a where
-      rep :: RM (N a) m -> RM (Rep a) m
-      obj :: RM (Rep a) m -> RM (N a) m
-
-  in module G
-    instance Generic (G.Even a) where
-      rep ~(G.Even a o) = FF (D a, R o)
-      obj ~(FF (D a, R o))) = G.Even a o
-
-INVARIANT: the RHS of a Rep should never include an @N@. @N@ is just in place
-to delay the representation of a type.
-
-#4 Sets of types
-
-d-rex also uses a universe of types constructed via V, :+, and N to represent
-finite sets (implemented as type-level binary trees) of types. The @Finite@
-type class recognizes the isomorphism between a finite closed universes and a
-set of types.
-
-  in module TypeBTree
-    type family Inhabitants u
-    class Finite u where
-      path :: u t -> Small (Inhabitants u) t
-      tag  :: Small (Inhabitants u) t -> u t
-
-  in module Ex
-    type instance Inhabitants (DCU Lit) = N Int :+ N Char
-
-    type instance Inhabitants (DCU (Either a b)) =
-      N (G.Left a b) :+ N (G.Right a b)
-
-    type instance Inhabitants (DCU (T.Even a)) =
-      N (G.Zero a) :+ N (G.Even a)
-
-@Inhabitants@/@Finite@ recognizes @V@, @:+@, and @N@ as the closed
-representational core of finite closed universes in the same way that
-@Rep@/@Generic@ encode isomorphisms between the full ensemble of core types and
-the large set of Haskell types they can represent.
-
-#5 Other Universes
-
-Exists, Small, All, MFun, MMap ...
-
-#6 Tag-Gist equivalence and Conversions
-
-...
+See the documentation at http://code.google.com/p/yoko
diff --git a/Type/Yoko/BTree.hs b/Type/Yoko/BTree.hs
--- a/Type/Yoko/BTree.hs
+++ b/Type/Yoko/BTree.hs
@@ -40,7 +40,7 @@
 
 type instance Pred (Uni ts) t = Elem t ts
 
-instance (ts ::: TSum) => EqT (Uni ts) where
+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
@@ -64,24 +64,27 @@
 primUni (Uni u) = w u where
   w :: Inu t ts -> PrimUni ts t
   w (Here Refl) = Refl
-  w (OnLeft u) = LeftD $ w u
-  w (OnRight v) = RightD $ w v
+  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)) = LeftD $ Uni u
-primUni1 (Uni (OnRight v)) = RightD $ Uni v
+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 (Inhabitants u ::: TSum) => Finite u where
+class Finite u where
   toUni :: u t -> Uni (Inhabitants u) t
 
--- | @fromUni@ sometimes requires a stronger context than does @toUni@, so we
+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 fromUni :: Uni (Inhabitants u) t -> u t
+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
@@ -89,11 +92,27 @@
 eqTFin x y = eqT (toUni x) (toUni y)
 
 type instance Inhabitants (Uni ts) = ts
-instance (ts ::: TSum) => Finite (Uni ts) where toUni = id
-instance Finite (Uni ts) => Etinif (Uni ts) where fromUni = id
+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
@@ -139,21 +158,21 @@
 
 
 -- | @each@ is the principal means of defining an @Each@ value.
-each :: forall u ts f. (ts ::: All u) => [qP|u :: *->*|] ->
-        (forall a. u a -> Unwrap f a) -> Each ts f
-each _ = \fs -> w inhabits fs where
+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 ts f. (Wrapper f, ts ::: All u) => [qP|u :: *->*|] ->
-         (forall a. u a -> f a) -> Each ts f
+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 ts. (Wrapper f, ts ::: All NoneD) => (forall a. f a) -> Each ts f
-eachF_ f = eachF Proxy ((\NoneD -> f) :: forall a. NoneD a -> f a)
+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)
 
 
 
diff --git a/Type/Yoko/Fun.hs b/Type/Yoko/Fun.hs
--- a/Type/Yoko/Fun.hs
+++ b/Type/Yoko/Fun.hs
@@ -19,8 +19,8 @@
 -}
 
 module Type.Yoko.Fun
-  (Domain(..), Dom, Rng, applyD, apply,
-   YieldsArrowTSSD, DomF, RngF, eachArrow,
+  (Domain(..), Dom, Rng, applyU, apply,
+   YieldsArrowTSSU, DomF, RngF, eachArrow,
    AsComp(..), WrapComp, WrapCompF
   ) where
 
@@ -45,42 +45,42 @@
 type family Rng (fn :: * -> *) t
 
 -- | @applyD@ is analogous to '$'.
-applyD :: Domain fn t -> fn t -> Dom fn t -> Rng fn t
-applyD (AppBy f) = f
+applyU :: Domain fn t -> fn t -> Dom fn t -> Rng fn t
+applyU (AppBy f) = f
 
--- | @apply = applyD inhabits@.
+-- | @apply = applyU inhabits@.
 apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t
-apply = applyD inhabits
+apply = applyU inhabits
 
 
 
--- | @YieldsArrowTSSD fn@ also gaurantees that @fn@ at @t@ yields a type of the
+-- | @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 YieldsArrowTSSD fn t where
-  YieldsArrowTSSD ::
+data YieldsArrowTSSU fn t where
+  YieldsArrowTSSU ::
     (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
-    ) => Domain fn t -> YieldsArrowTSSD 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 ::: YieldsArrowTSSD fn where inhabits = YieldsArrowTSSD inhabits
+         ) => t ::: YieldsArrowTSSU fn where inhabits = YieldsArrowTSSU inhabits
 
--- | Used by @YieldsArrowTSSD fn@ to structure the domain of @fn@.
+-- | Used by @YieldsArrowTSSU fn@ to structure the domain of @fn@.
 type family DomF (fn :: * -> *) :: * -> *
--- | Used by @YieldsArrowTSSD fn@ to structure the range of @fn@.
+-- | Used by @YieldsArrowTSSU fn@ to structure the range of @fn@.
 type family RngF (fn :: * -> *) :: * -> *
 
--- | Just a specialization: @yieldsArrowTSSD (YieldsArrowTSSD domD) fn = applyD domD fn@.
-yieldsArrowTSSD :: YieldsArrowTSSD fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t
-yieldsArrowTSSD (YieldsArrowTSSD domD) fn = applyD domD 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 (YieldsArrowTSSD fn)
+  (Finite u, Inhabitants u ::: All (YieldsArrowTSSU fn)
   ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))
-eachArrow fn = firstNT toUni $ each [qP|YieldsArrowTSSD fn :: *->*|] $
-  \d -> yieldsArrowTSSD d fn
+eachArrow fn = each [qP|YieldsArrowTSSU fn :: *->*|] $
+  \d -> yieldsArrowTSSU d fn
 
 
 
diff --git a/Type/Yoko/FunA.hs b/Type/Yoko/FunA.hs
--- a/Type/Yoko/FunA.hs
+++ b/Type/Yoko/FunA.hs
@@ -17,7 +17,7 @@
 -}
 
 module Type.Yoko.FunA
-  (Idiom, DomainA(..), applyA, applyAD) where
+  (Idiom, DomainA(..), applyA, applyAU) where
 
 import Type.Yoko.Fun
 import Type.Yoko.Universe
@@ -30,7 +30,7 @@
 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 = applyAD inhabits
+applyA = applyAU inhabits
 
-applyAD :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)
-applyAD (AppABy f) = f
+applyAU :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)
+applyAU (AppABy f) = f
diff --git a/Type/Yoko/Natural.hs b/Type/Yoko/Natural.hs
--- a/Type/Yoko/Natural.hs
+++ b/Type/Yoko/Natural.hs
@@ -43,8 +43,8 @@
 -- 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
-  LeftD  u -> f u
-  RightD v -> g v
+  LeftU  u -> f u
+  RightU v -> g v
 
 
 constNT :: Unwrap f t -> NT ((:=:) t) f
diff --git a/Type/Yoko/Sum.hs b/Type/Yoko/Sum.hs
--- a/Type/Yoko/Sum.hs
+++ b/Type/Yoko/Sum.hs
@@ -46,8 +46,8 @@
 instance (c ::: All u, d ::: All u) => (c :+ d) ::: All u where
   inhabits = SumS inhabits inhabits
 
--- | @All 'NoneD'@ is satisfied by any type-sum.
-type TSum = All NoneD
+-- | @All 'NoneU'@ is satisfied by any type-sum.
+type TSum = All NoneU
 
 
 
diff --git a/Type/Yoko/Universe.hs b/Type/Yoko/Universe.hs
--- a/Type/Yoko/Universe.hs
+++ b/Type/Yoko/Universe.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,
   FlexibleContexts, ScopedTypeVariables, FlexibleInstances,
-  UndecidableInstances, GADTs, Rank2Types #-}
+  UndecidableInstances, GADTs, Rank2Types, EmptyDataDecls #-}
 
 {- |
 
@@ -44,13 +44,13 @@
 
 
 -- | The universe of all types; it has /no/ contraints.
-data NoneD a = NoneD
-instance a ::: NoneD where inhabits = NoneD
+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) => {fstD :: u a, sndD :: v a} -> (u :&& v) a
+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
 
@@ -58,21 +58,21 @@
 
 
 
-instance (a ~ b) => b ::: ((:=:) a) where inhabits = Refl
+instance (a ~ b) => b ::: (:=:) a where inhabits = Refl
 
 
 infixr 2 :||
 -- | Universe sum.
 data (u :|| v) a where
-  LeftD  :: u a -> (u :|| v) a
-  RightD :: v a -> (u :|| v) a
+  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 $ LeftD inhabits
+  inhabits = Anno $ LeftU inhabits
 instance (False ~ Pred u a, a ::: v) => a ::: u :|| v :? False where
-  inhabits = Anno $ RightD inhabits
+  inhabits = Anno $ RightU inhabits
 
 
 type instance Pred (u :|| v) t = Or (Pred u t) (Pred v t)
@@ -80,7 +80,7 @@
 
 
 -- | The empty universe.
-data VoidU t = VoidU -- the empty universe
+data VoidU t -- the empty universe
 
 
 
diff --git a/yoko.cabal b/yoko.cabal
--- a/yoko.cabal
+++ b/yoko.cabal
@@ -1,5 +1,5 @@
 name: yoko
-version: 0.1
+version: 0.2
 synopsis: generic programming with disbanded constructors 
 
 description: @yoko@ views a nominal datatype as a /band/ of constructors, each
@@ -29,7 +29,7 @@
   constructor, say @John@, to be used independently of its original range type
   and sibling constructors.
   .
-  As a generic programming library, @yoko@ extends @intant-generics@ with
+  As a generic programming library, @yoko@ extends @instant-generics@ with
   support for constructor-centric generic programming. The @Examples/LL.hs@
   file distributed with the @yoko@ source demonstrates defining a
   lambda-lifting conversion between the two types @Inner@, which has lambdas,
@@ -54,6 +54,8 @@
   .
   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.
 
 category: Generics, Reflection
 
@@ -66,7 +68,7 @@
 build-type: Simple
 cabal-version: >= 1.6
 
-extra-source-files: README, Examples/*.hs
+extra-source-files: README, CHANGES, Examples/*.hs
 
 
 
@@ -98,7 +100,7 @@
                    Data.Yoko.Reflect,
                    Data.Yoko.InDT,
                    Data.Yoko.Reduce,
-                   Data.Yoko.Algebra
+                   Data.Yoko.Cata
 
 --                   Examples.TermBase,
 --                   Examples.TermGeneric,