Qiit.quot

-- The quotient, SUBSUMED GENERICALLY (docs/NovaFoundation.txt,
-- IDENTITY note): the signature for A / R over its full ambient
-- Γ = [a : 𝕌][r : a → a → Ω] — an arbitrary carrier and an
-- arbitrary Ω-valued relation, cls x ≡ cls y imposed under (r x y).

data [a : 𝕌] [r : a → a → Ω]
  Q : U
  cls : a → El Q
  qeq : (x : a) (y : a) → r x y → cls x ≡ cls y ∈ El Q

-- the GENERIC QUOTIENT LIFT: a function out of the quotient, from a
-- function on the carrier plus a respect proof — quot-elim's f/f⁼ at
-- full generality. Coherences are hypotheses, so the coherence
-- argument IS the caller's respect proof, passed straight through.
qlift : (a : 𝕌)
  (r : a → a → Ω)
  {b : 𝕌}
  (f : a → b)
  (resp : (x y : a) → r x y → f x ≡ f y)
  → Q _ r → b
  using (Qiit.quot.Q.unfold)
qlift = λa r b f resp q. QElim a r (λw. b) (λx. f x) (λx y h. resp x y h) q

qliftBeta : (a : 𝕌)
  (r : a → a → Ω)
  (b : 𝕌)
  (f : a → b)
  (resp : (x y : a) → r x y → f x ≡ f y)
  (x : a)
  → qlift _ (λy z. r y z) f resp (cls a r x) ≡ f x
  using (Qiit.quot.Q.eq, Qiit.quot.QElim.eq, Qiit.quot.cls.eq, Qiit.quot.qlift.eq)
qliftBeta = λa r b f resp x. ⋆

-- instance: ℕ quotiented by squashed equality; toNat is one qlift
eqN : ℕ → ℕ → Ω
eqN = λx y. x ≡ y

toNat : Q _ eqN → ℕ using (Qiit.quot.Q.unfold, Qiit.quot.eqN.unfold)
toNat = λq. qlift _ _ (λx. x) (λx y h. ⋆) q

toNatCls : toNat (cls ℕ eqN (S Z)) ≡ S Z
  using (Qiit.quot.Q.eq,
    Qiit.quot.QElim.eq,
    Qiit.quot.cls.eq,
    Qiit.quot.eqN.eq,
    Qiit.quot.qlift.eq,
    Qiit.quot.toNat.eq)
toNatCls = ⋆