\documentclass{article}

\usepackage{agda}

\begin{document}

\begin{code}%
\>\AgdaKeyword{module} \AgdaModule{Indenting4} \AgdaKeyword{where}\<%
\end{code}

\begin{code}%
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaFunction{Pow} \AgdaSymbol{:} \AgdaPrimitiveType{Set} \AgdaSymbol{→} \AgdaPrimitiveType{Set₁}\<%
\\
\>[0]\AgdaIndent{2}{}\<[2]%
\>[2]\AgdaFunction{Pow} \AgdaBound{X} \AgdaSymbol{=} \AgdaBound{X} \AgdaSymbol{→} \AgdaPrimitiveType{Set}\<%
\end{code}

\end{document}
