[Agda] Agda code in slides

[Sergei Meshveliani]

People,

I need to prepare a slide presentation in LaTex which has many fragments
of Agda code.
I write (as an example) 

----------------------------------------------
\documentclass[pdf]{beamer}
\mode<presentation>{}

% This handles the translation of unicode to latex:
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{autofe}
...

\begin{document}
\title{Foo}
\author{Foo}
\maketitle

\begin{frame}{Foo}

\begin{verbatim}
  record Foo : Set where
         constructor foo'
         field
           a   :  Rel C _
           op₂ :  C → C
           a≉0 :  a ≉ 0#

  _='_ :  Rel C _
  x =' y =  (f x * f y) ≈ y
\end{verbatim}
\end{frame}
\end{document}
----------------------------------------------

And  pdflatex reports errors.
Removing  {verbatim}  makes it compiled. But this breaks the code
script, indentations, frame nicety, etc.

What is, please, a way out?

Thanks, 

------
Sergei