You can encode maybe as well

It is the famous Landin's knot.

WTF... lol

It will be great if someone translate this to OCaml or any strict language, because the y combinator will mysteriously broke.
That will be a great lesson for anyone writing Definitional Interpreter - they share MetaLanguage characteristic, even sometimes unintentionally.
HOAS is another great example of the Object Language sharing the same characteristic of the MetaLanguage.

Haskell is HM (at least without wrapping), and UTLC is untyped. If you try to translate this kata to use plain haskell errors will show up.
For one you cant type the Y Combinator because it is recursive-typed. You do recursive type in Haskell by wrapping.
Peano Arithmetic also need System-F to type, and Rank Polymorphism have to be done... By wrapping again.

this is inefficient because init x is O(n). The O(n) thunk wont beat the O(n^2) total init cost.

I only maintain the haskell version. Can you update it yourself?

I am not very good with cat theory. I dont see how it can help, maybe you can point me to some example?

Resolving manually

it should never panic. isomorphism is an mathematical concept, that require you to map every single input to some valid output. panic is not a valid output.

This is the power of type driven programming.
refl is always a = a, b = b, c = c, etc. it is the isoPow/isoS/isoEither/isoTrans that get them into the right place.

tql,wsl

Can you add last and weaken in the description? I had reimplemented them, and if I know them I dont need to.

Because it is not hard?

Figure it out, maybe you should talk about idris module (public export) a bit as it is confusing for ppl coming from other language