How to define list zipping categorically/inductively? Lists and fixpoints

The type of $A$-lists is defined as $\mu F_A$, where $F_A(X) = 1 + A \times X$ is the "cons-or-nil"-functor and $\mu$ is the least fixpoint operator. In Haskell syntax, this would correspond to:

data List a
   = Nil
   | Cons a (List a)


Here, Nil is the sole inhabitant of $1$, and Cons a as corresponds to A \times X. The fact that lists are fixpoints is reflected in the recursive definition of List a.

Initial algebras

It is well known that least fixpoints have semantics in initial algebras.
See e.g. Brian Howard's thesis. For our purposes, the type of $A$-lists is the initial algebra of the functor $F_A$.

Algebra map

Being an algebra, lists come with the algebra map $\phi\colon F_A (\mu F_A) \to \mu F_A$. It an isomorphism, so if we unpack we have $1 + A \times \mu F_A \cong \mu F_A$. In words, a list is either empty or consists of an $A$ and another list.

Universal property

Since $\mu F_A$ is initial, there is a unique algebra map from $A$-lists to any $F_A$ algebra. That is, if there is a morphism $\beta\colon F_A B \to B$, there is a unique algebra map $\mathrm{it}(\beta)\colon \mu F_A \to B$.

Warm up: Unzip

unzip takes a list of pairs $\mu F_{A \times B}$ and produces a pair of lists $\mu F_A \times \mu F_B$. It is thus a function from a list into something else, and could thus be defined via the universal property. All we need to do is to give $\mu F_A \times \mu F_B$ the right $F_{A \times B}$-structure:

$$F_{A \times B} (\mu F_A \times \mu F_B) = 1 + A \times B \times  \mu F_A \times \mu F_B$$
$$\hookrightarrow 1 + A \times \mu F_A + B \times \mu F_B + A \times B \times \mu F_A \times \mu F_B$$
$$\cong (1 + A \times \mu F_A) \times (1 + B \times \mu F_B) = \mu F_A \times \mu F_B$$

One can see that we inject into either the case "both lists stop" or "both lists continue". Apply the universal property, and you have unzip.

Puzzle: Zip

Now we would like to do the reverse. Given two lists, create a list of pairs. The Haskell version is simple:

zip (Cons a as) (Cons b bs) = Cons (a, b) $ zip as bs
zip _ _ = Nil


But now we need to write a function into a list. This suggests using the algebra morphism, but I can't figure out how. Alternatively, one might want to create an algebra structure for $\mu F_{A \times B}$ for some other functor, but I don't know which, and I don't know how to map from two fixpoints into a single one.
This complication is the same as in the definition of the Church predecessor function. We need to take the tail of a list, but we only have a folding operation given by (weak) initiality, which does not directly provide access to that, so we need to rebuild the tail from the right end.

It is the easiest to write the solution in a lambda calculus with products, exponentials and foldr for lists, witnessing weak initiality. In Haskell:

-- foldr :: (a -&gt; b -&gt; b) -&gt; b -&gt; [a] -&gt; b

-- matching on whether a list is empty or non-empty
split :: [a] -&gt; b -&gt; (a -&gt; [a] -&gt; b) -&gt; b
split as b f = fst (foldr (\a (b, as) -&gt; (f a as, a:as)) (b, []) as)

zip :: [a] -&gt; [b] -&gt; [(a, b)]
zip = foldr (\a hyp ys -&gt; split ys [] (\b ys -&gt; (a, b): hyp ys))
            (\_ -&gt; [])


With split we can branch on whether a list is empty or non-empty, and we rebuild the tail of the list from the end. zip can be translated back to cartesian closed categories with list objects, but of course a precise definition in that setting would be much less readable, because of the mandatory point-free definitions.