[proofplan] We isolate the fragment of $T$ consisting of one Russell-style universe $\mathcal U$ with $\mathcal U : \mathcal U$ and dependent products closed in $\mathcal U$. In the first step we define $\lambda^\ast$ to be the one-sort pure type system with the axiom $*:*$ and product rule $(*,*,*)$, and we interpret it in $T$. The Girard-Hurkens paradox theorem for this pure type system gives a closed polymorphic contradiction term of type $\prod_{C:*} C$. We verify that the hypotheses of that paradox are exactly supplied by the stated rules of $T$, translate that closed term into $T$, and then apply it to the small empty type $\varnothing : \mathcal U$. [/proofplan] [step:Identify the type-in-type pure type system inside $T$] Let $\lambda^\ast$ denote the pure type system with one sort $*$, one axiom \begin{align*} * : *, \end{align*} and one product rule \begin{align*} (*,*,*), \end{align*} meaning that if $A$ is a type at sort $*$ and $B$ is a type at sort $*$ in context extended by $x:A$, then $\prod_{x:A}B(x)$ is again a type at sort $*$. We interpret this system in $T$ by sending the unique sort $*$ to the universe $\mathcal U$, sending variables to variables, sending dependent products in $\lambda^\ast$ to dependent products in $T$, and sending lambda abstraction and application to the corresponding dependent product introduction and elimination operations in $T$. This interpretation is well defined because $T$ has the ordinary structural rules, substitution, dependent product formation, dependent product introduction, dependent product elimination, and judgmental beta-conversion. The axiom $* : *$ is interpreted as the assumed judgment \begin{align*} \vdash \mathcal U : \mathcal U. \end{align*} The product rule $(*,*,*)$ is interpreted as the assumed closure of $\mathcal U$ under dependent products. [guided] The point of this step is to make precise which part of $T$ is responsible for the contradiction. We define the source system $\lambda^\ast$ to have exactly one universe-like sort $*$, with the self-typing axiom \begin{align*} * : *, \end{align*} and with dependent products allowed from $*$-small domains and $*$-small codomains back into $*$. We now define an interpretation of $\lambda^\ast$ in $T$. The sort $*$ is interpreted as the term $\mathcal U$. A context \begin{align*} x_1:A_1,\dots,x_n:A_n \end{align*} of $\lambda^\ast$ is interpreted as the corresponding context in $T$, with every type expression translated recursively. Variables are interpreted by the same variables. A product expression \begin{align*} \prod_{x:A}B(x) \end{align*} is interpreted as the dependent product in $T$ formed from the translations of $A$ and $B(x)$. A lambda abstraction is interpreted by the dependent product introduction rule of $T$, and an application is interpreted by the dependent product elimination rule of $T$. We must check that each rule of $\lambda^\ast$ is respected. The axiom $*:*$ is respected because the theorem assumes \begin{align*} \vdash \mathcal U : \mathcal U. \end{align*} The product rule is respected because the theorem assumes that, whenever \begin{align*} \Gamma \vdash A : \mathcal U \end{align*} and \begin{align*} \Gamma,x:A \vdash B(x) : \mathcal U, \end{align*} one can derive \begin{align*} \Gamma \vdash \prod_{x:A}B(x) : \mathcal U. \end{align*} The term-forming rules are respected because the statement includes the usual dependent product introduction and elimination rules. Substitution and beta-conversion are respected because these are included among the structural and judgmental equality rules of $T$. Thus every derivation in $\lambda^\ast$ translates into a derivation in $T$. [/guided] [/step] [step:Invoke the Girard-Hurkens paradox for the interpreted fragment] We use the Girard-Hurkens paradox theorem in its one-sort pure type system form: in the pure type system $\lambda^\ast$ with $*:*$ and the product rule $(*,*,*)$, there is a closed term \begin{align*} \Omega : \prod_{C:*} C. \end{align*} This is the precise external result used in the proof: its conclusion is the closed polymorphic contradiction term displayed above, not merely an abstract statement that the system is inconsistent. The previous step verifies the hypotheses needed to interpret every $\lambda^\ast$ derivation in $T$: the sort axiom is interpreted by $\vdash \mathcal U : \mathcal U$, the product rule is interpreted by closure of $\mathcal U$ under dependent products, and the term rules are interpreted by the dependent product introduction, elimination, substitution, conversion, and beta-conversion rules of $T$. Therefore the closed derivation of $\Omega$ translates to a closed term \begin{align*} \omega : \prod_{C:\mathcal U} C. \end{align*} [guided] The decisive external input is not that every closed type of $T$ is automatically inhabited. The precise Girard-Hurkens conclusion used here is stronger and more structured inside the type-in-type fragment itself: the one-sort pure type system $\lambda^\ast$, with axiom $*:*$ and product rule $(*,*,*)$, derives a closed polymorphic term \begin{align*} \Omega : \prod_{C:*} C. \end{align*} This is the exact paradox theorem being invoked. It says that, from the self-typing sort $*:*$ and impredicative dependent products over that same sort, the paradox constructs a function sending each small type $C$ to an element of $C$. We now check that this theorem applies to the interpreted fragment of $T$. The source sort $*$ is interpreted as $\mathcal U$, and the axiom $*:*$ is interpreted by the stated judgment \begin{align*} \vdash \mathcal U : \mathcal U. \end{align*} The source product rule $(*,*,*)$ is interpreted by the stated closure rule for $\mathcal U$: if \begin{align*} \Gamma \vdash A : \mathcal U \end{align*} and \begin{align*} \Gamma,x:A \vdash B(x) : \mathcal U, \end{align*} then \begin{align*} \Gamma \vdash \prod_{x:A}B(x) : \mathcal U. \end{align*} The lambda abstraction, application, substitution, conversion, and beta-conversion steps occurring in the Girard-Hurkens derivation are interpreted by the corresponding rules assumed for $T$. Hence the closed term $\Omega$ translates to a closed term \begin{align*} \omega : \prod_{C:\mathcal U} C \end{align*} in $T$. [/guided] [/step] [step:Instantiate the paradox with the empty type] The theorem assumes that $\varnothing$ is a closed empty type of $T$ and that it is small: \begin{align*} \vdash \varnothing : \mathcal U. \end{align*} Since $\omega$ has type $\prod_{C:\mathcal U}C$, the dependent product elimination rule applies to $\omega$ at the argument $\varnothing$. Define \begin{align*} t := \omega(\varnothing). \end{align*} The elimination rule gives the closed judgment \begin{align*} \vdash t : \varnothing. \end{align*} This is exactly the asserted inconsistency of $T$. [/step]