Exercise from Algebra of Programming on catamorphisms

This is an exercise from Algebra of Programming which I'm reading for self-study. Below, $$T$$ is the initial algebra of $$F$$.

What I've tried:

I can construct $$h \circ F (\pi_2) : F(A \times B) \rightarrow B$$. Then we take the product $$\langle g, h \circ F(\pi_2) \rangle : F(A \times B) \rightarrow A \times B$$. We can then take the catamorphism $$cata(\langle g, h \circ F(\pi_2) \rangle) : T \rightarrow A\times B$$ and need to show that $$f = \pi_1 \circ cata(\langle g, h \circ F(\pi_2) \rangle)$$.

I've tried using the fact that the diagram above commutes to get the equality above, to no avail. Any suggestions?

• What are $outl$ and the banana brackets around $k$? Commented Jul 8, 2022 at 2:01
• Hint: prove the stronger statement $(f,cata(h))=cata(\langle g,h\circ F(\pi_2)\rangle),$ using the uniqueness in the definition of cata. Commented Jul 8, 2022 at 8:48
• @ColinMcQuillan thanks! I was able to find a solution with your hint. Commented Jul 8, 2022 at 14:11

The solution as per @Colin McQuillan's hint above:

We show that the product $$\langle f, cata(h) \rangle$$ is equal to the catamorphism $$cata(\langle g, h \circ F(outr) \rangle)$$.

By the universal property of catamorphisms, it suffices to show that

$$\langle f, cata(h) \rangle \circ \alpha = \langle g, h \circ F(outr) \rangle \circ F \langle f, cata(h) \rangle$$

On the left, we have

$$\langle f, cata(h) \rangle \circ \alpha = \langle f \circ \alpha, cata(h) \circ \alpha \rangle = \langle g \circ F \langle f, cata(h) , h \circ F (cata(h)) \rangle \rangle$$

Notice that $$F(cata(h)) = F outr \circ F \langle f, cata(h) \rangle$$, so

$$\langle g \circ F \langle f, cata(h) , h \circ F (cata(h)) \rangle \rangle = \langle g \circ F \langle f, cata(h) \rangle, h \circ F outr \circ F \langle f, cata(h) \rangle\rangle = \langle g, h \circ F outr \rangle \circ F \langle f, cata(h) \rangle$$

as needed. $$\blacksquare$$