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](https://www.fing.edu.uy/~amiquel/publis/these.pdf). 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.*](https://www.fing.edu.uy/~amiquel/publis/types04.pdf).

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 perspicuous.

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 impredicative 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.