Girard's paradox

In mathematical logic, System U and System U⁻ are pure type systems, i.e. special forms of a typed lambda calculus with an arbitrary number of sorts, axioms and rules (or dependencies between the sorts). They were both proved inconsistent by Jean-Yves Girard in 1972. This result led to the realization that Martin-Löf's original 1971 type theory was inconsistent as it allowed the same "Type in Type" behaviour that Girard's paradox exploits.

System U is defined as a pure type system with

System U⁻ is defined the same with the exception of the ${\displaystyle (\triangle ,\ast )}$ rule.

The sorts ${\displaystyle \ast }$ and ${\displaystyle \square }$ are conventionally called “Type” and “Kind”, respectively; the sort ${\displaystyle \triangle }$ doesn't have a specific name. The two axioms describe the containment of types in kinds (${\displaystyle \ast :\square }$) and kinds in ${\displaystyle \triangle }$ (${\displaystyle \square :\triangle }$). Intuitively, the sorts describe a hierarchy in the nature of the terms.

...
Wikipedia