Direct tree-fold information obstruction (source code)

= Direct tree-fold information obstruction

A direct <tree fold> gives a parent operation only its children's folded summaries. If two different children have equal summaries, the parent cannot distinguish them. For a <leaf-labelled binary tree>, a function returning proper <subtrees> maps every leaf to `[]`. A direct fold with precisely that result type would therefore map every two-leaf tree to the same result, despite their possibly different labels. This rules out that direct fold, while permitting a richer folded summary followed by projection.