HoTT book, 3.5 and Predicative Aspects of Order Theory in Univalent Foundations. Effectively a way to recover impredicativity from a predicative theory by making the following map an equivalence.
\[ \textsf{Prop}_{\mathcal{U}_i} \rightarrow \textsf{Prop}_{\mathcal{U}_{i + 1}} \]