\documentclass{article} \usepackage{agda} \begin{document} % \begin{code} % postulate A : Set % \end{code} \end{document}