That's simple Tom. Imagine the factorial function for Int written as a paramorphism: type instance F Int = Either One instance (Mu Int) where inn (Left _) = 0 inn (Right n) = succ n out 0 = Left () out n = Right (pred n) instance Functor (F Int) where fmap _ (Left ()) = Left () fmap f (Right n) = Right (f n) fact :: Int -> Int fact = para (const 1 \/ (uncurry (*)) . (id >< succ)) If we consider that the paramorphism is implemented as an hylomorphism, then an intermediate virtual type (d in the hylo definition) [Int] If you test the constraints for d = [Int], a = Int and c = Int F d c ~ F a (c,a) F d a = F [Int] Int = Either One (Int,Int) F a (c,a) = F Int (Int,Int) = Either One (Int,Int) F d a ~ F a (a,a) F d a = F a (a,a) -- pure substitution of the above case Hope this helps. Thanks again for you patience, hugo