Let \(T\) be a base type theory. We work in \(T\). Let \(i:\mathord {\textnormal {\textsf {Level}}}\).

• -The function \(\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}:\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}(\mathcal {E}(i))\rightarrow \mathcal {U}(\mathord {\textnormal {\textsf {succ}}}(i))\) factors through \(\mathcal {U}(i)\).
• -Let \(A:\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}(\mathcal {E}(i))\). Then the counit of the adjunction \(\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}\dashv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}\) at \(A\) is an equivalence.
• -Let \(A:\mathcal {U}(i)\). Then the unit of the adjunction \(\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}\dashv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}\) at \(A\) is an equivalence.

In short, the adjunction \(\mathord {\textnormal {\textsf {C}}}_{\mathord {\textnormal {\textsf {Sp}}}}\dashv \mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}\) restricts to an equivalence \(\mathord {\textnormal {\textsf {GS}}}_{\mathord {\textnormal {\textsf {Sp}}}}(\mathcal {E}(i))\simeq \mathcal {U}(i)\) of categories.