quottyuniv

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