What are canonical injections in Martin Lof type theory In the following paragraph from Martin Lof's 1972 paper...

If $A$ and $B$ are types, then so is there disjoint union $A + B$, which is the type of objects of form $i(a)$ with $a:A$ or $j(b)$ with $b:B$. Here $i$ and $j$ denote the canonical injections.

... what is meant by the canonical injections here?
 A: There are a few different ways that you could think about this. Let me give you three different answers.
1: The “Set Theory” Perspective
Recall that Martin-Löf was trying to write down rules that would capture the essence of set theory. In set theory, when we have two types $A$ and $B$, we form their disjoint union, $A+B$,  by setting:
$$ A + B := (A \times \{0\}) \cup (B \times \{1\})$$
What are the “essential properties” of this set? Well, the idea is that we have a copy of $A$ and a copy of $B$ (and any “overlap” between $A$ and $B$ has been duplicated). Indeed we see that there is a pair of canonical injections $i:A \rightarrow A + B$ and $j: B \rightarrow A + B$, given by:
$$i: a \mapsto (a,0)$$
$$j: b \mapsto (b,1)$$
So if we’re thinking of type theory as being modeled by set theory, each type is a set and each term is an element of that set. So these term-injections are the “defining feature” of the coproduct type.
2: The “Type Theory” Perspective
In type theory, we usually give type formers by specifying formation rules, introduction rules, elimination rules, and computation rules. For the “disjoint union type” or “coproduct type”, the formation and introduction rules look like:
$$\begin{align*} & \frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash B \text{ type}}{\Gamma \vdash A + B \text{ type}} \text{+-Form} \\
 \quad \\
& \frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash B \text{ type} \quad \Gamma \vdash a : A}{\Gamma \vdash i(a) : A + B} \text{+-Intro-Left} \\
& \quad \\
& \frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash B \text{ type} \quad \Gamma \vdash b : B}{\Gamma \vdash j(b) : A + B} \text{+-Intro-Right}  \end{align*}$$
The Formation rule is telling us that given two types $A$ and $B$, we can form their coproduct $A + B$. The left introduction rule is telling us that to each term $a:A$, we get an associated term $i(a):A+B$. The right introduction rule is similar for $b:B$. If we look at the elimination rules as well, we will see that these terms are “all there are”.
If we squint our eyes and think about it, these $i$ and $j$ from the introduction rules look like the injections from $A$ and $B$ into $A + B$ from the set theory perspective. Indeed, if we have already defined function types, we may realize these injections as functions defined using these rules!
The “Category Theory” Perspective
This perspective is reenforced by considering category theory. Take $A$ and $B$ to be two objects in a category $\mathcal{C}$. A “coproduct” of $A$ and $B$ in $\mathcal{C}$ is a triple $(X, i, j)$, where $X$ is an object, $i:A \rightarrow X$, and $j: B \rightarrow X$ are morphisms with the following property: For any object $X’$ and morphisms $i’:A \rightarrow X’$ and $j’:B \rightarrow X’$, there is a unique map $\phi: X \rightarrow X’$ such that $ \phi \circ i = i’$ and $\phi \circ j = j’$. That is, for all objects $X’$ in $\mathcal{C}$, we have that $\text{hom}(A,X’) \times \text{hom}(B,X’) \cong \text{hom}(X,X’)$.
Such a coproduct need not exist, but it often does. In set, the coproduct can be realized using the construction from the first perspective! Notice that these defining injections become part of the definition of a coproduct in an arbitrary category. This is echoed by defining coproduct types with the help of these canonical injections.
One of the really interesting things about Martin-Löf type theory is that it has models in categories other than sets. Such coproduct constructions are used for realizing coproduct types.
