Equalizers of Comonads

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