in turn, eventually resulting in just leaf nodes – actual leaf nodes, and branch nodes whose children have already been dealt with (cut off below). By contrast, the corecursive traversal handles a root node (at the top) as the base case (given a node, first output the value), treats a tree as being synthesized of a root node and its children, then produces as auxiliary output a list of subtrees at each step, which are then the input for the next step – the child nodes of the original root are the root nodes at the next step, as their parents have already been dealt with (cut off above). In the recursive traversal there is a distinction between leaf nodes and branch nodes, while in the corecursive traversal there is no distinction, as each node is treated as the root node of the subtree it defines. Notably, given an infinite tree, the corecursive breadth-first traversal will traverse all nodes, just as for a finite tree, while the recursive depth-first traversal will go down one branch and not traverse all nodes, and indeed if traversing post-order, as in this example (or in-order), it will visit no nodes at all, because it never reaches a leaf. This shows the usefulness of corecursion rather than recursion for dealing with infinite data structures. In Python, this can be implemented as follows. The usual post-order depth-first traversal can be defined as: def df(node): """Post-order depth-first traversal.""" if node is not None: df(node.left) df(node.right) print(node.value) This can then be called by df(t) to print the values of the nodes of the tree in post-order depth-first order. The breadth-first corecursive generator can be defined as: def bf(tree): """Breadth-first corecursive generator.""" tree_list = [tree] while tree_list: new_tree_list = [] for tree in tree_list: if tree is not None: yield tree.value new_tree_list.append(tree.left) new_tree_list.append(tree.right) tree_list = new_tree_list This can then be called to print the values of the nodes of the tree in breadth-first order: for i in bf(t): print(i) Definition Initial data types can be defined as being the least fixpoint (up to isomorphism) of some type equation; the isomorphism is then given by an initial algebra. Dually, final (or terminal) data types can be defined as being the greatest fixpoint of a type equation; the isomorphism is then given by a final coalgebra. If the domain of discourse is the category of sets and total functions, then final