Core.quotEffective

-- EFFECTIVITY of the quotient: what does class a ≡ class b give back?
--
-- Not r a b. ≐ is an equivalence at every judgement (NovaFoundation.txt,
-- EQUIVALENCE RULES) while (/) quotients by an ARBITRARY Ω-valued
-- relation (ty-quot), so class equality is closed under symmetry and
-- transitivity whether or not r is — reversing el-quot-eq pointwise
-- would be inconsistent (the successor graph at the end of this file
-- collapses ℕ; NovaFoundation.txt's Ω block spells the damage out).
--
-- What comes back is the equivalence CLOSURE r⁺ — Core/prop.nova's
-- rClosure, the impredicative intersection of every equivalence
-- containing r — and it comes back exactly: quotient equality IS r⁺
-- (classEqIff). Effectivity on the nose is the corollary at an
-- equivalence r (effectiveAtEquiv), since there r⁺ is no coarser than
-- r. el-quot-eq at an ARBITRARY relation: the witness is supplied
-- (e-star-quot-wit), so the relation's shape is irrelevant — no
-- ∥𝟙∥/≡-shape restriction, and r may be a variable

import Core.prop (rClosure, rClosureContains, rClosureRefl, rClosureSymm, rClosureTrans, rClosureLeast, propExt, ↔, iffIntro)
import Core.equality (transportP, sym, trans)

classEqOfRel : {A : 𝕌} (r : A → A → Ω) (x y : A) → r x y → class x ≡ class y ∈ A / (u v. r u v)
classEqOfRel = λA r x y h. ⋆ h

-- ⟸ : class equality is an equivalence relation containing r, and r⁺ is
-- the LEAST such, so r⁺ implies it. No quotient elimination here —
-- leastness does all the work
classEqOfClosure : {A : 𝕌}
  (r : A → A → Ω)
  (a b : A)
  → rClosure r a b → class a ≡ class b ∈ A / (u v. r u v)
classEqOfClosure =
  λA r. rClosureLeast
    r
    λx y. class x ≡ class y ∈ A / (u v. r u v)
    λx y h. classEqOfRel r _ _ h
    λx. ⋆
    λx y z h1 h2. trans _ _ _ h1 h2
    λx y h. sym _ _ h

-- r⁺ a ⋅ respects r, so it factors through the class map. The
-- well-definedness goal is an Ω-EQUATION between two closure
-- instances — propositional extensionality, both implications from r⁺'s
-- own transitivity and symmetry. Nothing about r is assumed
clsRelWd : {A : 𝕌} (r : A → A → Ω) (a : A) {x y : A} → r x y → rClosure r a x ≡ rClosure r a y
  using (Core.prop.rClosure.eq, Core.prop.rClosure.unfold)
clsRelWd =
  λA r a x y h. propExt
    λk. rClosureTrans k (rClosureContains _ _ _ h)
    λk. rClosureTrans k (rClosureSymm (rClosureContains _ _ _ h))

-- the descent itself: quot-elim at the CONSTANT MOTIVE Ω. clsRelWd
-- above discharges its well-definedness obligation
clsRel : {A : 𝕌} (r : A → A → Ω) (a : A) → (A / (u v. r u v)) → Ω using (clsRelWd)
clsRel = λA r a q. quot-elim (x. rClosure r a x) q

-- ⟹ : EFFECTIVITY. clsRel a (class a) ≜ r⁺ a a holds by reflexivity of
-- the closure, and the class equation transports it to b — el-quot-beta
-- on both ends, congruence in between
effective : {A : 𝕌}
  (r : A → A → Ω)
  (a b : A)
  → (class a ≡ class b ∈ A / (u v. r u v)) → rClosure r a b
  using (Core.prop.rClosure.eq, Core.prop.rClosure.unfold, Core.quotEffective.clsRel.eq)
effective = λA r a b h. transportP (clsRel r a) h (rClosureRefl r a)

-- the characterization: quotient equality is exactly r⁺
classEqIff : {A : 𝕌}
  (r : A → A → Ω)
  (a b : A)
  → (class a ≡ class b ∈ A / (u v. r u v)) ↔ rClosure r a b
classEqIff = λA r a b. iffIntro (effective r a b) (classEqOfClosure r a b)

-- COROLLARY: at an equivalence relation, effectivity on the nose — r
-- itself is an equivalence containing r, so leastness collapses r⁺ into
-- it. This is the rule one wanted, with the hypotheses that make it true
effectiveAtEquiv : {A : 𝕌}
  (r : A → A → Ω)
  → ((x : A) → r x x)
    → ((x y z : A) → r x y → r y z → r x z)
      → ((x y : A) → r x y → r y x) → (a b : A) → (class a ≡ class b ∈ A / (u v. r u v)) → r a b
effectiveAtEquiv =
  λA r rRefl rTrans rSymm a b h. rClosureLeast
    _
    r
    λx y k. k
    rRefl
    rTrans
    rSymm
    _
    _
    effective r _ _ h

-- an instance of the corollary: ℕ by its own equality. The three
-- equivalence premises are each one ⋆ — reflection makes them
-- judgemental
natEq : ℕ → ℕ → Ω
natEq = λx y. x ≡ y

natEqEffective : {a b : ℕ} → (class a ≡ class b ∈ ℕ / (u v. natEq u v)) → a ≡ b
  using (hyp.rw, Core.quotEffective.natEq.eq, Core.quotEffective.natEq.unfold)
natEqEffective = effectiveAtEquiv natEq (λx. ⋆) (λx y z h1 h2. ⋆) (λx y h. ⋆)

-- and the refutation, kept as evidence: at the successor graph — not an
-- equivalence — the one-hop equation holds by el-quot-eq, the two-hop
-- one by transitivity through it, and the BACKWARD one by symmetry. A
-- rule reading r off any of the last two would inhabit
-- (S Z ≡ S (S Z) ∈ ℕ) and collapse ℕ. (Chaining is not automatic:
-- sgHop2 goes through sgHop1 as a rewrite candidate, so the hops must
-- be named — drop sgHop1 and sgHop2 stops elaborating)
SG : 𝕌
SG = ℕ / (n m. S n ≡ m)

sgHop1 : class Z ≡ class (S Z) ∈ SG using (Core.quotEffective.SG.unfold)
sgHop1 = ⋆

sgMid : class (S Z) ≡ class 2 ∈ SG using (Core.quotEffective.SG.unfold)
sgMid = ⋆

sgHop2 : class Z ≡ class 2 ∈ SG using (Core.quotEffective.SG.unfold, sgHop1, sgMid)
sgHop2 = trans _ _ _ sgHop1 sgMid

sgBack : class (S Z) ≡ class Z ∈ SG using (Core.quotEffective.SG.unfold, sgHop1)
sgBack = ⋆