# 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
open import Types.product using (Σ; _,_; fst; snd)
open import Types.functions
open import Types.equational

# Classifications of functions

Functions can be classified into:

1. Injective (one-to-one)
2. Surjective (onto)
3. Bijective (one-to-one and onto)

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 ≡ y

record Injection {f t} (From : Set f) (To : Set t) : Set (f ⊔ t) where
field
to        : 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.

-- Surjective : ∀ {a b} {A : Set a} {B : Set b} → (A → B) → Set (a ⊔ b)
-- Surjective f = ∀ y → ∃ λ x → f x ≡ y

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

## Bijection

record Bijection {f t} (From : Set f) (To : Set t) : Set (f ⊔ t) where
surjection : Surjection From To