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

\(\mathcal {S}(\Omega ,i)\rightarrow \mathord {\textnormal {\textsf {G}}}_{1}\pitchfork \mathcal {U}(i)\) induced by the morphism \(\bot \rightarrow \top \) in \(\Omega \) is an equivalence.