# Equalizers of Comonads

by Phil Freeman on 2017/07/13

Here's an interesting little result:

Consider a comonad `w` which preserves limits, and suppose we have a natural transformation `f :: w ~> I` where `I` is the identity functor.

Note that `extend f` is also a natural transformation `w ~> w`.

When the equalizer `q ~> w` of `extend f` and `id` exists, it also has a comonadic structure, induced by the one on `w`.

Before seeing the proof, let's consider what this means for the comonads as spaces approach to user interfaces.

## Example

Take `w` to be a cofree comonad generated by the functor

``````data Step a = Step a a
``````

The dual functor

``````data Action a = L a | R a
``````

defines a free monad which pairs with `w`. The actions

``````left, right :: Free Action Unit
left = liftFree (L unit)
right = liftFree (R unit)
``````

combine to give two "loops" `left *> right` and `right *> left`. These loops pair to give natural transformations `w ~> w`.

We can form the equalizer which makes these loops equal to the identity, and we can think of the resulting comonad as a zipper which is infinite in both directions.

In practice, this means that we can work with the original comonad `w` if it is more convenient, as long as our actions equalize the appropriate morphisms, so that we stay inside the equalizer.

## Proof (Sketch)

Suppose the equalizer `phi :: q ~> w` exists.

Consider the natural transformation `duplicate . phi :: q ~> w^2`. We have

``````extend f . duplicate . phi
= map f . duplicate . duplicate . phi
{- naturality -}
= duplicate . map f . duplicate . phi
= duplicate . extend f . phi
{- phi equalizes extend f and id -}
= duplicate . phi
``````

So `duplicate . phi` equalizes `extend f` and `id`. Therefore it factors through the equalizer, and we have `gamma :: q ~> w q` such that `map phi . gamma = duplicate . phi`.

Now, since `w` preserves limits, we have that `wq` is the equalizer of `map (extend f)` and `id`. `gamma` factors through this equalizer (to see this, consider composition on the left with `map phi`, which is mono), and so induces `alpha :: q -> q^2` such that `phi . alpha = gamma`.

The claim is that `alpha` gives a comonad structure on `q`, together with `extract` given by `extract . phi`.

To see this, observe that `map phi . phi . alpha = duplicate . phi`, and that `phi` is a mono. The comonad laws for `duplicate` pull back to the equivalent laws for `alpha` via the mono `phi`.

QED