Inclusion (mathematics)

Definition

In mathematics, an inclusion, inclusion map, or a canonical injection is a colloquial term for the "canonical" injective mapping from $A$ to $B$, where $A\subseteq B$.

The concept of an inclusion is particularly useful communication device in non–set-theoretic contexts where sub-collections are more difficult to define. One such setting is a type theoretic one such as Haskell: consider the inclusion $\text{toInt}:\text{Nat}\hookrightarrow \text{Int}$. In Haskell, two objects of different types are fundamentally different objects; to say $1:\text{Nat}$ is equal to $1:\text{Int}$ is nonsense in Haskell land. It is up to us to somewhat-arbitrarily agree that $\text{Nat}$ is a "sub-type" of $\text{Int}$, a statement that is justified by the injectivity of $\text{toInt}$.