Existence Theorem for Cumulative Universe Towers and Its Applications

Abstract

This paper builds a cumulative tower of Grothendieck universes that provides a precise size discipline for higher type theory. Starting from an increasing sequence of inaccessible cardinals, we give an inductive-recursive definition of universe codes, their decoding functor, and a rank that controls the growth of each code. For every level of the tower we prove closure under dependent products, dependent sums, identity types, and all finite limits and colimits; the colimit part is obtained with a rank-stable quotient constructor. A universe-lifting operation shows strict cumulativity across levels. Assuming propositional resizing at one level, we construct an explicit left adjoint to the inclusion of minus-one truncated types and show that resizing automatically lifts to every higher level. These ingredients combine in an Existence Theorem stating that, over Zermelo-Fraenkel set theory with the chosen inaccessible cardinals, the tower delivers a sound set-theoretic model of higher type theory. The results supply the size infrastructure required for forthcoming work on Rezk completions and higher topos models.