Existence Theorem for Cumulative Universe Towers and Its Applications

TL;DR

This paper constructs a cumulative tower of Grothendieck universes with precise size control, enabling a sound set-theoretic model of higher type theory and supporting advanced higher categorical structures.

Contribution

It introduces a new cumulative tower of universes with inductive-recursive codes, closure properties, and size control, facilitating models of higher type theory.

Findings

Proves closure under dependent types and limits at each universe level.

Establishes strict cumulativity and resizing properties across levels.

Provides a set-theoretic foundation for higher type theory models.

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.