# A.1.4 Coproduct types

We introduce primitive constants $c_{+}$, $c_{\mathsf{inl}}$, and $c_{\mathsf{inr}}$. We write $A+B$ instead of $c_{+}(A,B)$, ${\mathsf{inl}}(a)$ instead of $c_{\mathsf{inl}}(a)$, and ${\mathsf{inr}}(a)$ instead of $c_{\mathsf{inr}}(a)$:

• if $A,B:\mathcal{U}_{n}$ then $A+B:\mathcal{U}_{n}$

• moreover, ${\mathsf{inl}}:A\rightarrow A+B$ and ${\mathsf{inr}}:B\rightarrow A+B$

If we have $A$ and $B$ as above, $C:A+B\rightarrow\mathcal{U}_{m}$, $d:\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{% (x:A)}}C({\mathsf{inl}}(x))$, and $e:\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{% (y:B)}}C({\mathsf{inr}}(y))$, then we can introduce a defined constant $f:\mathchoice{{\textstyle\prod_{(z:A+B)}}}{\prod_{(z:A+B)}}{\prod_{(z:A+B)}}{% \prod_{(z:A+B)}}C(z)$ with the defining equations

 $f({\mathsf{inl}}(x)):\!\!\equiv d(x)\qquad\text{and}\qquad f({\mathsf{inr}}(y)% ):\!\!\equiv e(y).$
Title A.1.4 Coproduct types
\metatable