In dependent type theory, having a type of all types results in various paradoxes, such as Russell's paradox and Girard's paradox. There are two ways to resolve this issue. One way is to simply add a universe of small types and accept that not all types are small. On the other hand, one can use a hierarchy of universes or universe hierarchy and postulate that every type is an element of universes in this universe hierarchy: Given an universe level , each type universe consists of only the...