-- The universe code for quotient types and its El-decoding.
-- (ℕ / r) ≐ ℕ / r is definitional (the Ω-valued relation passes
-- through undecoded), so a variable of the code's moves to the
-- decoded quotient with no coercion.
qdecode : (v : ℕ / (x y. ∥ℕ∥)) → ℕ / (x y. ∥ℕ∥)
qdecode = λv. v
qcode : 𝕌
qcode = ℕ / (x y. ∥ℕ∥)