Paramorphisms

Paramorphisms correspond to the concept of primitive recursion. A paramorphism can be defined in terms of products and catamorphisms

or characterised by the universal property

It is a (strict) specialisation of the generalised tupling transformation mentioned before. I didn't get the statement about generalised tupling precise enough at the beginning, so I was confused by why the universal property of paramorphisms can be a bidirectional implication, until I realised that the statement of general tupling can be proven to be bidirectional:

Once the full-fledged tupling rule is established, the universal property of paramorphisms follows as an easy corollary since id = cata α.

--
It took me more time than I expected...