Classical.choice produces equal elements

Stream: new members

[Constantine Ter-Matevosian]

Hi all. I was looking at the proof of Diaconescu's theorem (Classical.em), and noticed that on lines 58-59 it uses [what I think is] the fact that Classical.choice produces equal elements of a Nonempty type.

theorem choiceEq {α : Sort u} (a b : Nonempty α) :
  @Eq α (Classical.choice a) (Classical.choice b) := by rfl

This then seems to propagate to other AC-related defs like Classical.indefiniteDescription, Classical.choose, and Classical.choose_spec, i.e. any two values of these defs are equal.

Out of sheer curiosity, how/why does this work? And why doesn't it work for, say,

axiom hi {A : Sort u} (B : Sort v) (x : A) : B

theorem hiEq {A : Sort u} {B : Sort v} (x x' : A) : hi B x = hi B x' := sorry

?

[Kyle Miller]

Nonempty is a proposition, and this is just relying on proof irrelevance (proofs of the same proposition are defeq).

[Constantine Ter-Matevosian]

Oh, right, true!! Thank you! <3