main.tex

%! Suppress = MightBreakTexify
\documentclass{article}

\usepackage[utf8]{inputenc}
\usepackage[pagebackref,citecolor=blue,linkcolor=OliveGreen,urlcolor=Mahogany,colorlinks]{hyperref}
\usepackage[usenames,dvipsnames]{xcolor}
\usepackage{url}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{lmodern}
\usepackage{etoolbox}
\usepackage{amsthm}
\usepackage{color}
\usepackage{cleveref}
\usepackage{tikz}
\usepackage{csquotes}
\usetikzlibrary{positioning}

% coq
\usepackage{minted}
\usemintedstyle{emacs}

\crefformat{section}{\S#2#1#3} % see manual of cleveref, section 8.2.1
\crefformat{subsection}{\S#2#1#3}
\crefformat{subsubsection}{\S#2#1#3}

\newcommand{\TODO}[0]{{\color{red} TODO}}
\newcommand{\lrangle}[1]{\langle #1\rangle}
\newcommand{\RedPRL}{{\color{red} Red}PRL}

\input{agda-macros}

\title{Constructive Interpretations of HoTT (Draft)}
\author{Tesla Ice Zhang}

% allow multiple labels in displaymath
%! Suppress = Makeatletter
\makeatletter
\patchcmd{\mathdisplay}
{\let\label\label@in@display}{}
{}{\fail}
%! Suppress = Makeatletter
\makeatother

% new cmd
\newcommand\xtag{
\refstepcounter{equation}%
\;\;\text{(\theequation)}}
\newcommand{\refl}{\textsf{refl}}

\begin{document}
\maketitle

\tableofcontents

\input{intro}
\input{path}
\input{hit}
\input{kan}
\input{ua}

\bibliography{ref}
\bibliographystyle{alpha}

\end{document}