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.53.0
+version:                0.53.1
 license:                BSD3
 cabal-version:          >= 1.2
 license-file:           LICENSE
@@ -130,14 +130,17 @@
                 Control.Morphism.Chrono,
                 Control.Morphism.Destroy,
                 Control.Morphism.Dyna,
+                Control.Morphism.Exo,
                 Control.Morphism.Futu,
                 Control.Morphism.Histo,
                 Control.Morphism.Hylo,
-                Control.Morphism.Meta,
+                Control.Morphism.Meta.Gibbons,
+                Control.Morphism.Meta.Erwig,
                 Control.Morphism.Para,
                 Control.Morphism.Postpro,
                 Control.Morphism.Prepro,
                 Control.Morphism.Span,
+                Control.Morphism.Synchro,
                 Control.Morphism.Universal,
                 Control.Morphism.Zygo,
                 Data.Void
diff --git a/src/Control/Functor/Algebra.hs b/src/Control/Functor/Algebra.hs
--- a/src/Control/Functor/Algebra.hs
+++ b/src/Control/Functor/Algebra.hs
@@ -16,6 +16,7 @@
 	, Bialgebra, GBialgebra
 	, Algebra, GAlgebra
 	, Coalgebra, GCoalgebra
+	, Trialgebra
 	, liftAlgebra
 	, liftCoalgebra
 	, liftDialgebra
@@ -39,6 +40,9 @@
 -- and so add no expressive power, but are a lot more convenient.
 type Bialgebra f g a = (Algebra f a, Coalgebra g a)
 type GBialgebra f g w m a = (GAlgebra f w a, GCoalgebra g m a)
+
+-- | Martin Erwig's trialgebras for indexed data types
+type Trialgebra f g h a = (Algebra f a, Dialgebra g h a)
 
 -- | F-Algebras
 type Algebra f a = f a -> a
diff --git a/src/Control/Functor/Extras.hs b/src/Control/Functor/Extras.hs
--- a/src/Control/Functor/Extras.hs
+++ b/src/Control/Functor/Extras.hs
@@ -18,13 +18,14 @@
 
 type Dist f g = forall a. f (g a) -> g (f a)
 
--- A natural transformation between functors f and g.
+-- | A natural transformation between functors f and g.
 type f :~> g = forall a. f a -> g a
+type Natural f g = f :~> g
 
--- Its bifunctorial analogue
+-- | A transformation natural in both sides of a bifunctor.
 type f :~~> g = forall a b. f a b -> g a b
 
--- Dinatural transformations
+-- | Dinatural transformations
 type Dinatural f g = forall a. f a a -> g a a
 
 class PostFold m f where
diff --git a/src/Control/Functor/Fix.hs b/src/Control/Functor/Fix.hs
--- a/src/Control/Functor/Fix.hs
+++ b/src/Control/Functor/Fix.hs
@@ -15,8 +15,10 @@
 	-- * Functor fixpoint
 	  FixF(InF,outF)
 	, outM, inW
+	, identityBialgebraF
 	-- * Bifunctor fixpoint
 	, Fix(InB,outB)
+	, identityBialgebraB
 	, paugment, pcoaugment
 	) where
 
@@ -37,8 +39,10 @@
 inW :: (Functor f, Comonad w) => GAlgebra f w (FixF f)
 inW = liftAlgebra InF
 
--- * Fixpoint of a bifunctor
+identityBialgebraF :: Bialgebra f f (FixF f)
+identityBialgebraF = (InF,outF)
 
+-- * Fixpoint of a bifunctor
 newtype Fix s a = InB { outB :: s a (Fix s a) }
 
 instance Bifunctor s Hask Hask Hask => Functor (Fix s) where
@@ -56,6 +60,9 @@
 instance (Bifunctor f Hask Hask Hask, PMonad f) => Monad (Fix f) where
         return = InB . preturn
         m >>= k = paugment (\f -> bihylo f id outB m) k
