An injection is a function that never maps distinct elements of the domain to the same element of the codomain. For example, (\x -> x + 1) is an injection, but (\x -> min x 0) is not.

Injections can be used to construct nested structures from singleton elements.