\documentclass{article} \usepackage{agda} \begin{document} \begin{code} variable A : Set f : A → A f x = x \end{code} \end{document}