{-
MGS 23 : Type Theory

Sunday
-}

open import Data.Nat

f : ℕ → ℕ
f x = x + 2

n : ℕ
n = 3

f' : ℕ → ℕ
f' = λ x → x + 2

-- f(3) , f 3

{-
f' 3
= (λ x → x + 2) 3
= (x + 2)[x := 3] -- β-step
= 3 + 2
= 5
-}

-- (λ x → M) N = M [x := N]

-- currying, schoenfinkling

g : ℕ → ℕ → ℕ
g = λ x → (λ y → x + y)

-- (g 2) 3 = g 2 3
-- g : ℕ × ℕ → ℕ
-- a curried 1st order function
-- A → B → C = A → (B → C)
-- g a b = (g a) b

-- higher order functions

h : (ℕ → ℕ) → ℕ
h = λ k → k 2 + k 3

-- h f
{-
h f' 
= (λ k → k 2 + k 3)(λ x → x + 2)
= (k 2 + k 3)[k := λ x → x + 2]
= (λ x → x + 2) 2 + (λ x → x + 2) 3
= (x + 2)[x := 2] + (x + 2)[x := 3]
= (2 + 2) + (3 + 2)
= 9
-}

-- combinators

variable A B C : Set

id : A → A
id = λ x → x

_∘_ : (B → C) → (A → B) → (A → C)
f ∘ g = λ x → f (g x)

K : A → B → A
K = λ a b → a
-- λ a → λ b → M = λ a b → M

S : (A → B → C) → (A → B) → (A → C)
S = λ f g a → f a (g a)

-- S + K are universal

I : A → A
I {A = A} = S K (K {B = A})
-- S K f a = K a (f a) = a

CC : (B → C) → (A → B) → (A → C)
CC = {!!}