## Stream: maths

### Topic: finite limits

#### Reid Barton (May 22 2020 at 23:53):

@Bhavik Mehta, I came across https://github.com/b-mehta/topos/issues/22. How do you understand the statement "C has finite products", in the absence of choice? Do you understand section A.1.2 of the Elephant?

#### Bhavik Mehta (May 22 2020 at 23:55):

If I recall correctly the Elephant doesn't talk about this in much detail - I'm happy with the definition of finite limits that's currently in mathlib

#### Bhavik Mehta (May 22 2020 at 23:56):

I also take back my first comment there - not really sure what I had in mind

#### Bhavik Mehta (May 22 2020 at 23:57):

Also the issues and readme there are getting quite out of date, if there's something in particular you're looking for do let me know!

#### Reid Barton (May 22 2020 at 23:57):

At the moment, I'm just looking through the library to see what's in it and I saw this issue referenced from the code.

#### Bhavik Mehta (May 22 2020 at 23:59):

The most recent stuff is in sheaf-new right now, I'm trying to refactor because I've got some pretty terribly written and organised code at the moment (and make PRs to mathlib)

#### Bhavik Mehta (May 23 2020 at 00:00):

I now agree with the opinion that binary products + terminal => finite products probably requires finite choice

#### Bhavik Mehta (May 23 2020 at 00:01):

Also I realised today that in lean unique_choice {α : Sort u} [subsingleton α] : nonempty α → α is equivalent to 'every mono in (Type u) is regular' which I didn't know before!

#### Bhavik Mehta (May 23 2020 at 00:01):

(maybe that should be Type u rather than Sort u but something like that)

#### Mario Carneiro (May 23 2020 at 02:04):

Does unique_choice imply LEM?

No

#### Reid Barton (May 23 2020 at 02:08):

Well, I guess I am not 100% sure about the situation with universes. A topos yields a model of the other axioms, without (in general) LEM.

#### Mario Carneiro (May 23 2020 at 02:09):

does proof irrelevance affect anything here?

#### Reid Barton (May 23 2020 at 02:09):

And always satisfies unique choice.

#### Reid Barton (May 23 2020 at 02:12):

I don't think proof irrelevance is a problem. Two proofs of a proposition are interpreted as two sections of a monomorphism, which must be equal. I'm not so sure how to interpret types which depend on proofs though.

#### Mario Carneiro (May 23 2020 at 02:14):

even in lean those aren't really a problem; you can always replace a type depending on a proof with a pi type over that proof and proof irrelevance ensures a definitional isomorphism going in both directions

#### Mario Carneiro (May 23 2020 at 02:19):

I guess the interpretation of unique_choice asserts "existence" a bit less strongly (and in particular not computably), almost as if everything is in the erased monad

#### Mario Carneiro (May 23 2020 at 02:19):

in fact I think unique_choice' {α : Type u} [subsingleton α] : nonempty α → erased α is provable

#### Mario Carneiro (May 23 2020 at 02:22):

import data.erased

def erased_unique_choice {α} [subsingleton α] (h : nonempty α) : erased α :=
⟨λ _, true, let ⟨a⟩ := h in ⟨a, funext \$ λ b, eq_true_intro (subsingleton.elim _ _)⟩


#### Mario Carneiro (May 23 2020 at 02:24):

So all of these are equivalent to unique_choice:

• subsingleton A -> nonempty A -> A
• unique A -> A
• nonempty A -> trunc A
• erased A -> A

#### Bhavik Mehta (May 23 2020 at 03:09):

I don't think the second is equivalent to unique choice, since unique uses inhabited rather than nonempty, so unique does contain the data of what we want

#### Bhavik Mehta (May 23 2020 at 03:26):

I believe Type u in Lean is a quasitopos computably, and a topos iff we have unique choice. (We always have unique choice for Prop though by proof irrel)

#### Bhavik Mehta (May 23 2020 at 03:27):

Maybe not by proof irrel actually but because the existential in the nonempty eliminates nicely

#### Bhavik Mehta (May 23 2020 at 03:27):

Mario Carneiro said:

So all of these are equivalent to unique_choice:

• subsingleton A -> nonempty A -> A
• unique A -> A
• nonempty A -> trunc A
• erased A -> A

I feel like these equivalences would make a fun kata if we figure out how to block usage of choice

Last updated: May 10 2021 at 07:15 UTC