{-

Sunday Exercises for Type Theory  at MGS 2023

-}
open import Data.Nat

variable
  A B C : Set

{- 1. -}

add3 : ℕ → ℕ
add3 = λ x → x + 3
-- λ = \Gl \lambda
-- \-> = → 

tw : (A → A) → A → A
tw = λ f n → f (f n)

-- evaluate C-c C-n
-- tw tw add3 1
{-
tw tw add3 1
= ...
= 13
-}

-- derive the result (in a comment) step by step

{- 2. -}

-- derive lambda terms with the following types

f₀ : (A → B) → (B → C) → (A → C)
f₁ : (A → B) → ((A → C) → C) → ((B → C) → C)
f₂ : (A → B → C) → B → A → C

-- C-c C-l load file
-- C-c C-, shows context inside a shed
-- C-c C-SPC to open a shed
-- C-c C-r refine, automatically inserts applications
--         and λ and ...

f₀ = λ f → λ g → λ a → g (f a)
f₁ = {!!}
f₂ = {!!}

{- 3. -}

-- Advanced (see lecture notes 2.4)

{-
Derive a function tw-c which behaves the same as tw 
using only S, K (and I which is defined using S and K below).
-}

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

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

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

f₀-c : (A → B) → (B → C) → (A → C)
f₀-c = S (K (S (S (K S) K))) K
{-
λ f → λ g → λ a → g (f a)
= λ f → λ g → S (λ a → g) (λ a → f a)
= λ f → λ g → S (K g) f
= λ f → S (λ g → S (K g)) (λ g → f)
= λ f → S (S (λ g → S) (λ g → K g)) (K f)
= λ f → (S (S (K S) K)) (K f)
= S (K (S (S (K S) K))) K

rules
λ x → M N = S (λ x → M) (λ x → N)
λ x → M = K M, x does not occur in M
λ x → M x = M, x does not occur in M
λ x → x = I = S K K

(λ x → M N) L = M[x:=L] N[x:=L]
S (λ x → M) (λ x → N) L =
(λ x → M) L ((λ x → M) L) =
M[x:=L] N[x:=L]


-}

-- tw = λ f → λ n → f (f n)
tw-c : (A → A) → A → A
tw-c = {!!}