{- 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 = {!!}