diff --git a/category-extras.cabal b/category-extras.cabal
--- a/category-extras.cabal
+++ b/category-extras.cabal
@@ -1,6 +1,6 @@
 name:                   category-extras
 category:               Control, Monads, Comonads
-version:                0.52.1
+version:                0.52.3
 license:                BSD3
 cabal-version:          >= 1.2
 license-file:           LICENSE
@@ -15,8 +15,7 @@
 description:            A vastly expanded collection of modules implementing various
                         ideas from category theory. Notable bits include: comonads,
                         adjunctions, functor fixedpoints and various recursion
-                        operaters ala /Functional Programming with Bananas, Lenses,
-                        Envelopes and Barbed Wire/.
+                        operaters ala /Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire/.
 build-type:             Simple
 
 flag ArrowSubclassesCategory
@@ -46,6 +45,9 @@
                 ExistentialQuantification,
                 Rank2Types
 
+        other-modules:
+                Control.Functor.Internal.Adjunction,
+                Control.Functor.Internal.Ideal
 
         exposed-modules:
                 Control.Category.Monoidal,
@@ -56,6 +58,7 @@
                 Control.Arrow.CoKleisli,
                 Control.Category.Associative,
                 Control.Category.Braided,
+                Control.Category.Discrete,
                 Control.Category.Distributive,
                 Control.Category.Dual,
                 Control.Category.Hask,
diff --git a/src/Control/Arrow/BiKleisli.hs b/src/Control/Arrow/BiKleisli.hs
--- a/src/Control/Arrow/BiKleisli.hs
+++ b/src/Control/Arrow/BiKleisli.hs
@@ -15,10 +15,8 @@
 	( BiKleisli(..)
 	) where
 
-#if __GLASGOW_HASKELL__ >= 609
 import Prelude hiding (id,(.))
 import Control.Category
-#endif
 import Control.Monad (liftM)
 import Control.Comonad
 import Control.Arrow
@@ -34,10 +32,10 @@
 	first (BiKleisli f) = BiKleisli $ \x -> do
 		u <- f (fmap fst x)
 		return (u, extract (fmap snd x))
-#if __GLASGOW_HASKELL__ >= 609
+#if __GLASGOW_HASKELL__ < 609
+	BiKleisli g >>> BiKleisli f = BiKleisli ((>>= f) . dist . extend g)
+#endif
+
 instance (Comonad w, Monad m, Distributes w m) => Category (BiKleisli w m) where
 	BiKleisli f . BiKleisli g = BiKleisli ((>>=f) . dist . extend g)
 	id = BiKleisli (return . extract)
-#else
-	BiKleisli g >>> BiKleisli f = BiKleisli ((>>= f) . dist . extend g)
-#endif
diff --git a/src/Control/Arrow/CoKleisli.hs b/src/Control/Arrow/CoKleisli.hs
--- a/src/Control/Arrow/CoKleisli.hs
+++ b/src/Control/Arrow/CoKleisli.hs
@@ -16,10 +16,8 @@
 	) where
 
 
-#if __GLASGOW_HASKELL__ >= 609
 import Prelude hiding (id,(.))
 import Control.Category
-#endif
 import Control.Comonad
 import Control.Arrow
 
@@ -34,11 +32,10 @@
 	CoKleisli a *** CoKleisli b = CoKleisli (a . fmap fst &&& b . fmap snd)
 	first a = a *** CoKleisli extract
 	second a = CoKleisli extract *** a
-#if __GLASGOW_HASKELL__ >= 609
-instance Comonad w => Category (CoKleisli w) where
-	id = CoKleisli extract
-	CoKleisli b . CoKleisli a = CoKleisli (b . fmap a . duplicate)
-#else
+#if __GLASGOW_HASKELL__ < 609
 	CoKleisli a >>> CoKleisli b = CoKleisli (b . fmap a . duplicate)
 #endif
 
+instance Comonad w => Category (CoKleisli w) where
+	id = CoKleisli extract
+	CoKleisli b . CoKleisli a = CoKleisli (b . fmap a . duplicate)
diff --git a/src/Control/Category/Cartesian/Closed.hs b/src/Control/Category/Cartesian/Closed.hs
--- a/src/Control/Category/Cartesian/Closed.hs
+++ b/src/Control/Category/Cartesian/Closed.hs
@@ -10,7 +10,7 @@
 -- Portability	: non-portable (class-associated types)
 --
 -- NB: Some rewrite rules are disabled pending resolution of:
