Universe hierarchy (Russell)

Layer 0 — Mathematicsin the Type Theory subtree

Russell-style universes Type_0 : Type_1 : Type_2 : ...; avoids Girard-Hurkens paradox of Type:Type; cumulative or non-cumulative variants in Coq, Agda, Lean.