Remove tex warnings
This commit is contained in:
parent
7faf0961c5
commit
e18730e0e5
|
@ -38,12 +38,11 @@
|
|||
\newcommand*{\department}[1]{\gdef\@department{#1}}
|
||||
\newcommand*{\researchgroup}[1]{\gdef\@researchgroup{#1}}
|
||||
\newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}}
|
||||
%% FRONTMATTER
|
||||
\newcommand*{\myfrontmatter}{%
|
||||
\newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm}
|
||||
\begingroup
|
||||
\thispagestyle{empty}
|
||||
\usepackage{noto}
|
||||
\fontseries{sb}
|
||||
%% \fontfamily{noto}\selectfont
|
||||
{\Huge\@title}\\[.5cm]
|
||||
{\Large A formalization of category theory in Cubical Agda}\\[2.5cm]
|
||||
\begin{center}
|
||||
|
@ -55,17 +54,16 @@
|
|||
{\Large\@author}\\[.5cm]
|
||||
Master's thesis in Computer Science
|
||||
\endgroup
|
||||
%% \renewcommand{\familydefault}{\rmdefault} \normalfont % Reset standard font
|
||||
%% \end{titlepage}
|
||||
|
||||
|
||||
% BACK OF COVER PAGE (BLANK PAGE)
|
||||
\newpage
|
||||
\newgeometry{a4paper} % Temporarily change margins
|
||||
\restoregeometry
|
||||
%% \newgeometry{a4paper} % Temporarily change margins
|
||||
%% \restoregeometry
|
||||
\thispagestyle{empty}
|
||||
\null
|
||||
|
||||
}
|
||||
|
||||
\renewcommand*{\maketitle}{%
|
||||
\begin{titlepage}
|
||||
|
|
|
@ -89,10 +89,12 @@ interest.
|
|||
With this definition we can also recover reflexivity. That is, for any $A \tp
|
||||
\MCU$ and $a \tp A$:
|
||||
%
|
||||
\begin{align}
|
||||
\begin{equation}
|
||||
\begin{aligned}
|
||||
\refl & \tp \Path (\lambda i \to A)\ a\ a \\
|
||||
\refl & \defeq \lambda i \to a
|
||||
\end{align}
|
||||
\end{aligned}
|
||||
\end{equation}
|
||||
%
|
||||
Or, in other terms; reflexivity is the path in $A$ that is $a$ at the left
|
||||
endpoint as well as at the right endpoint. It is inhabited by the path which
|
||||
|
@ -113,10 +115,12 @@ structure''. At the bottom of this hierarchy we have the set of contractible
|
|||
types:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
\begin{aligned}
|
||||
%% \begin{split}
|
||||
& \isContr && \tp \MCU \to \MCU \\
|
||||
& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c
|
||||
\end{alignedat}
|
||||
%% \end{split}
|
||||
\end{aligned}
|
||||
\end{equation}
|
||||
%
|
||||
The first component of $\isContr\ A$ is called ``the center of contraction''.
|
||||
|
@ -127,10 +131,10 @@ contractible, then it is isomorphic to the unit-type $\top$.
|
|||
The next step in the hierarchy is the set of mere propositions:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
\begin{aligned}
|
||||
& \isProp && \tp \MCU \to \MCU \\
|
||||
& \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1
|
||||
\end{alignedat}
|
||||
\end{aligned}
|
||||
\end{equation}
|
||||
%
|
||||
$\isProp\ A$ can be thought of as the set of true and false propositions. It is
|
||||
|
@ -144,10 +148,10 @@ stress that we have $\isProp\ A$.
|
|||
Then comes the set of homotopical sets:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
\begin{aligned}
|
||||
& \isSet && \tp \MCU \to \MCU \\
|
||||
& \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1)
|
||||
\end{alignedat}
|
||||
\end{aligned}
|
||||
\end{equation}
|
||||
%
|
||||
At this point it should be noted that the term ``set'' is somewhat conflated;
|
||||
|
@ -158,10 +162,10 @@ if $\isSet\ A$ is inhabited.
|
|||
The next step in the hierarchy is, as the reader might've guessed, the type:
|
||||
%
|
||||
\begin{equation}
|
||||
\begin{alignat}{2}
|
||||
\begin{aligned}
|
||||
& \isGroupoid && \tp \MCU \to \MCU \\
|
||||
& \isGroupoid\ A && \defeq \prod_{a_0, a_1 \tp A} \isSet\ (a_0 \equiv a_1)
|
||||
\end{alignedat}
|
||||
\end{aligned}
|
||||
\end{equation}
|
||||
%
|
||||
And so it continues. In fact we can generalize this family of types by indexing
|
||||
|
|
|
@ -195,7 +195,7 @@ Name & Agda & Notation \\
|
|||
\nomen{Type} & \texttt{Set} & $\Type$ \\
|
||||
\nomen{Set} & \texttt{Σ Set IsSet} & $\Set$ \\
|
||||
Function, morphism, map & \texttt{A → B} & $A → B$ \\
|
||||
Dependent- ditto & \texttt{(a : A) → B} & $∏_{a \tp A} → B$ \\
|
||||
Dependent- ditto & \texttt{(a : A) → B} & $∏_{a \tp A} B$ \\
|
||||
\nomen{Arrow} & \texttt{Arrow A B} & $\Arrow\ A\ B$ \\
|
||||
\nomen{Object} & \texttt{C.Object} & $̱ℂ.Object$ \\
|
||||
Definition & \texttt{=} & $̱\defeq$ \\
|
||||
|
|
|
@ -25,6 +25,7 @@
|
|||
%% department=Department of Computer Science and Engineering,
|
||||
%% researchgroup=Programming Logic Group
|
||||
%% ]{chalmerstitle}
|
||||
|
||||
\usepackage{chalmerstitle}
|
||||
\subtitle{A formalization of category theory in Cubical Agda}
|
||||
\authoremail{hanghj@student.chalmers.se}
|
||||
|
@ -48,7 +49,7 @@
|
|||
\newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@}
|
||||
\makeatother
|
||||
\begin{document}
|
||||
|
||||
\myfrontmatter
|
||||
\pagenumbering{roman}
|
||||
\maketitle
|
||||
\addtocontents{toc}{\protect\thispagestyle{empty}}
|
||||
|
|
|
@ -45,7 +45,7 @@
|
|||
%% \setmonofont{FreeMono.otf}
|
||||
|
||||
|
||||
\pagestyle{fancyplain}
|
||||
%% \pagestyle{fancyplain}
|
||||
\setlength{\headheight}{15pt}
|
||||
\renewcommand{\chaptermark}[1]{\markboth{\textsc{Chapter \thechapter. #1}}{}}
|
||||
\renewcommand{\sectionmark}[1]{\markright{\textsc{\thesection\ #1}}}
|
||||
|
|
Loading…
Reference in a new issue