PREDICATIVITY!!

Last night I was tired and went to bed early, so I got up in five this morning and tried to prove the Greedy Theorem in AoPA. The type of the theorem was spelled out without obstacles, and the Eilenberg-Wright lemma is automatically applied in AoPA. It was after I typed in "foldR-fusion (min R)" did I realise that the foldR-fusion theorem is not applicable, due to our annoying friend predicativity yet again! I started to wonder whether some book in the future would state that

After Russell proposed his paradox and Gödel proved his two incompleteness theorems, logicians and type theorists were so afraid of self-references that they introduced predicativity and universe hierarchy to try to defeat their enemy once and for all. The big weapon successfully destroyed self-references but also made the programmers' life really miserable. Fortunately, ...

Unfortunately it is not possible to know what follows the word "fortunately". Back to reality, maybe we can prove the Greedy Theorem by the Hylomorphism Theorem instead? If this doesn't work, the remaining two ways would be inventing another version of the fusion theorem or conducting a traditional brute-force proof, both of which are definitely not appealing.

--
And I think AoPA wouldn't be that usable and reusable if the problem of predicativity doesn't get solved...