\PassOptionsToPackage{ngerman,main=english}{babel}
\documentclass[11pt,a4paper,fleqn]{article}
\usepackage{iman,extra,isar}
\usepackage{isabelle,isabellesym}
\usepackage{railsetup}

\usepackage[margin={1in,1in}]{geometry}

\usepackage[T1]{fontenc} 
\usepackage{lmodern}
\usepackage{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{xspace}
\usepackage{MnSymbol}
\usepackage[utf8]{inputenc}
\usepackage{enumitem}
\usepackage{graphicx}
\usepackage{textcomp}
\usepackage{wasysym}
\usepackage{fontspec}

% bibliography
\usepackage[nottoc]{tocbibind}
\usepackage[square,numbers]{natbib}
\bibliographystyle{abbrvnat}

% this should be the last package used
\usepackage{pdfsetup}

% drop Isabelle tags
\isadroptag{theory}

% enumitem configuration
\setlist{noitemsep,topsep=0pt,parsep=0pt,partopsep=0pt}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}

\setcounter{tocdepth}{2}

\begin{document}

\title{Category Theory for ZFC in HOL II\\Elementary Theory of 1-Categories} 
\author{Mihails Milehins}
\maketitle

\newpage
\begin{abstract}
This article provides a formalization of the foundations of the theory 
of 1-categories in the object logic \textit{ZFC in HOL} 
(\cite{paulson_zermelo_2019}, also see \cite{barkaoui_partizan_2006}) of the 
formal proof assistant \textit{Isabelle} \cite{paulson_natural_1986}.
The methodology chosen for the formalization
rests on the ideas that were originally expressed in 
\cite{feferman_set-theoretical_1969}. 
Thus, in the context of this work, each category
is represented as a term of the type \textit{V} 
embedded into a stage of the von Neumann hierarchy 
\cite{takeuti_introduction_1971}.
\end{abstract}

\newpage

\renewcommand{\abstractname}{Acknowledgements}
\begin{abstract}
The author would like to acknowledge the assistance that he received from 
the users of the mailing list of Isabelle 
\href{https://lists.cam.ac.uk/mailman/listinfo/cl-isabelle-users}
in the form of answers given to his general queries. Special thanks
go to Andreas Lochbihler for suggesting the use of the combination 
of unrestricted overloading and locales for structuring mathematical 
knowledge on the mailing list of Isabelle: the design pattern that is 
used in this study builds upon this idea. Special thanks also go to
Thomas Sewell for suggesting a trick for rewriting 
expressions modulo associativity on the mailing list of Isabelle,
which was used on numerous occasions throughout the development
of this work. Furthermore, the author
would like to mention that the tool ``Sketch-and-Explore''
\cite{haftmann_sketch-and-explore_2021}
from the standard distribution of Isabelle was used extensively in the
development of this work. Moreover, the author would like 
to acknowledge the positive role that numerous Q\&A posted on the 
Stack Exchange network (especially Mathematics Stack Exchange, 
Stack Overflow and TeX Stack Exchange)
played in the development of this work. 
Lastly, the author would like to express gratitude to all members of his family 
and friends for their continuous support.
\end{abstract}

\newpage

\tableofcontents

\newpage

\parindent 0pt\parskip 0.5ex

\input{session}

\newpage

\bibliography{root}

\end{document}