@MatthewDotty : Strictly speaking, you'd also have to prove that the catamorphism is unique.