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 : Uis inconsistent?
- Is it possible to write a term that produces a proof of
U : U? Or is the encoding to large to write down easily "by hand", but can be believed to be done?
U : Uis not inconsistent (i.e., is consistent), then a couple of words on why the dependently typed world allows for
U : Uwhile ZFC cannot allow
U ∈ Uwould be appreciated.
I understand that talking about "dependently typed languages" 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.