Set quotients in V⁰
Construct set quotients in V⁰.
Given x : V⁰ and a relation R : El⁰ x → El⁰ x → U₀ we have a candiate for an embedding (El⁰ x) / R → V⁰ which sends: [ a ] ↦ sup⁰ (Σ (b : El⁰ x) [a] = [b] ) (f ∘ pr₁)
(Where [-] : El⁰ x ↠ (El⁰ x) / R is the canonical surjection, and f : El₀ x → V⁰ is the embedding part of x)
This embedding would allow us to construct an element x/R : V⁰. But there are a lots of details to check. First that the above is a well-defined map (respects R), and that it is an embedding. Then the pushout is a special case of this, which we construct as a set-quotient of the coproduct.
This type: Σ (b : El⁰ x) [a] = [b] represents the equivalence class of a in El⁰ x. So, no need to carve the equivalences classes out of the powerset.