{-
Exercises for TYP at MGS 2021
-}
open import Data.Nat
variable
A B C : Set
{- 1. -}
add3 : ℕ → ℕ
add3 x = x + 3
tw : (A → A) → A → A
tw f n = f (f n)
-- evaluate
-- tw tw add3 1
-- 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
f₀ = {!!}
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})
tw-c : (A → A) → A → A
tw-c = {!!}