1) Assume the existence of one particular fixpoint. That’s what I’ve done in the post.
2) Assume the existence of fixpoints for all formulas with one propositional variable, and get (1) as an immediate corollary. That’s not straightforward in Haskell because there are no type-level lambdas, but it’s easy in Agda.
3) Actually spell out a proof of (2), which is known as the diagonal lemma. You could probably do that in Agda, but I haven’t tried and haven’t seen anyone try. Also it’s not obvious which assumptions to use. Ideally we’d want a full account of Gödel numberings, but that would be a lot of work.
You can choose how deep you want to go:
1) Assume the existence of one particular fixpoint. That’s what I’ve done in the post.
2) Assume the existence of fixpoints for all formulas with one propositional variable, and get (1) as an immediate corollary. That’s not straightforward in Haskell because there are no type-level lambdas, but it’s easy in Agda.
3) Actually spell out a proof of (2), which is known as the diagonal lemma. You could probably do that in Agda, but I haven’t tried and haven’t seen anyone try. Also it’s not obvious which assumptions to use. Ideally we’d want a full account of Gödel numberings, but that would be a lot of work.