« Root

Reference. Introduction to Homotopy Type Theory [008M]

by Egbert Rijke.

Backlinks

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