--- <http://hachomage.hashomell.org/trac/ghc/tichomet/2291>
+-- <http://hackage.haskell.org/trac/ghc/ticket/2291>
 -------------------------------------------------------------------------------------------
 module Control.Category.Cartesian.Closed
 	( 
diff --git a/src/Control/Category/Discrete.hs b/src/Control/Category/Discrete.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Category/Discrete.hs
@@ -0,0 +1,27 @@
+{-# LANGUAGE GADTs #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	: Control.Category.Discrete
+-- Copyright 	: 2008 Edward Kmett
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: portable
+--
+-------------------------------------------------------------------------------------------
+module Control.Category.Discrete
+	( Discrete(Refl)
+	) where
+
+import Prelude hiding (id,(.))
+import Control.Category
+
+data Discrete a b where 
+	Refl :: Discrete a a
+
+instance Category Discrete where
+	id = Refl
+	Refl . Refl = Refl
+
+-- HasTerminalObject _|_ ?
diff --git a/src/Control/Comonad/Coideal.hs b/src/Control/Comonad/Coideal.hs
--- a/src/Control/Comonad/Coideal.hs
+++ b/src/Control/Comonad/Coideal.hs
@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
 -----------------------------------------------------------------------------
 -- |
 -- Module      :  Control.Comonad.Coideal
@@ -10,8 +11,16 @@
 --
 ----------------------------------------------------------------------------
 module Control.Comonad.Coideal
-	( module Control.Monad.Ideal
+	( 
+	-- * Coideal Comonads
+	  ComonadCoideal(..)
+	, Coideal
+	, coideal
+	, buildCoideal
+	-- * Mutual recursion for (co)ideal (co)monad (co)products
+	, Mutual(..)
+	-- * Coideal Comonad Product
+	, (:*)
 	) where
 
-import Control.Monad.Ideal
-
+import Control.Functor.Internal.Ideal
diff --git a/src/Control/Functor/Adjunction.hs b/src/Control/Functor/Adjunction.hs
--- a/src/Control/Functor/Adjunction.hs
+++ b/src/Control/Functor/Adjunction.hs
@@ -14,81 +14,8 @@
 module Control.Functor.Adjunction 
 	( Adjunction (unit, counit, leftAdjunct, rightAdjunct)
 	, ACompF(ACompF)
+	-- * Every Right Adjoint is Representable 
+	, repAdjunction, unrepAdjunction
 	) where
 
-import Control.Functor.Composition
-import Control.Functor.Exponential
-import Control.Functor.Full
-import Control.Functor.HigherOrder
-import Control.Applicative
-import Control.Monad.Reader
-import Control.Monad.State
-import Control.Monad.Identity
-import Control.Comonad.Reader
-import Control.Comonad.Context
-
--- | An 'Adjunction' formed by the 'Functor' f and 'Functor' g. 
-
--- Minimal definition:
-
--- 1. @leftAdjunct@ and @rightAdjunct@ 
-
--- 2. @unit@ and @counit@
-
-class (Functor f, Functor g) => Adjunction f g | f -> g, g -> f where
-	unit   :: a -> g (f a)
-	counit :: f (g a) -> a
-	leftAdjunct  :: (f a -> b) -> a -> g b
-	rightAdjunct :: (a -> g b) -> f a -> b
-
-	unit = leftAdjunct id
-	counit = rightAdjunct id
-	leftAdjunct f = fmap f . unit
-	rightAdjunct f = counit . fmap f
-
-instance (Adjunction f1 g1, Adjunction f2 g2) => Adjunction (CompF f2 f1) (CompF g1 g2) where
-	counit = counit . fmap (counit . fmap decompose) . decompose
-	unit = compose . fmap (fmap compose . unit) . unit
-
-
--- | Adjunction-oriented composition, yields monads and comonads from adjunctions
-newtype ACompF f g a = ACompF (CompF f g a) deriving (Functor, ExpFunctor, Full, Composition, HFunctor)
-
-instance Adjunction f g => Pointed (ACompF g f) where
-        point = compose . unit
-
-instance Adjunction f g => Copointed (ACompF f g) where
-        extract = counit . decompose
-
-instance Adjunction f g => Applicative (ACompF g f) where
-	pure = point
-	(<*>) = ap
-
-instance Adjunction f g => Monad (ACompF g f) where
-        return = point
-        m >>= f = compose . fmap (rightAdjunct (decompose . f)) $ decompose m
-
-instance Adjunction f g => Comonad (ACompF f g) where
-        extend f = compose . fmap (leftAdjunct (f . compose)) . decompose
-
-instance Adjunction ((,)e) ((->)e) where
-	leftAdjunct f a e  = f (e,a)
-	rightAdjunct f ~(e,a) = f a e
-	unit a e = (e,a)
-	counit (x,f) = f x
-
-instance Adjunction Identity Identity where
-	unit = Identity . Identity
-	counit = runIdentity . runIdentity 
-
-instance Adjunction (Coreader e) (Reader e) where
-	unit a = Reader (\e -> Coreader e a)
-	counit (Coreader x f) = runReader f x
-
-instance ComonadContext e ((,)e `ACompF` (->)e) where
-	getC = fst . decompose
-	modifyC f = uncurry (flip id . f) . decompose
-
-instance MonadState e ((->)e `ACompF` (,)e) where
-	get = compose $ \s -> (s,s)
-	put s = compose $ const (s,())
+import Control.Functor.Internal.Adjunction
diff --git a/src/Control/Functor/Full.hs b/src/Control/Functor/Full.hs
--- a/src/Control/Functor/Full.hs
+++ b/src/Control/Functor/Full.hs
@@ -12,6 +12,7 @@
 
 module Control.Functor.Full where
 
+import Control.Monad.Identity
 
 {- |
 	A 'Full' 'Functor' @F : C -> D@ provides for every pair of objects @c@, @c'@ in @C@
@@ -23,12 +24,15 @@
 
 class Functor f => Full f where
 	premap :: (f a -> f b) -> a -> b
+instance Full Identity where
+	premap f = runIdentity . f . Identity
 	
 {-# RULES
 	"fmap/premap" 	map . premap = id
  #-}
 
 class Functor f => Faithful f
+instance Faithful Identity 
 
 {- | 
 
diff --git a/src/Control/Functor/Internal/Adjunction.hs b/src/Control/Functor/Internal/Adjunction.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Functor/Internal/Adjunction.hs
@@ -0,0 +1,240 @@
+{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
+-------------------------------------------------------------------------------------------
+-- |
+-- Module	: Control.Functor.Internal.Adjunction
+-- Copyright 	: 2008 Edward Kmett
+-- License	: BSD
+--
+-- Maintainer	: Edward Kmett <ekmett@gmail.com>
+-- Stability	: experimental
+-- Portability	: non-portable (functional-dependencies)
+--
+-------------------------------------------------------------------------------------------
+
+module Control.Functor.Internal.Adjunction 
+	( 
+	-- * Adjunction
+	  Adjunction (unit, counit, leftAdjunct, rightAdjunct)
+	, ACompF(ACompF)
+	, repAdjunction, unrepAdjunction
+	-- * Representability
+	, Representable, rep, unrep
+	, Corepresentable, corep, uncorep
+	, Both(..), EitherF(..)
+	-- * Zapping
+	, Zap(..), (>$<)
+	, Bizap(..), (>>$<<)
+	) where
+
+import Control.Comonad.Reader
+import Control.Comonad.Context
+import Control.Functor.Combinators.Biff
+import Control.Functor.Contra
+import Control.Functor.Composition
+import Control.Functor.Exponential
+import Control.Functor.Full
+import Control.Functor.Strong
+import Control.Functor.HigherOrder
+import Control.Applicative
+import Control.Monad.Either ()
+import Control.Monad.Identity
+import Control.Monad.Reader
+import Control.Monad.State
+
+-- | An 'Adjunction' formed by the 'Functor' f and 'Functor' g. 
+
+-- Minimal definition:
+
+-- 1. @leftAdjunct@ and @rightAdjunct@ 
+
+-- 2. @unit@ and @counit@
+
+-- The following ambiguous instances prevent the requirement that (Zap f g, Zap g f) be 
+-- a prerequisite for Adjunction:
+
+-- instance (Adjunction f1 g1, Adjunction f2 g2) => Zap (CompF g1 g2) (CompF f2 f1) where ...
+-- instance (Adjunction f1 g1, Adjunction f2 g2) => Zap (CompF f2 f1) (CompF g1 g2) where ...
+-- instance (Zap f g, Zap f' g') => Zap (CompF f f') (Comp g g')
+--	zapWith f a b = zapWith (zapWith f) (decompose a) (decompose b)
+-- instance (Zap f g, Zap g f, Representable g (f ()), Functor f) => Adjunction f g | f -> g, g -> f where
+class (Representable g (f ()), Functor f) => Adjunction f g | f -> g, g -> f where
+	unit   :: a -> g (f a)
+	counit :: f (g a) -> a
+	leftAdjunct  :: (f a -> b) -> a -> g b
+	rightAdjunct :: (a -> g b) -> f a -> b
+
+	unit = leftAdjunct id
+	counit = rightAdjunct id
+	leftAdjunct f = fmap f . unit
+	rightAdjunct f = counit . fmap f
+
+zapWithGF :: Adjunction g f => (a -> b -> c) -> f a -> g b -> c
+zapWithGF f a b = uncurry (flip f) . counit . fmap (uncurry (flip strength)) $ strength a b
+
+-- more appropriate to use 'data Empty' or a (co)limit to ground out f ?
+repAdjunction :: Adjunction f g => (f () -> a) -> g a
+repAdjunction f = leftAdjunct f ()
+
+unrepAdjunction :: Adjunction f g => g a -> (f () -> a)
+unrepAdjunction = rightAdjunct . const
+
+-- TODO: widen?
+instance (Adjunction f1 g1, Adjunction f2 g2) => Representable (CompF g1 g2) (CompF f2 f1 ()) where
+	rep = repAdjunction
+	unrep = unrepAdjunction
+
+instance (Adjunction f1 g1, Adjunction f2 g2) => Adjunction (CompF f2 f1) (CompF g1 g2) where
+	counit = counit . fmap (counit . fmap decompose) . decompose
+	unit = compose . fmap (fmap compose . unit) . unit
+
+-- | Adjunction-oriented composition, yields monads and comonads from adjunctions
+newtype ACompF f g a = ACompF (CompF f g a) deriving (Functor, ExpFunctor, Full, Composition, HFunctor)
+
+instance Adjunction f g => Pointed (ACompF g f) where
+        point = compose . unit
+
+instance Adjunction f g => Copointed (ACompF f g) where
+        extract = counit . decompose
+
+instance Adjunction f g => Applicative (ACompF g f) where
+	pure = point
+	(<*>) = ap
+
+instance Adjunction f g => Monad (ACompF g f) where
+        return = point
+        m >>= f = compose . fmap (rightAdjunct (decompose . f)) $ decompose m
+
+instance Adjunction f g => Comonad (ACompF f g) where
+        extend f = compose . fmap (leftAdjunct (f . compose)) . decompose
+
+instance Zap ((->)e) ((,)e) where
+	zapWith = zapWithGF
+
+instance Representable ((->)e) (e,()) where
+	rep = repAdjunction
+	unrep = unrepAdjunction
+
+instance Representable ((->)e) e where
+	rep = id
+	unrep = id
+
+instance Adjunction ((,)e) ((->)e) where
+	leftAdjunct f a e  = f (e,a)
+	rightAdjunct f ~(e,a) = f a e
+	unit a e = (e,a)
+	counit (x,f) = f x
+
+instance Representable Identity (Identity ()) where
+	rep = repAdjunction
+	unrep = unrepAdjunction
+
+instance Adjunction Identity Identity where
+	unit = Identity . Identity
+	counit = runIdentity . runIdentity 
+
+instance Zap (Reader e) (Coreader e) where
+	zapWith = zapWithGF
+
+instance Representable (Reader e) (Coreader e ()) where
+	rep = repAdjunction
+	unrep = unrepAdjunction
+
+instance Adjunction (Coreader e) (Reader e) where
+	unit a = Reader (\e -> Coreader e a)
+	counit (Coreader x f) = runReader f x
+
+instance ComonadContext e ((,)e `ACompF` (->)e) where
+	getC = fst . decompose
+	modifyC f = uncurry (flip id . f) . decompose
+
+instance MonadState e ((->)e `ACompF` (,)e) where
+	get = compose $ \s -> (s,s)
+	put s = compose $ const (s,())
+class ContraFunctor f => Corepresentable f x where
+	corep :: (a -> x) -> f a 
+	uncorep :: f a -> (a -> x)
+
+class Functor f => Representable f x where
+	rep :: (x -> a) -> f a
+	unrep :: f a -> (x -> a)
+
+{-# RULES
+"rep/unrep" rep . unrep = id
+"unrep/rep" unrep . rep = id
+"corep/uncorep" corep . uncorep = id
+"uncorep/corep" unrep . corep = id
+ #-}
+
+--repAdjunction :: Adjunction f g => (f () -> a) -> g a
+--repAdjunction f = leftAdjunct f ()
+
+--unrepAdjunction :: Adjunction f g => g a -> (f () -> a)
+--unrepAdjunction = rightAdjunction . const
+
+data EitherF a b c = EitherF (a -> c) (b -> c)
+
+instance Functor (EitherF a b) where
+        fmap f (EitherF l r) = EitherF (f . l) (f . r)
+
+instance Representable (EitherF a b) (Either a b) where
+        rep f = EitherF (f . Left) (f . Right)
+        unrep (EitherF l r) = either l r
+
+instance Representable Identity () where
+	rep f = Identity (f ())
+	unrep (Identity a) = const a
+
+data Both a = Both a a 
+
+instance Functor Both where
+	fmap f (Both a b) = Both (f a) (f b)
+
+instance Representable Both Bool where
+	rep f = Both (f False) (f True)
+	unrep (Both x _) False = x
+	unrep (Both _ y) True = y
+
+-- instance Adjunction f g => Representable g (f ()) where
+-- instance Representable (Cofree Identity) (Free Identity ()) where
+
+
+{- | Minimum definition: zapWith -}
+
+-- zapWith :: Adjunction f g => (a -> b -> c) -> f a -> g b -> c
+-- zapWith f a b = uncurry (flip f) . counit . fmap (uncurry (flip strength)) $ strength a b
+
+-- zap :: Adjunction f g => f (a -> b) -> g a -> b
+-- zap = zapWith id
+
+class Zap f g | f -> g, g -> f where
+	zapWith :: (a -> b -> c) -> f a -> g b -> c
+	zap :: f (a -> b) -> g a -> b
+	zap = zapWith id
+
+(>$<) :: Zap f g => f (a -> b) -> g a -> b
+(>$<) = zap
+
+instance Zap Identity Identity where
+	zapWith f (Identity a) (Identity b) = f a b
+
+{- | Minimum definition: bizapWith -}
+
+class Bizap p q | p -> q, q -> p where
+	bizapWith :: (a -> c -> e) -> (b -> d -> e) -> p a b -> q c d -> e
+
+	bizap :: p (a -> c) (b -> c) -> q a b -> c
+	bizap = bizapWith id id
+
+(>>$<<) :: Bizap p q => p (a -> c) (b -> c) -> q a b -> c
+(>>$<<) = bizap
+
+instance Bizap (,) Either where
+	bizapWith l _ (f,_) (Left a) = l f a
+	bizapWith _ r (_,g) (Right b) = r g b 
+
+instance Bizap Either (,) where
+	bizapWith l _ (Left f) (a,_) = l f a
+	bizapWith _ r (Right g) (_,b) = r g b
+
+instance (Bizap p q, Zap f g, Zap i j) => Bizap (Biff p f i) (Biff q g j) where
+	bizapWith l r fs as = bizapWith (zapWith l) (zapWith r) (runBiff fs) (runBiff as)
diff --git a/src/Control/Functor/Internal/Ideal.hs b/src/Control/Functor/Internal/Ideal.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Functor/Internal/Ideal.hs
@@ -0,0 +1,119 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Functor.Internal.Ideal
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  portable
+--
+----------------------------------------------------------------------------
+module Control.Functor.Internal.Ideal
+	( 
+	-- * Ideal Monads
+	  MonadIdeal(..)
+	, Ideal
+	, ideal
+	, destroyIdeal
+	-- * Coideal Comonads
+	, ComonadCoideal(..)
+	, Coideal
+	, coideal
+	, buildCoideal
+	-- * Mutual recursion for (co)ideal (co)monad (co)products
+	, Mutual(..)
+	-- * Coideal Comonad Product
+	, (:*)
+	-- * Ideal Monad Coproduct
+	, (:+)
+	) where
+
+import Prelude hiding (fst, snd)
+import Control.Category.Cartesian 
+import Control.Category.Hask
+import Control.Comonad
+import Control.Functor
+import Control.Functor.Algebra
+import Control.Functor.Combinators.Lift
+import Control.Monad.Identity
+
+type Ideal = Ap Either 
+-- type Ideal f = Join (PFree f)
+type Coideal = Ap (,)
+-- type Coideal f = Join (PCofree f)
+
+ideal :: Either a (f a) -> Ideal f a
+ideal = mkAp
+
+coideal :: (a, f a) -> Coideal f a 
+coideal = mkAp
+
+runIdeal :: Ideal f a -> Either a (f a)
+runIdeal = runAp
+
+runCoideal :: Coideal f a -> (a, f a)
+runCoideal = runAp
+
+class Functor m => MonadIdeal m where
+	idealize :: m (Either a (m a)) -> m a
+
+instance Functor f => Pointed (Ideal f) where
+	point = Lift . Left . Identity
+
+-- this only really needs 'ap' but there is no 'unpointed/pre- applicative'
+{-
+instance Applicative f => Applicative (Ideal f) where
+	pure = point
+	Ideal (Left f) <*> Ideal (Left a) = Ideal $ Left (f a)
+	Ideal (Left f) <*> Ideal (Right bs) = Ideal $ Right (fmap f bs)
+	Ideal (Right fs) <*> Ideal (Left a) = Ideal $ Right (fmap ($a) fs)
+	Ideal (Right fs) <*> Ideal (Right bs) = Ideal $ Right (fs <*> bs)
+-}
+
+instance MonadIdeal m => Monad (Ideal m) where
+	return = point
+	m >>= f = ideal . (id ||| Right . idealize) . runIdeal $ fmap (runIdeal . f) m
+
+destroyIdeal :: Algebra m a -> Ideal m a -> a
+destroyIdeal phi = (id ||| phi) . runIdeal 
+
+
+-- instance MonadIdeal (Fst k) where
+--	idealize = mkFst . runFst
+
+class Functor w => ComonadCoideal w where
+	coidealize :: w a -> w (a, w a)
+
+instance Functor f => Copointed (Coideal f) where
+	extract = runIdentity . fst . runLift
+
+instance ComonadCoideal w => Comonad (Coideal w) where
+	extend f = fmap (f . coideal) . coideal . (id &&& coidealize . snd) . runCoideal
+
+buildCoideal :: Coalgebra m a -> a -> Coideal m a
+buildCoideal phi = coideal . (id &&& phi)
+
+-- instance ComonadCoideal (Fst k) where
+--	coidealize = mkFst . runFst
+
+-- * (Co)ideal (Co)products
+
+newtype Mutual p m n a = Mutual { runMutual :: m (p a (Mutual p n m a)) } 
+type Mutual' p m n = Lift p (Mutual p m n) (Mutual p n m)
+type (m :+ n) = Mutual' Either m n
+type (m :* n) = Mutual' (,) m n
+
+instance (Bifunctor p Hask Hask Hask, Functor m, Functor n) => Functor (Mutual p m n) where
+	fmap f = Mutual . fmap (bimap f (fmap f)) . runMutual
+
+{-
+instance (MonadIdeal m, MonadIdeal n) => MonadIdeal (m :+ n) where
+	idealize = undefined
+-}
+
+{-
+instance (ComonadCoideal w, ComonadCoideal v) => ComonadCoideal (w :* v) where
+	coidealize = undefined
+-}
diff --git a/src/Control/Functor/Lambek.hs b/src/Control/Functor/Lambek.hs
--- a/src/Control/Functor/Lambek.hs
+++ b/src/Control/Functor/Lambek.hs
@@ -20,7 +20,6 @@
 	) where
 
 import Control.Functor.Algebra 
-import Control.Functor.Extras
 import Control.Functor.Fix
 import Control.Functor.HigherOrder
 import Control.Morphism.Cata
diff --git a/src/Control/Functor/Limit.hs b/src/Control/Functor/Limit.hs
--- a/src/Control/Functor/Limit.hs
+++ b/src/Control/Functor/Limit.hs
@@ -12,9 +12,11 @@
 module Control.Functor.Limit
 	( Limit, HasLimit(limit)
 	, Colimit(..)
+	, liftLimit, liftColimit
 	) where
 
 import Prelude hiding (abs)
+import Control.Functor.Extras
 import Data.Monoid
 
 -- | @type Limit = Ran (Const Void)@
@@ -33,5 +35,11 @@
 instance Monoid a => HasLimit (Either a) where
 	limit = (Left mempty)
 
+liftLimit :: (f :~> g) -> Limit f -> Limit g
+liftLimit f a = f a
+
 -- | @type Colimit = Lan (Const Void)@
 data Colimit f = forall b. Colimit (f b)
+
+liftColimit :: (f :~> g) -> Colimit f -> Colimit g
+liftColimit f (Colimit a) = Colimit (f a)
diff --git a/src/Control/Functor/Representable.hs b/src/Control/Functor/Representable.hs
--- a/src/Control/Functor/Representable.hs
+++ b/src/Control/Functor/Representable.hs
@@ -11,41 +11,10 @@
 --
 -------------------------------------------------------------------------------------------
 
-module Control.Functor.Representable where
-
-import Control.Monad.Identity
-
-class Functor f => Representable f x where
-	rep :: (x -> a) -> f a
-	unrep :: f a -> (x -> a)
-
-{-# RULES
-"rep/unrep" rep . unrep = id
-"unrep/rep" unrep . rep = id
- #-}
-
-data EitherF a b c = EitherF (a -> c) (b -> c)
-
-instance Functor (EitherF a b) where
-        fmap f (EitherF l r) = EitherF (f . l) (f . r)
-
-instance Representable (EitherF a b) (Either a b) where
-        rep f = EitherF (f . Left) (f . Right)
-        unrep (EitherF l r) = either l r
-
-instance Representable Identity () where
-	rep f = Identity (f ())
-	unrep (Identity a) = const a
-
-data Both a = Both a a 
-
-instance Functor Both where
-	fmap f (Both a b) = Both (f a) (f b)
-
-instance Representable Both Bool where
-	rep f = Both (f False) (f True)
-	unrep (Both x _) False = x
-	unrep (Both _ y) True = y
+module Control.Functor.Representable 
+	( Representable, rep, unrep
+	, Corepresentable, corep, uncorep
+	, Both(..), EitherF(..)
+	) where
 
--- instance Adjunction f g => Representable g (f ()) where
--- instance Representable (Cofree Identity) (Free Identity ()) where
+import Control.Functor.Internal.Adjunction
diff --git a/src/Control/Functor/Zap.hs b/src/Control/Functor/Zap.hs
--- a/src/Control/Functor/Zap.hs
+++ b/src/Control/Functor/Zap.hs
@@ -17,47 +17,4 @@
 	, Bizap(..), (>>$<<)
 	) where
 
-import Control.Functor.Combinators.Biff
-import Control.Monad.Either ()
-import Control.Monad.Identity
-
-{- | Minimum definition: zapWith -}
-
--- zapWith :: Adjunction f g => (a -> b -> c) -> f a -> g b -> c
--- zapWith f a b = uncurry (flip f) . counit . fmap (uncurry (flip strength)) $ strength a b
-
--- zap :: Adjunction f g => f (a -> b) -> g a -> b
--- zap = zapWith id
-
-class Zap f g | f -> g, g -> f where
-	zapWith :: (a -> b -> c) -> f a -> g b -> c
-	zap :: f (a -> b) -> g a -> b
-	zap = zapWith id
-
-(>$<) :: Zap f g => f (a -> b) -> g a -> b
-(>$<) = zap
-
-instance Zap Identity Identity where
-	zapWith f (Identity a) (Identity b) = f a b
-
-{- | Minimum definition: bizapWith -}
-
-class Bizap p q | p -> q, q -> p where
-	bizapWith :: (a -> c -> e) -> (b -> d -> e) -> p a b -> q c d -> e
-
-	bizap :: p (a -> c) (b -> c) -> q a b -> c
-	bizap = bizapWith id id
-
-(>>$<<) :: Bizap p q => p (a -> c) (b -> c) -> q a b -> c
-(>>$<<) = bizap
-
-instance Bizap (,) Either where
-	bizapWith l _ (f,_) (Left a) = l f a
-	bizapWith _ r (_,g) (Right b) = r g b 
-
-instance Bizap Either (,) where
-	bizapWith l _ (Left f) (a,_) = l f a
-	bizapWith _ r (Right g) (_,b) = r g b
-
-instance (Bizap p q, Zap f g, Zap i j) => Bizap (Biff p f i) (Biff q g j) where
-	bizapWith l r fs as = bizapWith (zapWith l) (zapWith r) (runBiff fs) (runBiff as)
+import Control.Functor.Internal.Adjunction
diff --git a/src/Control/Monad/Ideal.hs b/src/Control/Monad/Ideal.hs
--- a/src/Control/Monad/Ideal.hs
+++ b/src/Control/Monad/Ideal.hs
@@ -17,107 +17,10 @@
 	, Ideal
 	, ideal
 	, destroyIdeal
-	-- * Coideal Comonads
-	, ComonadCoideal(..)
-	, Coideal
-	, coideal
-	, buildCoideal
 	-- * Mutual recursion for (co)ideal (co)monad (co)products
 	, Mutual(..)
-	-- * Coideal Comonad Product
-	, (:*)
 	-- * Ideal Monad Coproduct
 	, (:+)
 	) where
 
-import Prelude hiding (fst, snd)
-import Control.Category.Cartesian 
-import Control.Category.Hask
-import Control.Comonad
-import Control.Functor
-import Control.Functor.Algebra
-import Control.Functor.Combinators.Lift
-import Control.Monad.Identity
--- Control.Arrow ((|||),(&&&))
--- import Control.Functor.Combinators.Biff
--- import Control.Functor.Combinators.Join
--- import Control.Applicative
-
-type Ideal = Ap Either 
--- type Ideal f = Join (PFree f)
-type Coideal = Ap (,)
--- type Coideal f = Join (PCofree f)
-
-ideal :: Either a (f a) -> Ideal f a
-ideal = mkAp
-
-coideal :: (a, f a) -> Coideal f a 
-coideal = mkAp
-
-runIdeal :: Ideal f a -> Either a (f a)
-runIdeal = runAp
-
-runCoideal :: Coideal f a -> (a, f a)
-runCoideal = runAp
-
-class Functor m => MonadIdeal m where
-	idealize :: m (Either a (m a)) -> m a
-
-instance Functor f => Pointed (Ideal f) where
-	point = Lift . Left . Identity
-
--- this only really needs 'ap' but there is no 'unpointed/pre- applicative'
-{-
-instance Applicative f => Applicative (Ideal f) where
-	pure = point
-	Ideal (Left f) <*> Ideal (Left a) = Ideal $ Left (f a)
-	Ideal (Left f) <*> Ideal (Right bs) = Ideal $ Right (fmap f bs)
-	Ideal (Right fs) <*> Ideal (Left a) = Ideal $ Right (fmap ($a) fs)
-	Ideal (Right fs) <*> Ideal (Right bs) = Ideal $ Right (fs <*> bs)
--}
-
-instance MonadIdeal m => Monad (Ideal m) where
-	return = point
-	m >>= f = ideal . (id ||| Right . idealize) . runIdeal $ fmap (runIdeal . f) m
-
-destroyIdeal :: Algebra m a -> Ideal m a -> a
-destroyIdeal phi = (id ||| phi) . runIdeal 
-
-
--- instance MonadIdeal (Fst k) where
---	idealize = mkFst . runFst
-
-class Functor w => ComonadCoideal w where
-	coidealize :: w a -> w (a, w a)
-
-instance Functor f => Copointed (Coideal f) where
-	extract = runIdentity . fst . runLift
-
-instance ComonadCoideal w => Comonad (Coideal w) where
-	extend f = fmap (f . coideal) . coideal . (id &&& coidealize . snd) . runCoideal
-
-buildCoideal :: Coalgebra m a -> a -> Coideal m a
-buildCoideal phi = coideal . (id &&& phi)
-
--- instance ComonadCoideal (Fst k) where
---	coidealize = mkFst . runFst
-
--- * (Co)ideal (Co)products
-
-newtype Mutual p m n a = Mutual { runMutual :: m (p a (Mutual p n m a)) } 
-type Mutual' p m n = Lift p (Mutual p m n) (Mutual p n m)
-type (m :+ n) = Mutual' Either m n
-type (m :* n) = Mutual' (,) m n
-
-instance (Bifunctor p Hask Hask Hask, Functor m, Functor n) => Functor (Mutual p m n) where
-	fmap f = Mutual . fmap (bimap f (fmap f)) . runMutual
-
-{-
-instance (MonadIdeal m, MonadIdeal n) => MonadIdeal (m :+ n) where
-	idealize = undefined
--}
-
-{-
-instance (ComonadCoideal w, ComonadCoideal v) => ComonadCoideal (w :* v) where
-	coidealize = undefined
--}
+import Control.Functor.Internal.Ideal
diff --git a/src/Control/Monad/Indexed/Cont.hs b/src/Control/Monad/Indexed/Cont.hs
--- a/src/Control/Monad/Indexed/Cont.hs
+++ b/src/Control/Monad/Indexed/Cont.hs
@@ -21,7 +21,7 @@
 
 import Control.Applicative
 import Control.Functor.Pointed
-import Control.Monad.Trans
+-- import Control.Monad.Trans
 import Control.Monad.Identity
 import Control.Monad.Indexed
 import Control.Monad.State