Propositional Uniqueness for Coproduct Types? I'm working through the HoTT book and have just finished the section on coproducts. In short, I am wondering if there is a uniqueness principle for coproduct types. I can not find mention of one in the HoTT book. I have produced what I believe is a proof of the propositional uniqueness principle for coproduct types, i.e. that every $z:A+B$ is either of the form $inl(a)$ for some $a:A$, or of the form $inr(b)$ for some $b:B$. I even checked this proof in Coq. Now, I looked through the HoTT book's index and could find no mention of a uniqueness principle for coproduct types. Because I can't find a proof of the uniqueness principle in the book, I am worried that coproduct types do not actually satisfy such a principle. I know some incarnations of coproducts (such as of groups) introduce elements or terms that were not in the original object (e.g. the coproduct of the free group on the letter $x$ with the free group on the letter $y$ has a term of the form $xy$ which is in neither of the free groups). So, am worried I made a mistake in my proof and also did not prove what I thought I proved in Coq. Does anybody know about such a uniqueness principle?
---- I just thought of something. Since you can define coproduct types as a dependent sum over the type $2$, does the uniqueness principle follow from the dependent sum's uniqueness principle and the second projection? This is not how I proved it but it would explain why the HoTT book doesn't mention the principle.
 A: It depends on what exactly you have in mind.

*

*If you mean that you can deduce something like: $$Π(s : A + B). (Σ(a : A). \mathsf{Id}\ (\mathsf{inl}\ a)\ s) + (Σ(b : B). \mathsf{Id}\ (\mathsf{inr}\ b)\ s)$$ then it should follow from the induction principle. If this isn't in the HoTT book, then it probably just means that it wasn't a lemma they needed for anything else. The induction principle is sort of a generalization of this. To establish $P(s)$, it suffices to establish $P(\mathsf{inl}\ a)$ and $P(\mathsf{inr}\ b)$.


*If you mean that there is some sort of judgmental, eta-like rule for sums, then this is usually not included in theories for any inductive types, for technical reasons. Sums would be less problematic because they aren't recursive (so, there'd be no worry about expanding forever), but eta rules involving inductive eliminators are kind of unwieldy.


*If you mean that for any closed term $s : A + B$ there must either be a closed $a : A$ or closed $b : B$ such that $s$ is judgmentally equal to $\mathsf{inl}\ a$ or $\mathsf{inr}\ b$ respectively, then this property is called "canonicity." It is a desirable property when using the type theory as a programming language. However, postulates without a computational interpretation generally invalidate it. So, e.g. excluded middle causes it to fail, because there is no mechanism for deciding arbitrary propositions. And in fact, the univalence axiom in the book also breaks it, since there is no (complete) computational interpretation given for it (this can in principle be fixed, though).
If you define binary sums in terms of $Σ$ and $2$, then these scenarios reduce to analogous ones for those types. Judgmental eta rules are frequently used for $Σ$ (although I think the HoTT book does not include one), but #1, #2 and #3 will be similar for $2$ as for $+$.
The stuff about groups is not really relevant. It essentially means that groups do not form a model of type theory. You can actually encode the phenomenon in HoTT, though, because identity/path types act like groups. So, if you encode a group $G$ as a type with one point $\mathsf{base}$ such that the loop space $\mathsf{Id\ base\ base}$ is isomorphic to $G$, then I think their codproduct as groups is encoded by the wedge sum over their base points (page 257 of the book). If you have groups $G$ and $H$, then $G$ embeds as left paths, and $H$ embeds as right paths, and the added path between the left and right base points lets you compose them together.
