Zulip Chat Archive

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?

Reid Barton (May 23 2020 at 02:04):

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: Dec 20 2023 at 11:08 UTC