empty pi unique without quot.sound

Stream: general

[Eric Rodriguez]

I'm curious about this:

import logic.is_empty

def empty_pi {α} {g : α → Sort*} [h : is_empty α] : Π a, g a := h.elim

lemma empty_pi_unique {α} {g : α → Sort*} [is_empty α] : ∀ f : Π a, g a, f = empty_pi := sorry

You can clearly solve it with funext, which shows that quot.sound suffices to prove it. Is this statement even provable without quot.sound?

[Floris van Doorn]

Yes, you need function extensionality to prove this. In some systems function extensionality is added as an axiom, but in Lean we derive function extensionality from quot.sound.

[Floris van Doorn]

So quot.sound is not technically necessary, but (some axiom that implies) function extensionality is