Weak univalence implies choice

Stream: maths

[Chris Hughes]

Today I proved that weak_univalence {α β : Sort*} : α ≃ β → α = β and quot.sound imply choice as stated in Lean. You can get a weaker version of choice without quot.sound; this requires decidable equality on the type you're choosing from.
https://gist.github.com/ChrisHughes24/c7b8bcb3e50b2531be94f11ba2c23e3c

Curiously, Lean didn't ask me to mark the definition as noncomputable since I only used propositional axioms.

I copied the version of em from the HoTT book for part of this. It's much easier to understand than the Lean proof.

[Floris van Doorn]

That is surprising, since choice as stated in Lean is inconsistent with full univalence.

[Floris van Doorn]

How much do you rely on definitional proof irrelevance?

[Chris Hughes]

The main non-HoTT-valid thing I do is unique choice on {β : Type u // option β = plift α}

[Floris van Doorn]

Interesting. In HoTT that type is indeed not a proposition (subsingleton), while here it is. There is a weird interplay between proof irrelevance and "weak univalence".

Some remarks (probably not new to Chris):

• Unique Choice is provable in HoTT, but the proof Chris gave is looks a little weird from a HoTT perspective, since it relies on the fact that = is a proposition.
• The proof that option is injective also works in HoTT. unit + A ≃ unit + B → A ≃ B is proven here in Lean 2 HoTT. It is not an "embedding" though (which would be necessary to do the rest of the argument in HoTT).
• The proof structure is interesting (weird): you first prove decidable choice, then you prove LEM from that, and then you use that to show that the decidability condition in choice is superfluous.

[Floris van Doorn]

Although your proof heavily relies on proof irrelevance, I don't think you ever need it to be definitional.

[Kenny Lau]

  definition unit_sum_equiv_cancel_map : A → B :=
  begin
    intro a, cases sum.mem_cases (H (inr a)) with u b, rotate 1, exact b.1,
    cases u with u Hu, cases sum.mem_cases (H (inl ⋆)) with u' b, rotate 1, exact b.1,
    cases u' with u' Hu', exfalso, apply empty_of_inl_eq_inr,
    calc inl ⋆ = H⁻¹ (H (inl ⋆)) : (to_left_inv H (inl ⋆))⁻¹
           ... = H⁻¹ (inl u') : {Hu'}
           ... = H⁻¹ (inl u) : is_prop.elim
           ... = H⁻¹ (H (inr a)) : {Hu⁻¹}
           ... = inr a : to_left_inv H (inr a)
  end

[Kenny Lau]

https://github.com/leanprover/lean2/blob/master/hott/types/sum.hlean#L218

[Kenny Lau]

I cannot understand this at all

[Floris van Doorn]

The proof is not readable at all, and also not intended as such. The idea is, given f : unit + A ≃ unit + B we define a function g : A → B such that

• if f(inr a) = inr b then g(a) = b
• if f(inr a) = inl star then f (inl star) = inr b' for some b' and we define g(a) = b'
• Everything after the exfalso is a (longer than necessary) proof that f(inr a) = inl star and f (inl star) = inl star is impossible.

[Kenny Lau]

oh I understand it now, I thought it was some HoTT-specific thing that didn't hold in real maths

[Kenny Lau]

thanks