-- contains Unicode characters; download, don't copy from browser module nothing where -- refine, rename parameters test1 : ∀ (A B : Set) → A → B → A test1 = ? -- put parameters on LHS test2 : ∀ {A B : Set} → A → B → A test2 = ? -- more use of refine test3 : ∀ {A B C : Set} → (A → B → C) → (A → B) → (A → C) test3 = ?