I feel like most of my posts on mathoverflow and cstheory.stackexchange consist of this answer, but the most perspicuous (in my opinion) proof of inconsistency of U and $*:*$ is a construction by Alexandre Miquel, given in his phd dissertation. Tragically, it is in French, so I'll summarize the idea below, and maybe you'll be able to fill in the remainder using his other paper lamda-Z: Zermelo's Set Theory as a PTS with 4 Sorts..
The idea is to build a model of naive set theory in $*:*$. The naive theory allows for unrestricted comprehension, and in particular the paradox falls out quite easily. The proof term of $\bot$ itself is longer than in Hurkens' presentation, but I think it's safe to say that the process is at least more straightforward.
The crucial idea is to model a set as a directed pointed graph. The point represents the set, the graph contains all the members of the set, and the membership relation is represented by the edges. We rely on the encoding of $\Sigma$ types in the impredicative theories.
A set $S$ is thus an element of
$$\mathrm{Set}=\Sigma (A:*)(x :A)(R:A\rightarrow A\rightarrow *) $$
where the carrier is $A$, the base is $x$ and the edge relation is $R$. What's a bit counter-intuitive is that sets are not necessarily well-founded. To get sane notions of equality and membership, we need to define equality as bisimilarity $\simeq$ of pointed graphs.
Then it's pretty easy to define membership: $S\in T$ if
- $T = (A, x, R)$
- There is some $y$ with $R\ y\ x$ ($y$ is an element of $x$)
- $S\simeq (A, y, R)$ ($S$ is the "same set" as $y$)
Then we can show:
For each predicate $P:\mathrm{Set}\rightarrow *$ that respects bisimilarity there is a set $$ \{\ x\ |\ P(x)\ \}$$
It's then easy to show that $P(x)=x\notin x$ respects bisimilarity.