From e18730e0e5645fc1b52ed6cc22c6443aa35e3602 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 8 May 2018 02:00:23 +0200 Subject: [PATCH] Remove tex warnings --- doc/chalmerstitle.sty | 12 +++++------- doc/cubical.tex | 24 ++++++++++++++---------- doc/introduction.tex | 2 +- doc/main.tex | 3 ++- doc/packages.tex | 2 +- 5 files changed, 23 insertions(+), 20 deletions(-) diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty index 631eaa8..a31e8a2 100644 --- a/doc/chalmerstitle.sty +++ b/doc/chalmerstitle.sty @@ -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} diff --git a/doc/cubical.tex b/doc/cubical.tex index db3ffbb..96a67ef 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -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 diff --git a/doc/introduction.tex b/doc/introduction.tex index 7a5d1a0..231097c 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -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$ \\ diff --git a/doc/main.tex b/doc/main.tex index bdf4b49..a74978c 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -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}} diff --git a/doc/packages.tex b/doc/packages.tex index 120699d..f592a65 100644 --- a/doc/packages.tex +++ b/doc/packages.tex @@ -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}}}