A.1.4 Coproduct types

We introduce primitive constants $c_{+}$, $c_{\mathrm{𝗂𝗇𝗅}}$, and $c_{\mathrm{𝗂𝗇𝗋}}$.We write $A+B$ instead of $c_{+}(A,B)$, $\mathrm{𝗂𝗇𝗅}(a)$ instead of$c_{\mathrm{𝗂𝗇𝗅}}(a)$, and $\mathrm{𝗂𝗇𝗋}(a)$ instead of $c_{\mathrm{𝗂𝗇𝗋}}(a)$:

• if $A,B:{𝒰}_n$ then $A+B:{𝒰}_n$

• moreover, $\mathrm{𝗂𝗇𝗅}:A\to A+B$ and $\mathrm{𝗂𝗇𝗋}:B\to A+B$

If we have $A$ and $B$ as above, $C:A+B\to {𝒰}_m$,$d:{\prod }_{(x:A)}C(\mathrm{𝗂𝗇𝗅}(x))$, and $e:{\prod }_{(y:B)}C(\mathrm{𝗂𝗇𝗋}(y))$,then we can introduce a defined constant $f:{\prod }_{(z:A+B)}C(z)$ with the defining equations

$$f(\mathrm{𝗂𝗇𝗅}(x)):\equiv d(x)\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}f(\mathrm{𝗂𝗇𝗋}(y)):\equiv e(y).$$