A base type theory is a type theory that has the unit type, pair types, identity types, function types, inductive types, and a univalent universe \(\mathcal {U}(i):\mathord {\textnormal {\textsf {Type}}}(\mathord {\textnormal {\textsf {succ}}}(i))\) that represents \(\mathord {\textnormal {\textsf {Type}}}(i)\) for every \(i:\mathord {\textnormal {\textsf {Level}}}\).