The "attach" trick for quotients?

Stream: general

[mniip]

Analogously to, say, List.attach, it's possible to define Quotient.attach with the following type:

def Quotient.attach {r : Setoid α} (q : Quotient r) : Trunc { x // ⟦x⟧ = q }
  := sorry

Normally when eliminating a quotient we have to show that the continuation is "proper" on its entire domain (Quotient.lift), but with the "attach" trick we can weaken this assumption to only things that are equivalent to the actual value we're eliminating:

def Quotient.lift_attached {r : Setoid α} (q : Quotient r)
  (f : α → β) (proper : ∀ x y, ⟦x⟧ = q → ⟦y⟧ = q → f x = f y)
  : β
  := q.attach.lift (λt => f t.1) $ by
    intro ⟨_, _⟩ ⟨_, _⟩
    dsimp only
    apply proper <;> assumption

We can get even lazier and only relate it to q.out:

def Quotient.lift_attached' {r : Setoid α} (q : Quotient r)
  (f : α → β) (proper : ∀ x, r x q.out → f x = f q.out)
  : β
  := q.attach.lift (λt => f t.1) $ by
    intro ⟨x, _⟩ ⟨y, _⟩
    dsimp only
    rw [proper x, proper y]
    . exact Quotient.mk_eq_iff_out.mp ‹_›
    . exact Quotient.mk_eq_iff_out.mp ‹_›

Here's a possible implementation:

Implementation

import Mathlib.Data.Quot

instance Setoid.Attached {r : Setoid α} (q : Quotient r)
  : Setoid { x // ⟦x⟧ = q } where
  r := λa b => r.r a.1 b.1
  iseqv :=
    { refl := λ_ => r.iseqv.refl _
    , symm := r.iseqv.symm
    , trans := r.iseqv.trans
    }

def Quotient.fib_attach
  : Quotient r → (q : Quotient r) × Quotient (r.Attached q)
  := Quotient.lift (λx => ⟨⟦x⟧, Quotient.mk _ ⟨x, rfl⟩⟩) $ by
    dsimp only [HasEquiv.Equiv]
    intro x y _
    have e : ⟦x⟧ = ⟦y⟧ := Quot.sound ‹_›
    calc
      _ = ⟨⟦y⟧, Quotient.mk _ ⟨x, e⟩⟩ := by
        generalize ⟦y⟧ = q at *
        subst e
        rfl
      _ = _ := by
        apply congrArg
        apply Quotient.sound
        assumption

def Quotient.fib_attach_eq : (fib_attach q).1 = q
  := q.ind (motive:=λq => (fib_attach q).1 = q) λ_ => rfl

def Quotient.attach {r : Setoid α} (q : Quotient r) : Trunc { x // ⟦x⟧ = q }
  := (Quotient.fib_attach_eq ▸ q.fib_attach.2).lift Trunc.mk $ by
    intro _ _ _
    apply Trunc.eq

It has some nice definitional equality properties:

def Quotient.lift_attached_eq : ⟦x⟧.lift_attached f p = f x
  := rfl

def Quotient.lift_attached'_eq : ⟦x⟧.lift_attached' f p = f x
  := rfl

This looked pretty remarkable to me.

[Eric Wieser]

I think your first example can be shortened with docs#Quotient.recOnSubsingleton

[mniip]

Actually it's the implementation of Quotient.attach that can be greatly simplified using recOnSubsingleton indeed:

def Quotient.attach {r : Setoid α} (q : Quotient r) : Trunc { x // ⟦x⟧ = q }
  := q.recOnSubsingleton λx => Trunc.mk ⟨x, rfl⟩

[mniip]

I guess what my original implementation does is reinvent the dependent eliminator (Quotient.recOn) in terms of the non-dependent eliminator (Quotient.lift)...

[Eric Wieser]

(docs#Quotient.recOn)