Lifting a quotient function

Stream: Is there code for X?

[Robin Arnez]

import Mathlib.Data.Quot

noncomputable def Quotient.liftFun {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).out)

theorem Quotient.liftFun_mk {s : Setoid α} (f : (β → α) → γ) (h : ∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) (g : β → α) :
    Quotient.liftFun f h (fun x => Quotient.mk s (g x)) = f g := by
  unfold liftFun
  apply h
  intro x
  exact Quotient.mk_out (g x)

Is there a computable version of this function? I feel like this is a safe operation but I haven't seen any computable versions...

[Aaron Liu]

No, this is equivalent to a version of the axiom of choice. You can still make it computable, though.

import Mathlib.Data.Quot

unsafe def Quotient.liftFunImpl {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).unquot)

@[implemented_by Quotient.liftFunImpl]
def Quotient.liftFun {s : Setoid α} (f : (β → α) → γ) : (∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) →
    (β → Quotient s) → γ := fun _ q => f (fun a => (q a).out)

theorem Quotient.liftFun_mk {s : Setoid α} (f : (β → α) → γ) (h : ∀ f₁ f₂, (∀ x, f₁ x ≈ f₂ x) → f f₁ = f f₂) (g : β → α) :
    Quotient.liftFun f h (fun x => Quotient.mk s (g x)) = f g := by
  unfold liftFun
  apply h
  intro x
  exact Quotient.mk_out (g x)

[Robin Arnez]

Ah, okay, kinda thought that already. I feel like something like this should exist somewhere in mathlib or batteries though (I guess with an unsafe implementation).

[Aaron Liu]

Actually, you might be able to bypass choice with some dependent type casting shenanigans. I don't actually have a proof yet.

[Robin Arnez]

Huh, okay... I mean ideally liftFun_mk would be defeq but I don't think we will get that.