How to define list zipping categorically/inductively?
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.