Injective functions #
Change the value of an embedding
f at one point. If the prescribed image
is already occupied by some
f a', then swap the values at these two points.
f : α ↪ α' is an embedding and
g : Π a, β α ↪ β' (f α) is a family
of embeddings, then
sigma.map f g is an embedding.
The type of embeddings
α ↪ β is equivalent to
the subtype of all injective functions
α → β.
α₁ ≃ α₂ and
β₁ ≃ β₂, then the type of embeddings
α₁ ↪ β₁
is equivalent to the type of embeddings
α₂ ↪ β₂.