## 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