Control.Morphism.Meta.Erwig

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

Documentation

meta :: Functor h => Bialgebra m n b -> (h :~> m) -> Bialgebra f h a -> a -> b

meta d f c is Martin Erwig's metamorphism from c to d