finite limits

Stream: maths

[Reid Barton]

@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]

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]

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

[Bhavik Mehta]

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]

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]

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]

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

[Bhavik Mehta]

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]

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

[Mario Carneiro]

Does unique_choice imply LEM?

[Reid Barton]

No

[Reid Barton]

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]

does proof irrelevance affect anything here?

[Reid Barton]

And always satisfies unique choice.

[Reid Barton]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Bhavik Mehta]

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