Note that a function, by definition, can never produce multiple outputs given the same input.

Injection

A function f : X → Y is injective if \(∀ x ∈ X, y ∈ Y, f(x) == f(y) ⟹ x == y\). Or in other words, the map is one-to-one between all objects of X and some objects of Y.

module_{a b ℓ}{A :Set a}{B : A →Set b}{_=₁_: Rel A ℓ}{_=₂_:(x : A)→ Rel (B x) ℓ}(eq1 : IsEquivalence _=₁_)(eq2 :(x : A)→ IsEquivalence (_=₂_ x))where

Injective : A → B → Set Injective f = ∀ {x y : A} → (f x) =₁_ (f y) → x (=₂ x) y

Surjection

A function f : X → Y is surjective if \(∀ y ∈ Y, ∃ x ∈ X s.t. f(x) == y\). This states that for every element of Y, there should be at least one element of X such that f(x) == y. So Y is an complete image of X.

Bijection

Bijection is the combination of injection and surjection.