## Stream: maths

### Topic: Weak univalence implies choice

#### 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.

#### Floris van Doorn (Jul 13 2019 at 21:56):

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

#### Floris van Doorn (Jul 13 2019 at 21:57):

How much do you rely on definitional proof irrelevance?

#### Chris Hughes (Jul 13 2019 at 22:18):

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

#### 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.

#### 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.

#### 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


#### Kenny Lau (Jul 14 2019 at 05:04):

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

#### Kenny Lau (Jul 14 2019 at 05:04):

I cannot understand this at all

#### 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.

#### 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

#### Kenny Lau (Jul 14 2019 at 10:42):

thanks

Last updated: May 14 2021 at 19:21 UTC