Fascinating! A couple of questions:

Are there any non-singleton sets with the fixpoint property?

> a ↦ f (e a a)

Don't you mean

   a ↦ e a a

? Because later you expand (g a0) to (e a0 a0).