module Function where

open import Level

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

----------------------------------------------------------------------
-- Composition
----------------------------------------------------------------------
infixr  _∘_ _∘₂_
_∘_ :
  {ℓ 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