Quotient dlift

Stream: Is there code for X?

[William Sørensen]

Hi is there code for this in Mathlib or should i push it up

def Quotient.liftd
    {α : Sort u} {s : Setoid α} {β : Quotient s → Sort v}
    (f : (v : α) → β (Quotient.mk s v))
    (heq : ∀ (a b : α), a ≈ b → f a ≍ f b)
    (q : Quotient s)
    : β q :=
  let res := Quotient.lift
    (β := (x : Quotient s) ×' β x)
    (s := s) (fun q => ⟨Quotient.mk s q, f q⟩)
    (fun a b rel => (PSigma.mk.injEq _ _ _ _).mpr ⟨Quotient.sound rel, heq _ _ rel⟩)
    q
  have : res.fst = q := by induction q using Quotient.ind; rfl
  cast (congr rfl this) res.snd

@[simp]
theorem Quotient.liftd_mk
    {α : Sort u} {s : Setoid α} {β : Quotient s → Sort v}
    (f : (v : α) → β (Quotient.mk s v))
    (heq : ∀ (a b : α), a ≈ b → f a ≍ f b)
    (v : α)
    : Quotient.liftd f heq (.mk s v) = f v :=
  rfl

[Junyan Xu]

Quotient.hrecOn for the first

[William Sørensen]

Hmm yes i guess that is more general. This might just have quite niche usages. Need to experiment with hrecOn to see if it has the same defeq

[Aaron Liu]

Its literally defined the same way

[Aaron Liu]

well, almost the same way