Assuming enough Universes [008L]

We will assume that for every finite list of of types in context trough there exists a universe that contains these types. See Postulate 6.2.1 in Introduction to Homotopy Type Theory