Zulip Chat Archive

Stream: general

Topic: empty pi unique without quot.sound

Eric Rodriguez (Nov 10 2021 at 13:07):

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 (Nov 10 2021 at 13:21):

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 (Nov 10 2021 at 13:22):

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

Last updated: Dec 20 2023 at 11:08 UTC