%%%%%%%%%%%%%%%%%%%% Cover page %%%%%%%%%%%%%%%%%%%%

\newgeometry{noheadfoot,bindingoffset=-5pt,top=0pt,bottom=0pt,inner=0pt,outer=0pt}%
\ifOPTcover
\setcounter{page}{-1} % Otherwise we end up having two pages numbered 1
\newlength{\coverheight}
\setlength{\coverheight}{\OPTcoverheight}
\newlength{\coverwidth}
\setlength{\coverwidth}{\OPTcoverwidth}
\input{frontpage}
\ThisLLCornerWallPaper{1.1}{\OPTfrontimage}
\pagecolor{covercolor}
\frontpage
\newpage
% Reset page counter, cover page does not count
\ifpdf
\nopagecolor
\else
\pagecolor{white}
\fi
\cleartooddpage
\else
\fi

%%%%%%%%%%%%%%%%%%%% Bastard page %%%%%%%%%%%%%%%%%%%%
\ifOPTbastard
\cleartooddpage
\hbox{}
\vspace{0.2\textwidth}
{\centering
\makebox[\OPTbastardwidth][s]{
\fontsize{\OPTbastardtitlefont}{\OPTbastardtitlefont}\fontshape{n}\selectfont%
\textbf{Homotopy Type Theory}}\par
\vspace*{\OPTbastardtitleskip}
\makebox[\OPTbastardwidth][s]{
\fontsize{\OPTbastardsubtitlefont}{\OPTbastardsubtitlefont}\fontshape{n}\selectfont%
\textit{Univalent Foundations of Mathematics}}\par
}
\else
\fi

%%%%%%%%%%%%%%%%%%%% Title page %%%%%%%%%%%%%%%%%%%%
\cleartooddpage
\hbox{}\vfill
{\centering
\makebox[\OPTtitlewidth][s]{\fontsize{\OPTtitletitlefont}{\OPTtitletitlefont}\fontseries{b}\selectfont%
Homotopy Type Theory}\par
\vspace*{\OPTtitletitleskip}
\makebox[\OPTtitlewidth][s]{\fontsize{\OPTtitlesubtitlefont}{\OPTtitlesubtitlefont}\fontshape{it}\selectfont%
Univalent Foundations of Mathematics}\par
\vspace*{\OPTtitleskip}
{\fontsize{\OPTtitleauthorfont}{\OPTtitleauthorfont}\fontshape{n}\selectfont%
The Univalent Foundations Program\par
\vspace*{\OPTtitleauthorskip}
Institute for Advanced Study\par
}
\vspace*{\OPTtitleskip}
\vspace*{\OPTtitleskip}
\includegraphics[width=\OPTtitlewidth]{\OPThalftorus}\par
}

\vfill
\hbox{}

\clearpage
%%% Restore page style
\restoregeometry

%%%%%%%%%%%%%%%%%%%% Copyright page %%%%%%%%%%%%%%%%%%%%
\hbox{}
\vfill
\input{version.tex}
{\small
\noindent
\emph{``Homotopy Type Theory: Univalent Foundations of Mathematics''}\\
\copyright\ 2013 The Univalent Foundations Program

\medskip
\noindent
Book version: \texttt{\OPTversion}

\medskip
\noindent
MSC 2010 classification:
\texttt{03-02},
\texttt{55-02},
\texttt{03B15}

\bigskip
\footnotesize

\noindent
This work is licensed under the
\textbf{\emph{Creative Commons Attribution-ShareAlike 3.0 Unported License.}}
%
To view a copy of this license, visit
\url{http://creativecommons.org/licenses/by-sa/3.0/}.

\bigskip

\noindent
This book is freely available at \url{http://homotopytypetheory.org/book/}.

\bigskip

\noindent
\emph{\textbf{\small Acknowledgment}}

\medskip

\noindent
Apart from the generous support from the Institute for Advanced Study, some contributors
to the book were partially or fully supported by the following agencies and grants:
%
\begin{itemize}
\item Association of Members of the Institute for Advanced Study: a grant to the Institute for Advanced Study % Dan Grayson
% SLOVENIA
\item Agencija za raziskovalno dejavnost Republike Slovenije:  % Andrej's Slovenian agency
\href{http://www.sicris.si/search/prg.aspx?id=6120}{P1--0294},
\href{http://www.sicris.si/search/prj.aspx?id=7109}{N1--0011}.

\item Air Force Office of Scientific Research:
  FA9550-11-1-0143, and % Steve's ASFOR
  FA9550-12-1-0370.  % Bob's ASFOR
  {
    \setlength{\parskip}{0pt}
    \begin{quote}
      \noindent\scriptsize
      This material is based in part upon work supported by the AFOSR under the above awards.
      Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the author(s) and do not necessarily reflect the views of the AFOSR.
    \end{quote}
  }

\item Engineering and Physical Sciences Research Council: % Thorsten and students
   \href{http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/G034109/1}{EP/G034109/1}, % Reusability and dependent types
   \href{http://gow.epsrc.ac.uk/NGBOViewGrant.aspx?GrantRef=EP/G03298X/1}{EP/G03298X/1}. % Theory and Application of Induction Recursion

\item European Union's 7th Framework Programme under grant agreement nr.\ 243847 (%
\href{http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/ForMath/}{ForMath}). %% several Europeans, via Bas

\item National Science Foundation:
  \href{http://www.nsf.gov/awardsearch/showAward.do?AwardNumber=1001191}{DMS-1001191}, %% Steve's NSF, including Chris and Kristina
  \href{http://www.nsf.gov/awardsearch/showAward.do?AwardNumber=1100938}{DMS-1100938}, %% Vladimir's NSF
  \href{http://www.nsf.gov/awardsearch/showAward.do?AwardNumber=1116703}{CCF-1116703}, %% Foundations and Applications of Higher-Dimensional Directed Type Theory
  and
  \href{http://www.nsf.gov/awardsearch/showAward.do?AwardNumber=1128155}{DMS-1128155}. %% IAS support for Mike Shulman, copied from our %% paper by Dan Licata
  {
    \setlength{\itemsep}{0pt}
    \begin{quote}
      \noindent\scriptsize
      This material is based in part upon work supported by the
      National Science Foundation under the above awards.  Any opinions,
      findings, and conclusions or recommendations expressed in this
      material are those of the author(s) and do not necessarily reflect the
      views of the National Science Foundation.
    \end{quote}
  }
\item The Simonyi Fund: a grant to the Institute for Advanced Study          %% Dan Grayson
  \end{itemize}


}
\cleartooddpage

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "hott-online"
%%% End:
