Note about universes

[Russoul]

The standard construction of universes a la Tarski is sometimes considered the only formal definition of universes in type theory.
One problem of working with them is that we have El : Tm Γ 𝕌 → Ty Γ but no inverse. Lack of inverse is sensible and is used to sidestep a paradox. That implies that we can't formally omit El, when working with universes. There seems to be a nice alternative to standard universes though: universes a la Coquand a la Tarski.
We have an indexed statement: Tmᵢ₊₁ Γ 𝕌 ≅ Tyᵢ Γ. That is, El now has an inverse. But what's even nicer about them is that we can now ask for stricter: Tmᵢ₊₁ Γ 𝕌 ≡ Tyᵢ Γ hence formally justifying Russell-style universes.