universal property of ๐๐๐๐ can be stated as the following equivalence between two definitions for a function ๐ that processes lists: ๐ = ๐ โบ ๐ = ๐๐๐๐ ๐ ๐ ๐ ๐ฅ โถ ๐ฅ๐ = ๐ ๐ฅ ๐ ๐ฅ๐ In the right-to-left direction, substituting ๐ = ๐๐๐๐ ๐ ๐ into the two equations for ๐ gives the recursive definition for ๐๐๐๐ . Conversely, in the left-to-right direction the two equations for g are precisely the assumptions required to show that ๐ = ๐๐๐๐ ๐ ๐ using a simple proof by induction on finite listsโฆ Taken as a whole, the universal property states that for finite lists the function ๐๐๐๐ ๐ ๐ is not just a solution to its defining equations, but in fact the unique solutionโฆ. The universal property of ๐๐๐๐ can be generalised to handle partial and infinite listsโฆ Graham Hutton @haskelhutt ๐๐๐๐ :: ๐ผ โ ๐ฝ โ ๐ฝ โ ๐ฝ โ ๐ผ โ ๐ฝ ๐๐๐๐ ๐ ๐ฃ = ๐ฃ ๐๐๐๐ ๐ ๐ฃ ๐ฅ โถ ๐ฅ๐ = ๐ ๐ฅ ๐๐๐๐ ๐ ๐ฃ ๐ฅ๐