I think the problem is hidden beneath the fixed point operator (I've edited the code to be more correct). For Id, is there actually a type Psi such that Psi <~> (Id[Psi] => A)? Isn't that where the Y combinator comes in - the only reason loeb is able to act as a Y combinator is that it gets one passed in via the fixed point lemma? Isn't a fixed point lemma always going to be the same as a Y combinator?
(I wish we were working with a proof that didn't invoke this external lemma)
I asked the folks on /r/haskell, we hashed out a version in Agda and then I translated it into Haskell. It's not completely in the spirit of the original question, but at least it's a starting point. The code is here, you can try it out on CompileOnline.
ETA: now I also wrote a post about it.
If it's worth saying, but not worth its own post (even in Discussion), then it goes here.
Notes for future OT posters:
1. Please add the 'open_thread' tag.
2. Check if there is an active Open Thread before posting a new one. (Immediately before; refresh the list-of-threads page before posting.)
3. Open Threads should be posted in Discussion, and not Main.
4. Open Threads should start on Monday, and end on Sunday.