+
+identityBialgebraB :: Bialgebra (f a) (f a) (Fix f a)
+identityBialgebraB = (InB,outB)
 
 paugment :: PMonad f => (forall c. (f a c -> c) -> c) -> (a -> Fix f b) -> Fix f b
 paugment g k = g (InB . pbind (outB . k))
diff --git a/src/Control/Morphism/Ana.hs b/src/Control/Morphism/Ana.hs
--- a/src/Control/Morphism/Ana.hs
+++ b/src/Control/Morphism/Ana.hs
@@ -42,11 +42,11 @@
 distAna :: Functor f => Dist Identity f
 distAna = fmap Identity . runIdentity
 
-biana :: Bifunctor f Hask Hask Hask => Coalgebra (f b) a -> a -> Fix f b
-biana g = InB . bimap id (biana g) . g
+biana :: QFunctor f Hask Hask => Coalgebra (f b) a -> a -> Fix f b
+biana g = InB . second (biana g) . g
 
-g_biana :: (Bifunctor f Hask Hask Hask, Monad m) => Dist m (f b) -> GCoalgebra (f b) m a -> a -> Fix f b
-g_biana k g = a . return where a = InB . bimap id (a . join) . k . liftM g
+g_biana :: (QFunctor f Hask Hask, Monad m) => Dist m (f b) -> GCoalgebra (f b) m a -> a -> Fix f b
+g_biana k g = a . return where a = InB . second (a . join) . k . liftM g
 
 -- | A higher-order anamorphism for constructing higher order functors.
 hana :: HFunctor f => HCoalgebra f a -> a :~> FixH f
diff --git a/src/Control/Morphism/Cata.hs b/src/Control/Morphism/Cata.hs
--- a/src/Control/Morphism/Cata.hs
+++ b/src/Control/Morphism/Cata.hs
@@ -40,11 +40,11 @@
 distCata :: Functor f => Dist f Identity
 distCata = Identity . fmap runIdentity
 
-bicata :: Bifunctor f Hask Hask Hask => Algebra (f b) a -> Fix f b -> a
-bicata f = f . bimap id (bicata f) . outB
+bicata :: QFunctor f Hask Hask => Algebra (f b) a -> Fix f b -> a
+bicata f = f . second (bicata f) . outB
 
-g_bicata :: (Bifunctor f Hask Hask Hask, Comonad w) => Dist (f b) w -> GAlgebra (f b) w a -> Fix f b -> a
-g_bicata k g = extract . c where c = liftW g . k . bimap id (duplicate . c) . outB
+g_bicata :: (QFunctor f Hask Hask, Comonad w) => Dist (f b) w -> GAlgebra (f b) w a -> Fix f b -> a
+g_bicata k g = extract . c where c = liftW g . k . second (duplicate . c) . outB
 
 hcata :: HFunctor f => HAlgebra f a -> FixH f :~> a
 hcata f = f . hfmap (hcata f) . outH
