HoTT.tex

% !TEX encoding = UTF-8 Unicode

\documentclass[12pt]{amsart}
\usepackage{geometry}
\geometry{letterpaper}

\usepackage{hyperref}

\usepackage{ucs}
\usepackage[utf8x]{inputenc}

\usepackage{fancyvrb}

\DefineVerbatimEnvironment
  {code}{Verbatim}
  {}

\title{HoTT Exercises in Agda}
\author{Eric Bailey}
% \date{}

\begin{document}

\maketitle
\tableofcontents

\newpage
\input{HoTT/Chapter1/Ex1.lagda.tex}
\end{document}