# Does "unique mere existence" imply "existence"?

Hopefully this question fits in well here. I'm hoping that more people who know the answer will see it here than on somwehere like mse, but please let me know if you'd rather I move it there!

Say you're able to prove that $$\exists x:X . \varphi(x)$$. That is, you're able to prove the propositional truncation $$\left \lVert \sum_{x:X} \varphi(x) \right \rVert$$. This is, obviously, not enough to conclude that $$\sum_{x:X} \varphi(x)$$ in general. One quick way to see this is via sheaf models, where the $$\Sigma$$-type tells us about a global section but the $$\exists$$-type only tells us that you can find a local section everywhere. There's no reason for these local sections to glue into a global section.

But, let's say you're moreover able to prove that there's a unique witness to $$\varphi$$, so that $$\forall x,y. \varphi(x) \land \varphi(y) \to x=y$$ (of course, there's no difference here between $$\forall$$ and $$\Pi$$). Now in the sheaf model picture, even if you only have local sections the uniqueness tells us that these sections must glue! So here we should be able to pass from $$\exists! x:X . \varphi$$ to $$\sum_{x:X} \varphi$$. Is there some way to prove this purely type-theoretically?

I'm mainly interested in the internal logic of 1-topoi, so I don't think I necessarily have univalence available, but of course I'm also interested in minor perturbations of this question too. So if you have a solution that uses an assumption about the type theory, like univalence, or an assumption about the type, like decidable equality, I'm very happy to hear about it!

Thanks in advance ^_^

• What is your internal logic of 1-topoi like? Do extract an element of a singleton subset (which is what you're asking about in terms of higher-order logic), you need something, for instance the definite description operator or some such. If you're working with dependent type theory, then James Wood's answer will do the job. Apr 21 at 10:33
• I think this is subtle. For example, in Lean, I would interpretation propositional truncation as Nonempty. But then your theorem (a form of “unique choice”) is not provable without choice. I think that would also be the case for most other interactive theorem provers as well but I’m not sure of the details. Apr 21 at 23:37
• But why would you interpret it that way when unique choice is sound in every topos? Apr 22 at 15:10
• @DanDoel I got confused by terminology. So, here “proposition” just means subsingleton type and not an element of the topos’s subobject classifier (e.g. Lean’s Prop)? (Most theorem provers still define say $\exists$ using the later, right?) Also I thought the internal logic of a topos was closer to intuitionistic higher order logic, like the base logic in Isabelle/HOL or HOL Light, but now I realize the OP’s question wouldn’t even make sense in that setting since there are no sigma types there. (I’m probably still not making sense. I guess I still have a lot to understand about this field…) Apr 22 at 20:41
• @DanDoel Wait, first I was thinking that you are objecting to my saying that Nonempty(X) -> X is the natural way to interpret the OP’s question in say Lean, and then it doesn’t follow from the axioms (without choice). But even if I literately use the OP’s(∃! x:X, phi x) -> (∑ x:X, phi x) it still doesn’t follow. I’m not sure if you are saying this would hold in a topos if I used the correct internal logic (and that Lean or Coq isn’t close enough) or if you are saying I shouldn’t call the OP’s property a form of “unique choice” (but I think a lot of resources do call this unique choice). Apr 22 at 21:00

If $$\varphi$$ is proposition-valued and has at most one witness, then $$\sum_{x:X}\varphi(x)$$ is a proposition. We can see this because, given two inhabitants of $$\sum_{x:X}\varphi(x)$$, they have the same first projection by uniqueness of witness, and they have the same second projection because the type of the second projections is a proposition.
Then, the universal property of propositional truncation says that, for any proposition $$P$$, we get a map $$\lVert P \rVert \to P$$, which is what we wanted.
This proof relies only on having sensible, MLTT-like behaviour of propositional truncation, $$\sum$$-types, function types, and identity types.