\documentclass{article} \usepackage{agda} \begin{document} Assume that we are given a type % \begin{code}[hide] module _ ( \end{code} \begin{code}[inline] A : Set \end{code} \begin{code}[hide] ) ( \end{code} % , and that a function % \begin{code}[inline*] F : Set → Set → Set → Set \end{code} \begin{code}[hide] ) where \end{code} % is also given. \end{document}