```module Function where

open import Level

----------------------------------------------------------------------
-- Identity function
----------------------------------------------------------------------
id :
{ℓ : Level}
{A : Set ℓ}
→ ---------
A → A
id x = x

----------------------------------------------------------------------
-- Composition
----------------------------------------------------------------------
infixr 5 _∘_ _∘₂_
_∘_ :
{ℓ m n : Level}
{A : Set ℓ}
{B : A → Set m}
{C : (x : A) → B x → Set n}
(g : {x : A}(y : B x) → C x y)
(f : (x : A) → B x)
→ ----------------------------
(x : A) → C x (f x)
(g ∘ f) x = g (f x)

_∘₂_ :
{k ℓ m n : Level}
{A : Set k}
{B : Set ℓ}
{C : Set m}
{D : Set n}
(g : C → D)
(f : A → B → C)
→ -------------
A → B → D
(g ∘₂ f) x y = g (f x y)

----------------------------------------------------------------------
-- Constant function
----------------------------------------------------------------------
K :
{ℓ m : Level}
{A : Set ℓ}
{B : Set m}
→ -----------
B → (A → B)
K y _ = y

----------------------------------------------------------------------
-- Function application
----------------------------------------------------------------------
apply :
{ℓ m : Level}
{A : Set ℓ}
{B : A → Set m}
(x : A)
→ ---------------------
((x' : A) → B x') → B x
apply x f  = f x

```