Primitive functions for sums [dt-003D]
DefinitionConstructors 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}
TheoremContinuity of sum constructors [dt-0033]
The constructor functions \mathit {inl} and \mathit {inr} are continuous.
DefinitionThe 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}
Exercise [dt-0035]
Prove that the case function [f,g](x) is, given continuous functions f : A \twoheadrightarrow C and g : B \twoheadrightarrow C, continuous on its argument x.
As mentioned in Construction [dt-0031], the only directed subsets of A + B are those that contain entirely values of the format (0,\_) and optionally \bot _{A+B}, or those that contain entirely values of the format (1,\_) and optionally \bot _{A+B}. Call this directed subset X.
Solution.