Editing Catamorphisms (section)

== Mendler and the Contravariant Yoneda Lemma ==
The definition of a Mendler-style algebra above can be seen as the application of the contravariant version of the Yoneda lemma to the functor in question. 

In type theoretic terms, the contravariant Yoneda lemma states that there is an isomorphism between (f a) and ∃b. (b -> a, f b), which can be witnessed by the following definitions.

<haskell>
  data CoYoneda f a = forall b. CoYoneda (b -> a) (f b)  
  toCoYoneda :: f a -> CoYoneda f a 
  toCoYoneda = CoYoneda id  
  fromCoYoneda :: Functor f => CoYoneda f a -> f a 
  fromCoYoneda (CoYoneda f v) = fmap  f v   
</haskell>
Note that in Haskell using an existential requires the use of data, so there is an extra bottom that can inhabit this type that prevents this from being a true isomorphism.

However, when used in the context of a (CoYoneda f)-Algebra, we can rewrite this to use universal quantification because the functor f only occurs in negative position, eliminating the spurious bottom.
<haskell>
  Algebra (CoYoneda f) a 
    = (by definition) CoYoneda f a -> a 
    ~ (by definition) (exists b. (b -> a, f b)) -> a 
    ~ (lifting the existential) forall b. (b -> a, f b) -> a 
    ~ (by currying) forall b. (b -> a) -> f b -> a 
    = (by definition) MendlerAlgebra f a
</haskell>