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