 To make sure that this works, we follow an arbitrary pair of streams, say  ⟨s,t⟩  around the square, starting in the upper-left.   Going down, we have the stream    zip(s, t). From this, the structure takes this to ⟨head(zip(s, t)),  tail(zip(s, t))⟩  ∈ FN∞. But we could also take our  ⟨s, t⟩  across the top via f to get  ⟨head(s),      ⟨t, tail(s)⟩⟩. Now Fzip applies to this pair, and  this is where the action of F as a functor enters.   We get  ⟨head(s), zip(tail(t), s)⟩. So overall, we have  