Is a type theory with an infinite descending hierarchy ... : U₋₂ : U₋₁ : U₀ of universes consistent? Maybe set theorists have come up with an anti-foundation set theory that an infinite descending chain of models of set theory?
Conversation
This stuff is well beyond me but I remember “Dependently typed lambda calculus with a lifting operator” by Rouhling (under the supervision of Coquand) drouhling.github.io/data/internshi mentioned something about levels over ℤ and the challenges.
1
“Let us however remark that it is unclear whether we can define a model for such a hierarchy, since the absence of a bottom universe forbids the usual inductive-recursive definitions.” – assuming that this is not news to you or all that helpful from the little I understand 😅