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:
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.
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.
$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.
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.
foldroperation (for some specific element type). $\endgroup$