\documentclass{article}

% Support for Agda code.
\usepackage{agda}

% Use fonts with a decent coverage of non-ASCII characters.
\usepackage{fontspec}
\setmainfont{DejaVu Serif}
\setsansfont{DejaVu Sans}
\setmonofont{DejaVu Sans Mono}

% Use special font families without TeX ligatures for Agda code. (This
% code is inspired by a comment by Enrico Gregorio/egreg:
% https://tex.stackexchange.com/a/103078.) 
\newfontfamily{\AgdaSerifFont}{DejaVu Serif}
\newfontfamily{\AgdaSansSerifFont}{DejaVu Sans}
\newfontfamily{\AgdaTypewriterFont}{DejaVu Sans Mono}
\renewcommand{\AgdaFontStyle}[1]{{\AgdaSansSerifFont{}#1}}
\renewcommand{\AgdaKeywordFontStyle}[1]{{\AgdaSansSerifFont{}#1}}
\renewcommand{\AgdaStringFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
\renewcommand{\AgdaCommentFontStyle}[1]{{\AgdaTypewriterFont{}#1}}
\renewcommand{\AgdaBoundFontStyle}[1]{\textit{\AgdaSerifFont{}#1}}

\begin{document}

Some code:
\begin{code}
{-# OPTIONS --without-K --count-clusters #-}

open import Agda.Builtin.String

-- A comment with some TeX ligatures:
-- --, ---, ?`, !`, `, ``, ', '', <<, >>.

Θ₁ : Set → Set
Θ₁ = λ A → A

a-name-with--hyphens : ∀ {A : Set} → A → A
a-name-with--hyphens ff--fl = ff--fl

ffi : String
ffi = "--"
\end{code}
Note that the code is indented.

\end{document}