Zulip Chat Archive

Stream: maths

Topic: Weak univalence implies choice


view this post on Zulip Chris Hughes (Jul 13 2019 at 16:33):

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.

view this post on Zulip Floris van Doorn (Jul 13 2019 at 21:56):

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

view this post on Zulip Floris van Doorn (Jul 13 2019 at 21:57):

How much do you rely on definitional proof irrelevance?

view this post on Zulip Chris Hughes (Jul 13 2019 at 22:18):

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

view this post on Zulip Floris van Doorn (Jul 13 2019 at 23:17):

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.

view this post on Zulip Floris van Doorn (Jul 13 2019 at 23:20):

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

view this post on Zulip Kenny Lau (Jul 14 2019 at 05:04):

  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

view this post on Zulip Kenny Lau (Jul 14 2019 at 05:04):

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

view this post on Zulip Kenny Lau (Jul 14 2019 at 05:04):

I cannot understand this at all

view this post on Zulip Floris van Doorn (Jul 14 2019 at 10:08):

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.

view this post on Zulip Kenny Lau (Jul 14 2019 at 10:42):

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

view this post on Zulip Kenny Lau (Jul 14 2019 at 10:42):

thanks


Last updated: May 14 2021 at 19:21 UTC