Zulip Chat Archive

Stream: maths

Topic: finite limits


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 22 2020 at 23:56):

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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip Bhavik Mehta (May 23 2020 at 00:00):

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

view this post on Zulip 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!

view this post on Zulip Bhavik Mehta (May 23 2020 at 00:01):

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

view this post on Zulip Mario Carneiro (May 23 2020 at 02:04):

Does unique_choice imply LEM?

view this post on Zulip Reid Barton (May 23 2020 at 02:04):

No

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 23 2020 at 02:09):

does proof irrelevance affect anything here?

view this post on Zulip Reid Barton (May 23 2020 at 02:09):

And always satisfies unique choice.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 23 2020 at 02:19):

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

view this post on Zulip 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 _ _)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Bhavik Mehta (May 23 2020 at 03:27):

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

view this post on Zulip 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