Definition. The case function [dt-0034]

Elimination of sums is captured by the case function [f,g] : (A + B) \twoheadrightarrow C, made from functions f : A \twoheadrightarrow C and g : B \twoheadrightarrow C. This function is defined by: \begin {array}{l} [f,g] : (A + B) \twoheadrightarrow C\\ [f,g](x) = \begin {cases} f(a) & \text {if}\ x = (0,a) \\ g(b) & \text {if}\ x = (1,b) \\ \bot _C & \text {if}\ x = \bot _{A+B}\end {cases} \end {array}