Why isn't a propositional computation rule for quotients enough to derive funext?

[david-christiansen]

What question should the reference manual answer?

Why isn't a propositional computation rule for quotients enough to derive funext? This would satisfy curiosity about quotients and why they are the way they are in Lean.

Additional context
This was a request from a colleague reviewing the chapter on quotients pre-publication. Here's where the proof breaks:

axiom Q.{u} {α : Sort u} (r : α → α → Prop) : Sort u

axiom Q.mk.{u} {α : Sort u} (r : α → α → Prop) (a : α) : Q r

axiom Q.lift.{u, v} {α : Sort u} {r : α → α → Prop} {β : Sort v} (f : α → β) (a : ∀ (a b : α), r a b → Eq (f a) (f b)) :
  Q r → β

axiom Q.sound.{u} : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Q.mk r a = Q.mk r b


axiom Q.comp.{u,v} {α : Sort u} {r : α → α → Prop} {β : Sort v} {f : α → β} {prf : ∀ (a b : α), r a b → Eq (f a) (f b)} {a : α} : Q.lift f prf (Q.mk r a) = f a

theorem funext'' {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x}
    (h : ∀ x, f x = g x) : f = g := by
  let eqv (f g : (x : α) → β x) := ∀ x, f x = g x
  let extfunApp (f : Q eqv) (x : α) : β x :=
    Q.lift
      (fun (f : ∀ (x : α), β x) => f x)
      (fun _ _ h => h x)
      f

  suffices extfunApp (Q.mk eqv f) = extfunApp (Q.mk eqv g) by
    simp [extfunApp] at this
    /-
    α : Sort u
    β : α → Sort v
    f g : (x : α) → β x
    h : ∀ (x : α), f x = g x
    eqv : ((x : α) → β x) → ((x : α) → β x) → Prop := fun f g => ∀ (x : α), f x = g x
    extfunApp : Q eqv → (x : α) → β x := fun f x => Q.lift (fun f => f x) ⋯ f
    this : (fun x => Q.lift (fun f => f x) ⋯ (Q.mk eqv f)) = fun x => Q.lift (fun f => f x) ⋯ (Q.mk eqv g)
    ⊢ f = g
    -/
    sorry
  exact congrArg extfunApp (Q.sound h)

The problem is that rewriting propositionally under a lambda requires funext, which we don't want to assume in the course of proving it. The definitional computation rule solves the problem by making the two sides defeq to fun x => f x and fun x => g x, which by eta is convertible with the desired goal.