module _ (A : Set) where id : A → A id x = x