# Understanding Isabelle's implementation of coinduction

I'm studying how coinduction was encoded in Isabelle. At page 7 of the attached document, the author describes how some datatypes can be encoded as initial algebras. Here is one example:

Finite lists

The unary type constructor list, which sends each type α to the type α list of lists of α elements, is categorically given as the initial algebra on the second argument of the binary functor (F, Fmap), where (α, β) F = unit+α×β and Fmap f g = id⊕ f ⊗g.

More precisely, there exists a (polymorphic) folding bijection fld : (α, α list) F → α list making (fld, α list) the initial algebra for the unary functor (α, _) F. Here, fld = $$\langle$$Nil, Cons$$\rangle$$, where Nil and Cons are the familiar list operations. The initial algebra property corresponds to the availability of the standard iterator for lists. Then (list, map) is itself a unary functor.

First parragraph

If $$U$$ is the set of types. $$F: U \times U \to U$$ is a functor which on objects acts like $$F(\alpha,\beta) = unit+\alpha \times \beta$$ and on morphisms acts as $$F((f,g)) = id \oplus f \otimes g$$. As usual, this functor will lead to another functor if we fix $$\alpha$$. Let's call it $$G$$. Then, one defines lists as being the initial algebra (if it exists) for the functor $$G$$. Let's call $$\alpha \; list$$ the carrier of that algebra.

I think initial algebras for polynomial functors $$F: Set \to Set$$ always exist so let's drop the existence matter here.

Second parragraph

$$fld$$ seems to be the structure mapping of the coalgebra $$fld: G(\alpha \; list) \to \alpha \; list$$. So in my notation the $$G$$-algebra is $$(\alpha \; list, fld)$$. One may check that $$\langle Nil, Cons \rangle$$ make $$fld$$ work in the initiality diagram.

Now:

What is meant by the standard "iterator" for lists?

Where was $$(list,map)$$ defined? (I think nowhere). What is the author transmitting by saying that $$(list,map)$$ is a unary functor?

It may be worth reading the following section on "Finitely branching trees of finite depth" in the linked thesis.

• The standard iterator on lists is the catamorphism, which corresponds to the foldr operation (for some specific element type). Apr 1, 2020 at 7:02