[zozbot234]

You can always add axioms to improve logical strength. For example, one common approach for dealing with size issues in set theory is positing so-called 'inaccessible cardinals' which amount to something quite similar to the 'universes' of type theory.

[cwzwarich]

Adding axioms to simple type theory is more awkward than adding them to a set theory like ZFC. One approach to universes I’ve seen in Isabelle/HOL world is to postulate the existence of a universe as a model of set theory. But then you’re stuck reasoning semantically about a model of set theory. Nobody has scaled this up to a large pluralist math library like Mathlib.