 Here is how zip  is uniquely defined via a corecursive definition. Write  N∞× N∞  as S in this discussion. We want a map from S to N∞.  We are dealing with S as the final coalgebra of   the functor Fa = N × a.  And we’ll write the structure  on the final coalgebra as ⟨ head, tail&amp;thinsp;⟩, just as we did it in Section 1.1. The idea is to turn  S into the carrier set of a coalgebra for, say  (S, f).  Then zip will be the unique coalgebra morphism from   (S, f) to   (S, ⟨ head,tail ⟩ ).    It remains to define f. Let  