\documentclass{article}
\usepackage{agda}
\begin{document}

\begin{code}%
\>\AgdaFunction{id} \AgdaSymbol{:} \AgdaSymbol{\{}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{\}} \AgdaSymbol{→} \AgdaBound{A} \AgdaSymbol{→} \AgdaBound{A}\<%
\\
\>\AgdaFunction{id} \AgdaSymbol{\{}\AgdaArgument{A} \AgdaSymbol{=} \AgdaBound{A}\AgdaSymbol{\}} \AgdaBound{x} \AgdaSymbol{=} \AgdaBound{x}\<%
\\
%
\\
\>\AgdaFunction{foo} \AgdaSymbol{:} \AgdaSymbol{(}\AgdaBound{A} \AgdaSymbol{:} \AgdaPrimitiveType{Set}\AgdaSymbol{)} \AgdaSymbol{→} \AgdaBound{A} \AgdaSymbol{→} \AgdaBound{A}\<%
\\
\>\AgdaFunction{foo} \AgdaBound{B} \AgdaBound{x} \AgdaSymbol{=} \AgdaFunction{id} \AgdaSymbol{\{}\AgdaArgument{A} \AgdaSymbol{=} \AgdaBound{B}\AgdaSymbol{\}} \AgdaBound{x}\<%
\end{code}

\end{document}
