diff --git a/Data/Yoko.hs b/Data/Yoko.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko.hs
@@ -0,0 +1,19 @@
+{- |
+
+Module      :  Data.Yoko
+Copyright   :  (c) The University of Kansas 2011
+License     :  BSD3
+
+Maintainer  :  nicolas.frisby@gmail.com
+Stability   :  experimental
+Portability :  see LANGUAGE pragmas (... GHC)
+
+-}
+module Data.Yoko
+  (module Type.Yoko, module Data.Yoko.Generic, module Data.Yoko.Reflect, module Data.Yoko.InDT
+  ) where
+
+import Type.Yoko
+import Data.Yoko.Generic
+import Data.Yoko.Reflect
+import Data.Yoko.InDT
diff --git a/Data/Yoko/Algebra.hs b/Data/Yoko/Algebra.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Algebra.hs
@@ -0,0 +1,86 @@
+{-# 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/Core.hs b/Data/Yoko/Core.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Core.hs
@@ -0,0 +1,83 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/CoreTypes.hs
@@ -0,0 +1,17 @@
+{- |
+
+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/Generic.hs b/Data/Yoko/Generic.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Generic.hs
@@ -0,0 +1,156 @@
+{-# 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/InDT.hs b/Data/Yoko/InDT.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/InDT.hs
@@ -0,0 +1,78 @@
+{-# 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 @HasTagRepDCD 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
+instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)
+         ) => t ::: HasTagRepDCD tag c where inhabits = HasTagRepDCD inhabits
+
+-- | Given @HasTagRepDCD 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
+  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 HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc))
+
+-- | A constructor type @dc@ inhabits @ImageHasTagRepDCD 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
+
+-- | Given @ImageInDTD 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
+
+-- | 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
+         ) => dc ::: ImageInDTDA t fn where
+  inhabits = ImageInDTDA inhabits
+
+imageInDTAD :: 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
diff --git a/Data/Yoko/Reduce.hs b/Data/Yoko/Reduce.hs
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Reduce.hs
@@ -0,0 +1,54 @@
+{-# 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)
+
+Reduction of a band of constructors into a mediation of their range.
+
+-}
+module Data.Yoko.Reduce (AnRMNUni, Reduce(..), ReduceDC(..)) where
+
+import Type.Yoko
+
+import Data.Yoko.Generic
+import Data.Yoko.Reflect
+
+
+
+type AnRMNUni m ts = AnRMN m (Uni ts)
+
+
+
+-- | @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)
+
+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
+
+-- | @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)
+
+
+
+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
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/Reflect.hs
@@ -0,0 +1,103 @@
+{-# 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
+
+
+
+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)
+
+
+
+
+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 (DCU 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
+
+
+
+
+{- | 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
new file mode 100644
--- /dev/null
+++ b/Data/Yoko/ReflectBase.hs
@@ -0,0 +1,106 @@
+{-# 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 :: DCU (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
+    _ -> 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)
+
+-- | @UniqueDC@ is for newtypes and GADT constructors where the type @dc@
+-- determines the constructor.
+class UniqueDC dc where uniqueTo :: Range dc -> RMNI dc
+
+
+
+
+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 (DCOf 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 (DCU 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)
+      ) => 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.
+  data DCU t :: * -> * -- universe of constructor types
+
+  -- | /Disband/ this type into one of its data constructors.
+  disband :: t -> Disbanded IdM t
diff --git a/Examples/InnerBase.hs b/Examples/InnerBase.hs
new file mode 100644
--- /dev/null
+++ b/Examples/InnerBase.hs
@@ -0,0 +1,8 @@
+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
new file mode 100644
--- /dev/null
+++ b/Examples/InnerGeneric.hs
@@ -0,0 +1,90 @@
+{-# 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
+  fromUni (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
+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
new file mode 100644
--- /dev/null
+++ b/Examples/LL.hs
@@ -0,0 +1,63 @@
+{-# 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 $ imageInDTAD LL
+--  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAD 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
new file mode 100644
--- /dev/null
+++ b/Examples/LL0.hs
@@ -0,0 +1,57 @@
+
+
+
+
+
+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
new file mode 100644
--- /dev/null
+++ b/Examples/LLBase.hs
@@ -0,0 +1,13 @@
+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
new file mode 100644
--- /dev/null
+++ b/Examples/LLBasics.hs
@@ -0,0 +1,71 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Examples/LLDirect.hs
@@ -0,0 +1,81 @@
+{- |
+
+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
new file mode 100644
--- /dev/null
+++ b/Examples/LLGeneric.hs
@@ -0,0 +1,89 @@
+{-# 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
+  fromUni (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
+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
new file mode 100644
--- /dev/null
+++ b/Examples/Main.hs
@@ -0,0 +1,25 @@
+{- |
+
+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
new file mode 100644
--- /dev/null
+++ b/Examples/ReflectAux.hs
@@ -0,0 +1,18 @@
+{- |
+
+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) where
+
+import Type.Serialize
+
+import Data.Yoko hiding (qK)
diff --git a/Examples/TermBase.hs b/Examples/TermBase.hs
new file mode 100644
--- /dev/null
+++ b/Examples/TermBase.hs
@@ -0,0 +1,24 @@
+{- |
+
+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
new file mode 100644
--- /dev/null
+++ b/Examples/TermGeneric.hs
@@ -0,0 +1,191 @@
+{-# 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
+  fromUni (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
+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
+  fromUni (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
+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 . uniqueTo; 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"
+  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
+  fromUni (Uni (Here Refl)) = Decl_
+instance (t ::: Uni (DCs B.Decl)) => t ::: DCU B.Decl where
+  inhabits = fromUni 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
new file mode 100644
--- /dev/null
+++ b/Examples/TermInner.hs
@@ -0,0 +1,60 @@
+{-# 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 $ imageInDTD 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
new file mode 100644
--- /dev/null
+++ b/Examples/TermTest.hs
@@ -0,0 +1,82 @@
+{-# 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.Algebra".
+
+-}
+module Examples.TermTest where
+
+import Examples.TermBase
+import qualified Examples.TermGeneric as G
+
+import Type.Yoko
+import Data.Yoko.Algebra
+
+
+-- | 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 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 ReduceDC SemM G.Decl where reduceDC = eDecl
+
+eval x = ($ x) $ cata $ algebras [qP|SemM|]
+
+-- NB equivalent
+eval' x = ($ x) $ cata $ (reduce .|. reduce) -- :: AlgebraFam 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/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,1 @@
+BSD3
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,249 @@
+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
+
+...
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/Type/Yoko.hs b/Type/Yoko.hs
new file mode 100644
--- /dev/null
+++ b/Type/Yoko.hs
@@ -0,0 +1,36 @@
+{- |
+
+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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/BTree.hs
@@ -0,0 +1,175 @@
+{-# 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 (ts ::: TSum) => 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) = LeftD $ w u
+  w (OnRight v) = RightD $ 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
+
+
+
+
+-- | Finite universes can be represented as type-sums.
+type family Inhabitants u
+class (Inhabitants u ::: TSum) => Finite u where
+  toUni :: u t -> Uni (Inhabitants u) t
+
+-- | @fromUni@ 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
+
+-- | 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 (ts ::: TSum) => Finite (Uni ts) where toUni = id
+instance Finite (Uni ts) => Etinif (Uni ts) where fromUni = id
+
+
+
+-- | @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 ts f. (ts ::: All u) => [qP|u :: *->*|] ->
+        (forall a. u a -> Unwrap f a) -> Each ts f
+each _ = \fs -> 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 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)
+
+
+
+-- | 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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/Fun.hs
@@ -0,0 +1,136 @@
+{-# 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, applyD, apply,
+   YieldsArrowTSSD, 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 '$'.
+applyD :: Domain fn t -> fn t -> Dom fn t -> Rng fn t
+applyD (AppBy f) = f
+
+-- | @apply = applyD inhabits@.
+apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t
+apply = applyD inhabits
+
+
+
+-- | @YieldsArrowTSSD 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 ::
+    (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t
+    ) => Domain fn t -> YieldsArrowTSSD 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
+
+-- | Used by @YieldsArrowTSSD fn@ to structure the domain of @fn@.
+type family DomF (fn :: * -> *) :: * -> *
+-- | Used by @YieldsArrowTSSD 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
+
+-- | 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)
+  ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))
+eachArrow fn = firstNT toUni $ each [qP|YieldsArrowTSSD fn :: *->*|] $
+  \d -> yieldsArrowTSSD 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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/FunA.hs
@@ -0,0 +1,36 @@
+{-# 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, applyAD) 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 = applyAD inhabits
+
+applyAD :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)
+applyAD (AppABy f) = f
diff --git a/Type/Yoko/MFun.hs b/Type/Yoko/MFun.hs
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/MFun.hs
@@ -0,0 +1,97 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/Natural.hs
@@ -0,0 +1,82 @@
+{-# 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
+  LeftD  u -> f u
+  RightD 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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/Sum.hs
@@ -0,0 +1,102 @@
+{-# 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 'NoneD'@ is satisfied by any type-sum.
+type TSum = All NoneD
+
+
+
+
+
+-- | 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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/TFunA.hs
@@ -0,0 +1,110 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/TSTSS.hs
@@ -0,0 +1,29 @@
+{- |
+
+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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/Type.hs
@@ -0,0 +1,84 @@
+{-# 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
new file mode 100644
--- /dev/null
+++ b/Type/Yoko/Universe.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,
+  FlexibleContexts, ScopedTypeVariables, FlexibleInstances,
+  UndecidableInstances, GADTs, Rank2Types #-}
+
+{- |
+
+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 NoneD a = NoneD
+instance a ::: NoneD where inhabits = NoneD
+
+type Both = (:&&)
+infixr 3 :&&
+-- | Universe product.
+data (u :&& v) a where (:&&) :: (a ::: u, a ::: v) => {fstD :: u a, sndD :: 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
+  LeftD  :: u a -> (u :|| v) a
+  RightD :: 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
+instance (False ~ Pred u a, a ::: v) => a ::: u :|| v :? False where
+  inhabits = Anno $ RightD inhabits
+
+
+type instance Pred (u :|| v) t = Or (Pred u t) (Pred v t)
+
+
+
+-- | The empty universe.
+data VoidU t = VoidU -- the empty universe
+
+
+
+instance (f t ::: u) => t ::: (u :. f) where inhabits = Compose inhabits
diff --git a/yoko.cabal b/yoko.cabal
new file mode 100644
--- /dev/null
+++ b/yoko.cabal
@@ -0,0 +1,107 @@
+name: yoko
+version: 0.1
+synopsis: generic programming with disbanded constructors 
+
+description: @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
+  programming to enrich its @instant-generics@ foundation with capabilities
+  derived from the constructor-centric perspective.
+  .
+  For example, consider the following /nominal datatype/.
+  .
+  @
+    data Beatles = John ... | Paul ... | George ... | Ringo ...
+  @
+  .
+  This type can of course be understood as a sum of the individual
+  /constructor types/.
+  .
+  @
+    data John = John ...
+    data Paul = Paul ...
+    data George = George ...
+    data Ringo = Ringo ...
+  @
+  .
+  @yoko@'s conceptual foundations start there. In particular, this allows a
+  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
+  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,
+  and @Prog@, which has top-level function declarations instead.
+  .
+  @
+    data Inner = Lam Type Inner | Var Int | App Inner Inner
+  .
+    data Term = Var Int | App Term Term | DVar Int
+    data Prog = Prog ([Type], Type, Term) Term
+  @
+  .
+  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
+  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
+  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.
+
+category: Generics, Reflection
+
+license: BSD3
+license-file: LICENSE
+author: Nicolas Frisby <nicolas.frisby@gmail.com>
+maintainer: Nicolas Frisby <nicolas.frisby@gmail.com>
+stability: experimental
+
+build-type: Simple
+cabal-version: >= 1.6
+
+extra-source-files: README, Examples/*.hs
+
+
+
+library
+  build-depends: base >= 4 && < 5
+  build-depends: type-equality < 0.2, tagged >= 0.2 && < 0.3
+
+  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,
+
+                   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.Algebra
+
+--                   Examples.TermBase,
+--                   Examples.TermGeneric,
+--                   Examples.InnerBase,
+--                   Examples.InnerGeneric,
+--                   Examples.TermInner