# Zulip Chat Archive

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