Lang.quotient

-- The smallest quotient: ℕ collapsed by the total relation ∥𝟙∥.
-- Basic quotient-type facts. Relations are Ω-valued (docs/NovaFoundation.txt),
-- so the total relation is the squash ∥𝟙∥.

collapse : class Z ≡ class (S Z) ∈ ℕ / (n m. ∥𝟙∥)
collapse = ⋆

collapseElim : (q : ℕ / (n m. ∥𝟙∥)) → quot-elim (x. ℕ) (a. Z) (class Z : ℕ / (n m. ∥𝟙∥)) ≡ Z
collapseElim = λq. ⋆