module Issue604 where f : (y : Set1) → (x : Set) → Set1 f x = ?