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.

Injective :∀{a b}{A :Set a}{B :Set b}→(A → B)→Set(a ⊔ b)Injective f =∀{x y}→ f x ≡ f y → x ≡ yrecord Injection {f t}(From :Set f)(To :Set t):Set(f ⊔ t)wherefieldto: From → To injective : Injective to

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.

record Surjection {f t}(From :Set f)(To :Set t):Set(f ⊔ t)wherefieldto: From → To from : To → From right-inverse-of :∀ x →to(from x) ≡ x

Bijection

Bijection is the combination of injection and surjection. A bijection implies one-to-one correspondence from the domain to the codomain − each element of one set is paired with exactly one element of the other set, and each element of the other set is paired with exactly one element of the first set. There are no unpaired elements.

record Bijection {f t}(From :Set f)(To :Set t):Set(f ⊔ t)wherefield injection : Injection From To surjection : Surjection From To