Do The Hokey Cokey

by Nicolas Wu

Posted on 18 April 2011

A recent blog post by Jeremy Gibbons, Morality and Temptation, left the exercise of finding two definitions of the arrow with the signature μF → νF, and showing that they are equivalent. This post shows my solution to this problem, and while I’m here, I too have a confession to make: when dealing with the ins and outs of initial algebras and final coalgebras I sometimes get the Hokey Cokey playing in my mind. For those of you who don’t know this children’s song, it goes something like this:

You put your left foot in,
Your left foot out,
In, out, in, out,
You shake it all about.
You do the Hokey Cokey,
And you turn around,
That’s what it’s all about!

Now that’s out of the way, let’s focus on the problem at hand. I’ll start by summarising some of the basics of what we’re tackling.

Your F-Algebra In

Given a functor $F : \C → \C$, an F-Algebra is a pair (X,f), where $X ∈ \C$, and $f ∈ \C(F X, X)$. F-Algebras are objects in the category written Alg_F, where an arrow in this category is given by an $h ∈ \C$ such that the following property holds between two objects (X,f), and (Y,g): h.f = g.Fh The construction of a fold is given by looking at the initial object in this category, written as (μF,in). Initial objects have a unique arrow to every object in the category; in this category the unique arrow to an object (Y,g) is given by $\fold{g}$, and it makes the following commute (you’ll have to excuse the ASCII diagrams, I have yet to find a good way of rendering commutative diagrams for the web):

        F(|g|)
   F μF ─——————> F Y
    │             │
 in │             │ g
    │             │
    V             V
    μF ---------> Y
         (|g|)

Following the arrows of this diagram gives us most of the ingredients needed to state the Universal Property of a fold, which is as follows: $$ h . in = g . F h ⇔ \fold{g} = h $$ In other words, $\fold{g}$ is the unique solution that satisfies this commuting diagram.

Your F-Coalgebra Out

Given a functor $F : \C → \C$, an F-coalgebra is the categorical dual of an F-algebra and inhabits the Coalg_F category. Here, objects are pairs (X,f), where $X ∈ \C$, and $f ∈ \C(X, F X)$.

Unsurprisingly, we are interested in the final object, written (νF,out), of this category, where the unique arrow from every object (X,f) to the final object is written $\unfold{f}$, and the following commutes:

       F[(f)]
  F X ────────> F νF
   ^             ^
   │             │
 f │             │ out
   │             │
   │             │
   X ----------> νF
        [(f)]

The universal property also dualises, and in this case we have: $$ h = \unfold{f} ⇔ F h . f = out . h $$ This property simply states that $\unfold{f}$ is the unique equation satisfying the commuting diagram.

In, Out, In, Out

Our goal is to find two definitions of an arrow of type μF → νF, and to show that these definitions are equivalent. Looking at the definition of an initial F-algebra, it’s pretty obvious that we can produce such an arrow by taking the fold of an arrow with type F(νF) → νF. Using the inverse of out, which we’ll write as out°, is a fairly obvious choice and produces the following diagram:

         F(|out°|)
    F μF ─———————> F νF
     │              │
     │              │
  in │              │ out°
     │              │
     V              V
     μF ----------> νF
         (|out°|)

By dualizing, the alternative definition of this arrow becomes quite apparent, where the unfold of in° is used instead:

         F[(in°)]
    F μF ─———————> F νF
     ^              ^
     │              │
 in° │              │ out
     │              │
     │              │
     μF ----------> νF
         [(in°)]

So, we now have two definitions for the arrow in question, $\fold{out°}$, and $\unfold{in°}$. All that is left is to show that these two definitions are equivalent.

Shake It All About

The universal properties of folds and unfolds are a useful way of encoding lots of information about their structure in one place. Consequently, these properties are very useful tools for proving properties of folds and unfolds.

By plugging our two arrows into the equations that describe the universal properties of folds and unfolds, we get the following: $$ \unfold{in°} . in = out° . F \unfold{in°} ⇔ \fold{out°} = \unfold{in°} ⇔ F \fold{out°} . in° = out . \fold{out°} $$ I think this equation is marvellous, I don’t know if it has a name, but for the purpose of this post I’ll call it the Hokey Cokey Law. The left hand side comes from instantiating the universal property for folds with an unfold, and the right hand side comes from instantiating the universal property for unfolds with a fold.

Do the Hokey Cokey

We still haven’t proved that $\fold{out°} = \unfold{in°}$, but proving either the left hand side or the right hand side of the equation is all that is required. Let’s start with what is known: the universal property of fold applied to $\fold{out°}$:

$\fold{out°} . in = out° . F \fold{out°}$

$\hint{⇒}{Leibniz, twice}$

$out . \fold{out°} . in . in° = out . out° . F \fold{out°} . in°$

$\hint{⇒}{Identity, twice}$

$out . \fold{out°} = F \fold{out°} . in°$

$\hint{⇔}{Hokey Cokey}$

$\fold{out°} = \unfold{in°}$

So there you have it, the Hokey Cokey in all its glory. Of course, we could take this proof and turn around, since everything dualises: we could have equally picked the universal of unfold applied to $\unfold{in°}$, and would have arrived at the left hand side of our equivalence. That’s what it’s all about!

Woah! The Hokey Cokey!
Woah! The Hokey Cokey!
Woah! The Hokey Cokey!
Knees bent, arms stretched, ra ra ra!