Does univ : univ always lead to a contradiction in a dependently typed language? I am currently following Checking Dependent Types with Normalization by Evaluation: A Tutorial by David Christiansen, where we consider the type of U (the universe of types) to be U itself [this can be seen section 7.4.1 in the implementation of synth where we have ['U (go '(the U U))]: That is, the untyped expression U is elaborated into the expression U of type U. Effectively, we have taken that Univ : Univ.
This cannot happen in ZFC due to the axiom of foundation. I suspect type-inferring U as having type U is inconsistent. I do not know how to prove this; I would attempt to encode a Russell-style paradox if I were pressed to produce a proof.

Is it really true that U : U is inconsistent?
Is it possible to write a term that produces a proof of False assuming U : U? Or is the encoding to large to write down easily &quot;by hand&quot;, but can be believed to be done?
If U : U is not inconsistent (i.e., is consistent), then a couple of words on why the dependently typed world allows for U : U while ZFC cannot allow U ∈ U would be appreciated.

I understand that talking about &quot;dependently typed languages&quot; is broad enough to be senseless. As a beginner, I find it hard to restrict to one theory, because I don't know the trade-offs between the theories. For the sake of the answer, please feel free to restrict to, say, MLTT, or CoC, or LF.
U : U is inconsistent in a wide variety of settings. It is safe to say that it's inconsistent in any type theory. Deriving False from it is feasible by hand. The simplest version of this is called Hurkens' paradox:

Original source
Coq implementation.
Agda implementation.

The Coq source additionally describes the sufficient conditions for getting False. In short, we don't need U : U, it's enough to have two universes, where one is contained in the other, and both are closed under impredicative function types.