Well, cooperating in the Prisoner's Dilemma against an identical agent is a simple special case of UDT reasoning, and people are writing math papers about it as you can see. Besides, if UDT is trivial, how come it has unsolved problems? Off the top of my head: spurious proofs, agent simulates predictor, logical uncertainty... The fact that already solved problems look trivial isn't strong evidence to me, because I know how much effort it takes to get something like Counterfactual Mugging from the "impossible" pile into the "trivial" pil...
About a month ago I accidentally found out that the LW idea of quining cooperation is already studied in academia:
1) Moshe Tennenholtz's 2004 paper Program Equilibrium describes the idea of programs cooperating in the Prisoner's Dilemma by inspecting each other's source code.
2) Lance Fortnow's 2009 paper Program Equilibria and Discounted Computation Time describes an analogue of Benja Fallenstein's idea for implementing correlated play, among other things.
3) Peters and Szentes's 2012 paper Definable and Contractible Contracts studies quining cooperation over a wider class of definable (not just computable) functions.
As far as I know, academia still hasn't discovered Loebian cooperation or the subsequent ideas about formal models of UDT, but I might easily be wrong about that. In any case, the episode has given me a mini-crisis of faith, and a new appreciation of academia. That was a big part of the motivation for my previous post.