agda/test/LaTeXAndHTML/succeed/UnicodeInput.lagda

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

\begin{code}
data αβγδεζθικλμνξρστυφχψω : Set₁ where

postulate
  →⇒⇛⇉⇄↦⇨↠⇀⇁ : Set
\end{code}

\[
∀X [ ∅ ∉ X ⇒ ∃f:X ⟶  ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]
\]
\end{document}