qiitQuot

-- The quotient, SUBSUMED GENERICALLY (docs/NovaFoundation.txt,
-- IDENTITY note): the signature for A / R over its full ambient
-- Γ = [a : 𝕌][r : El a → El a → Ω] — an arbitrary carrier and an
-- arbitrary Ω-valued relation, cls x ≡ cls y imposed under Prf (r x y).
data [a : 𝕌] [r : El a → El a → Ω]
     ( Q : U
     ; cls : El a → El Q
     ; qeq : (x : El a) (y : El a) → Prf (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.
def qlift : (a : 𝕌) (r : El a → El a → Ω) (b : 𝕌)
            (f : El a → El b)
            (resp : (x : El a) (y : El a) → Prf (r x y) → f x ≡ f y ∈ _)
            → El (Q _ r) → El b ≔
  λa. λr. λb. λf. λresp. λq.
    QElim a r (λw. b) (λx. f x) (λx. λy. λh. resp _ _ h) q

def qliftBeta : (a : 𝕌) (r : El a → El a → Ω) (b : 𝕌)
                (f : El a → El b)
                (resp : (x : El a) (y : El a) → Prf (r x y) → f x ≡ f y ∈ El b)
                (x : El a) → qlift _ _ _ f resp (cls _ r x) ≡ f x ∈ El b ≔
  λa. λr. λb. λf. λresp. λx. ⋆

-- instance: ℕ quotiented by squashed equality; toNat is one qlift
def eqN : El ℕ → El ℕ → Ω ≔ λx. λy. (x ≡ y ∈ _)

def toNat : El (Q _ eqN) → ℕ ≔
  λq. qlift _ eqN _ (λx. x) (λx. λy. λh. ⋆) q

def toNatCls : toNat (cls _ eqN (S Z)) ≡ S Z ∈ _ ≔ ⋆