Contents Previous Next

Functions, Continued…

module Types.functions2 where

open import Lang.dataStructures using (
  Bool; true; false;
; List;
  one; two; three; four; five; six; seven; eight; nine; ten; zero; succ;
  _::_; [];
; singleton;)

open import Agda.Primitive using (Level; __; lsuc)

open import Types.equality using (IsEquivalence; Setoid; Rel)
open import Types.product using (Σ; _,_; fst; snd)
open import Types.functions

Classifications of functions

Functions can be broadly classified as:

  1. Injective (one-to-one)
  2. Surjective (onto)
  3. Bijective (one-to-one and onto)
Injection vs Surjection vs Bijection

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


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))

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


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 is the combination of injection and surjection.

Proofs as Data