Definition. Constructors for sums [dt-0032]

For constructing sums, we use two primitive constructor functions, \mathit {inl} and \mathit {inr}: \begin {array}{l} \mathit {inl} : A \twoheadrightarrow (A + B)\\ \mathit {inl}(x) = (0,x)\\[1em] \mathit {inr} : B \twoheadrightarrow (A + B)\\ \mathit {inr}(y) = (1,y) \end {array}