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).