diff --git a/src/Control/Morphism/Exo.hs b/src/Control/Morphism/Exo.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Exo.hs
@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Morphism.Exo
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+-- Martin Erwig's exomorphism
+----------------------------------------------------------------------------
+module Control.Morphism.Exo 
+	( exo
+	) where
+
+import Control.Functor.Algebra
+import Control.Morphism.Hylo
+
+-- | Martin Erwig's exomorphism from d to d'
+exo :: Functor h => Bialgebra m n b -> (h b -> m b) -> (h a -> h (g a)) -> Trialgebra f g h a -> g a -> b
+exo d' f g d = hylo (fst d' . f) id (g . snd d)
+
diff --git a/src/Control/Morphism/Meta.hs b/src/Control/Morphism/Meta.hs
deleted file mode 100644
--- a/src/Control/Morphism/Meta.hs
+++ /dev/null
@@ -1,33 +0,0 @@
-{-# OPTIONS_GHC -fglasgow-exts #-}
------------------------------------------------------------------------------
--- |
--- Module      :  Control.Morphism.Meta
--- Copyright   :  (C) 2008 Edward Kmett
--- License     :  BSD-style (see the file LICENSE)
---
--- Maintainer  :  Edward Kmett <ekmett@gmail.com>
--- Stability   :  experimental
--- Portability :  non-portable (rank-2 polymorphism)
---
--- A very basic Jeremy Gibbons metamorphism, without all 
--- the productive stream stuff. See:
--- <http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/metamorphisms-scp.pdf>
--- TODO: Add some support for spigot algorithms over streams/lists.
-----------------------------------------------------------------------------
-module Control.Morphism.Meta where
-
-import Control.Functor.Algebra
-import Control.Functor.Extras
-import Control.Functor.Fix
-import Control.Comonad
-import Control.Monad.Identity
-import Control.Morphism.Ana
-import Control.Morphism.Cata
-
-meta :: (Functor f, Functor g) => 
-	  Coalgebra f b -> (a -> b) -> Algebra g a -> FixF g -> FixF f
-meta f e g = ana f . e . cata g
-
-g_meta :: (Monad m, Functor f, Comonad w, Functor g) => 
-	  Dist m f -> Dist g w -> GCoalgebra f m b -> (a -> b) -> GAlgebra g w a -> FixF g -> FixF f
-g_meta m w f e g = g_ana m f . e . g_cata w g
diff --git a/src/Control/Morphism/Meta/Erwig.hs b/src/Control/Morphism/Meta/Erwig.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Meta/Erwig.hs
@@ -0,0 +1,29 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Morphism.Meta.Erwig
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+-- Martin Erwig's metamorphisms for indexed data types.
+-- 
+-- ADT fusion: @snd c . fst c == id  => erwig d id c . erwig c id d' = erwig d id d'@
+-- 
+-- FreeMeta: @l strict, snd c == snd c' == phi', fst d == fst d' == alpha, l . fst c = fst c' . fmap l, snd d' . rr = fmap r . snd d ==> l . (erwig d id c) = (erwig d' id c') . r@
+----------------------------------------------------------------------------
+module Control.Morphism.Meta.Erwig
+	( meta
+	) where
+
+import Control.Functor.Algebra
+import Control.Functor.Extras
+import Control.Morphism.Hylo
+
+-- | @meta d f c@ is Martin Erwig's metamorphism from @c@ to @d@
+meta :: Functor h => Bialgebra m n b -> (h :~> m) -> Bialgebra f h a -> a -> b
+meta d f c = hylo (fst d) f (snd c)
+
diff --git a/src/Control/Morphism/Meta/Gibbons.hs b/src/Control/Morphism/Meta/Gibbons.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Meta/Gibbons.hs
@@ -0,0 +1,39 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Morphism.Meta.Gibbons
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+-- A very basic Jeremy Gibbons metamorphism, without all 
+-- the productive stream stuff. See:
+-- <http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/metamorphisms-scp.pdf>
+-- TODO: Add some support for spigot algorithms over streams/lists.
+----------------------------------------------------------------------------
+module Control.Morphism.Meta.Gibbons 
+	( meta
+	, g_meta
+	) where
+
+import Control.Functor.Algebra
+import Control.Functor.Extras
+import Control.Functor.Fix
+import Control.Comonad
+import Control.Monad.Identity
+import Control.Morphism.Ana
+import Control.Morphism.Cata
+
+-- Jeremy Gibbons' metamorphism
+meta :: (Functor f, Functor g) => 
+	  Coalgebra f b -> (a -> b) -> Algebra g a -> FixF g -> FixF f
+meta f e g = ana f . e . cata g
+
+-- | Generalized Jeremy Gibbons metamorphism
+g_meta :: (Monad m, Functor f, Comonad w, Functor g) => 
+	  Dist m f -> Dist g w -> GCoalgebra f m b -> (a -> b) -> GAlgebra g w a -> FixF g -> FixF f
+g_meta m w f e g = g_ana m f . e . g_cata w g
+
diff --git a/src/Control/Morphism/Postpro.hs b/src/Control/Morphism/Postpro.hs
--- a/src/Control/Morphism/Postpro.hs
+++ b/src/Control/Morphism/Postpro.hs
@@ -15,18 +15,28 @@
 module Control.Morphism.Postpro 
 	( postpro
 	, g_postpro
+	, bipostpro
+	, g_bipostpro
 	) where
 
 import Control.Monad
+import Control.Category.Hask
+import Control.Functor
 import Control.Functor.Algebra 
 import Control.Functor.Extras
 import Control.Functor.Fix
 import Control.Morphism.Ana
 
 -- prepro f e = x where x = f . fmap (x . cata (InF . e)) . outF
-postpro :: Functor f => (c -> f c) -> (f :~> f) -> c -> FixF f
+postpro :: Functor f => Coalgebra f c -> (f :~> f) -> c -> FixF f
 postpro g e = x where x = InF . fmap (ana (e . outF) . x) . g
 
 -- | Generalized postpromorphisms
 g_postpro :: (Functor f, Monad m) => Dist m f -> GCoalgebra f m a -> (f :~> f) -> a -> FixF f
 g_postpro k g e = a . return where a = InF . fmap (ana (e . outF) . a . join) . k . liftM g
+
+bipostpro :: Bifunctor f Hask Hask Hask => Coalgebra (f a) c -> (f a :~> f a) -> c -> Fix f a
+bipostpro g e = x where x = InB . bimap id (biana (e . outB) . x) . g
+
+g_bipostpro :: (Bifunctor f Hask Hask Hask, Monad m) => Dist m (f a) -> GCoalgebra (f a) m c -> (f a :~> f a) -> c -> Fix f a
+g_bipostpro k g e = a . return where a = InB . bimap id (biana (e . outB) . a . join) . k . liftM g
diff --git a/src/Control/Morphism/Prepro.hs b/src/Control/Morphism/Prepro.hs
--- a/src/Control/Morphism/Prepro.hs
+++ b/src/Control/Morphism/Prepro.hs
@@ -10,10 +10,11 @@
 -- Portability :  non-portable (rank-2 polymorphism)
 -- 
 -- See Maarten Fokkinga''s PhD Dissertation for cascade and prepro.
--- g_prepro is an obvious generalization.
+-- g_prepro is an obvious generalization. The prepro variants of other
+-- morphisms are distributed through the corresponding files.
 ----------------------------------------------------------------------------
 module Control.Morphism.Prepro 
-	( prepro, g_prepro, cascade
+	( prepro, g_prepro, cascade, biprepro, g_biprepro
 	) where
 
 import Control.Comonad
@@ -23,22 +24,33 @@
 import Control.Functor.Algebra 
 import Control.Functor.Extras
 import Control.Functor.Fix
--- import Control.Functor.HigherOrder
 import Control.Monad.Identity
 import Control.Morphism.Cata
 
 -- | @cascade f . map f = map f . cascade f@
+-- | @cascade f = biprepro InB (first f)@
+-- | @cascade f = x where x = InB . bimap id (x . fmap f) . outB@
+-- | @cascade f = x where x = InB . bimap id (fmap f . x) . outB@
 cascade :: Bifunctor s Hask Hask Hask => (a -> a) -> Fix s a -> Fix s a 
-cascade f = InB . bimap id (cascade f . fmap f) . outB 
--- equivalently:
--- cascade f = InB . bimap id (fmap f . cascade f) . outB 
+-- cascade f = biprepro InB (first f)
+cascade f = x where x = InB . bimap id (x . fmap f) . outB 
+-- equivalently: @cascade f = InB . bimap id (fmap f . cascade f) . outB@
 
-prepro :: Functor f => (f c -> c) -> (f :~> f) -> FixF f -> c
+-- | Fokkinga's Prepromorphism
+prepro :: Functor f => Algebra f c -> (f :~> f) -> FixF f -> c
 prepro f e = x where x = f . fmap (x . cata (InF . e)) . outF
 
--- | Generalized prepromorphisms
+-- | Generalized prepromorphisms, parameterized by a comonad
+-- This is used to generate most of the specialized prepromorphisms in other modules.
+-- You can use the distributive law combinators to build up analogues of other recursion 
+-- schemes.
 g_prepro :: (Functor f, Comonad w) => Dist f w -> GAlgebra f w a -> (f :~> f) -> FixF f -> a
 g_prepro k g e = extract . c where c = liftW g . k . fmap (duplicate . c . cata (InF . e)) . outF
 
---repro :: Functor f => (f b -> b) -> (f :~> f) -> (f :~> f) -> (a -> f a) -> a -> b
---repro f fe ge g = x where x = f . fmap (ana (fe . outF) . x . cata (InF . ge)) . g
+-- | Prepromorphisms for bifunctors
+biprepro :: Bifunctor f Hask Hask Hask => Algebra (f a) c -> (f a :~> f a) -> Fix f a -> c
+biprepro f e = x where x = f . bimap id (x . bicata (InB . e)) . outB
+
+-- | Generalized bifunctor prepromorphism, parameterized by a comonad
+g_biprepro :: (Bifunctor f Hask Hask Hask, Comonad w) => Dist (f a) w -> GAlgebra (f a) w c -> (f a :~> f a) -> Fix f a -> c
+g_biprepro k g e = extract . c where c = liftW g . k . bimap id (duplicate . c . bicata (InB . e)) . outB
diff --git a/src/Control/Morphism/Synchro.hs b/src/Control/Morphism/Synchro.hs
new file mode 100644
--- /dev/null
+++ b/src/Control/Morphism/Synchro.hs
@@ -0,0 +1,48 @@
+{-# OPTIONS_GHC -fglasgow-exts #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Control.Morphism.Synchro
+-- Copyright   :  (C) 2008 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  experimental
+-- Portability :  non-portable (rank-2 polymorphism)
+--
+-- Martin Erwig's synchromorphisms.
+----------------------------------------------------------------------------
+module Control.Morphism.Synchro where
+
+import Control.Category.Cartesian ((&&&))
+import Control.Category.Hask
+import Control.Functor
+import Control.Functor.Algebra
+
+-- | @synchro d' f d g1 g2 d''@ is Martin Erwig's @d,d''-synchromorphism to d'@. Mostly useful for graph algorithms.
+synchro :: 
+	QFunctor h Hask Hask => 
+	Bialgebra m n c -> 
+	(h x (Either a c) -> m c) -> 
+	Trialgebra (f x) (g x) (h x) a -> 
+	((h x a, b) -> k x b) -> 
+	((h x a, j x b) -> h x (Either a (g x a, b))) -> 
+	Bialgebra (k x) (j x) b -> 
+	(g x a, b) -> c 
+
+--             g1
+-- h = D' <- D <-> D''
+--       f     g2
+-- dfs = List <- Graph <-> Stack -- depth-first search
+-- bfs = List <- Graph <-> Queue -- breadth-first search
+
+synchro d' f d g1 g2 d'' = h where
+	h = fst d' . f . second (second h) . g2 . (fst &&& (snd d'' . fst d'' . g1)) . first (snd d)
+	-- (g x a, b) 			>- first (snd d)  ->
+	-- (h x a, b) 			>- (fst &&& g1) ->
+	-- (h x a, k x b) 		>- second (fst d'') ->
+	-- (h x a, b) 			>- second (snd d'') ->
+	-- (h x a, j x b)		>- g2 ->
+	-- (h x (Either a (g x a, b)) 	>- second (second h) ->
+	-- (h x (Either a c))		>- f ->
+	-- m c				>- fst d'
+	-- c