diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty index ac849be..5ec687e 100644 --- a/doc/chalmerstitle.sty +++ b/doc/chalmerstitle.sty @@ -39,6 +39,47 @@ \newcommand*{\researchgroup}[1]{\gdef\@researchgroup{#1}} \newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}} +%% \begin{titlepage} +\newgeometry{top=3cm, bottom=3cm, + left=2.25 cm, right=2.25cm} % Temporarily change margins +% Cover page background +%% \AddToShipoutPicture*{\backgroundpic{-4}{56.7}{figure/auxiliary/frontpage_gu_eng.pdf}} +%% \AddToShipoutPicture*{\backgroundpic{-4}{56.7}{logo_eng.pdf}} +%% \includegraphics[width=0.2\pdfpagewidth]{logo_eng.pdf} +%% \begin{center} +%% \includegraphics[width=0.5\paperwidth,height=\paperheight,keepaspectratio]{logo_eng.pdf}% +%% \end{center} +%% \addtolength{\voffset}{2cm} + +% Cover picture (replace with your own or delete) +{\Huge\@title}\\[.5cm] +{\Large A formalization of category theory in Cubical Agda}\\[2.5cm] +\begin{center} +\includegraphics[\linewidth,height=0.35\paperheight,keepaspectratio]{isomorphism.png} +\end{center} + +% Cover text +\vfill +%% \renewcommand{\familydefault}{\sfdefault} \normalfont % Set cover page font +Master's thesis in Computer Science \\[1cm] +{\Large\@author} \\[2cm] +\textsc{Department of Computer Science and Engineering}\\ +\textsc{Chalmers University of Technology}\\ +\textsc{University of Gothenburg}\\ +\textsc{Gothenburg, Sweden \the\year} + +%% \renewcommand{\familydefault}{\rmdefault} \normalfont % Reset standard font +%% \end{titlepage} + + +% BACK OF COVER PAGE (BLANK PAGE) +\newpage +\newgeometry{a4paper} % Temporarily change margins +\restoregeometry +\thispagestyle{empty} +\null + + \renewcommand*{\maketitle}{% \begin{titlepage} @@ -56,11 +97,11 @@ \includegraphics[width=0.2\pdfpagewidth]{logo_eng.pdf} \vspace{5mm} - Department of Computer Science and Engineering\\ - \emph{\@researchgroup}\\ + \textsc{Department of Computer Science and Engineering}\\ + \textsc{{\@researchgroup}}\\ %Name of research group (if applicable)\\ \textsc{\@institution} \\ - Gothenburg, Sweden \the\year \\ + \textsc{Gothenburg, Sweden \the\year}\\ \end{center} @@ -105,5 +146,5 @@ Telephone +46 31 772 1000 \setlength{\parskip}{0.5cm}\\ %Printed by [Name of printing company]\\ Gothenburg, Sweden \the\year - +\restoregeometry \end{titlepage}} diff --git a/doc/implementation.tex b/doc/implementation.tex index caf5c94..9194bae 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -149,7 +149,7 @@ $$ So to give the continuous function $I \to \IsPreCategory$ that is our goal we introduce $i \tp I$ and proceed by constructing an element of $\IsPreCategory$ by using that all the projections are propositions to generate paths between all -projections. Once we have such a path e.g. $p : \isIdentity_a \equiv +projections. Once we have such a path e.g. $p \tp \isIdentity_a \equiv \isIdentity_b$ we can elimiate it with $i$ and thus obtaining $p\ i \tp \isIdentity_{p\ i}$ and this element satisfies exactly that it corresponds to the corresponding projections at either endpoint. Thus the element we construct @@ -198,9 +198,9 @@ provide since, as we have shown, $\IsPreCategory$ is a proposition. However, even though $\Univalent$ is also a proposition, we cannot use this directly to show the latter. This is becasue $\isProp$ talks about non-dependent paths. To `promote' this to a dependent path we can use another useful combinator; -$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $B : A \to +$\lemPropF$. Given a type $A \tp \MCU$ and a type family on $A$; $B \tp A \to \MCU$. Let $P$ be a proposition indexed by an element of $A$ and say we have a -path between some two elements in $A$; $p : a_0 \equiv a_1$ then we can built a +path between some two elements in $A$; $p \tp a_0 \equiv a_1$ then we can built a heterogeneous path between any two $b$'s at the endpoints: % $$ @@ -240,15 +240,15 @@ here, but the curious reader can check the implementation for the details. \section{Equivalences} \label{sec:equiv} -The usual notion of a function $f : A \to B$ having an inverses is: +The usual notion of a function $f \tp A \to B$ having an inverses is: % $$ -\sum_{g : B \to A} f \comp g \equiv \identity_{B} \x g \comp f \equiv \identity_{A} +\sum_{g \tp B \to A} f \comp g \equiv \identity_{B} \x g \comp f \equiv \identity_{A} $$ % This is defined in \cite[p. 129]{hott-2013} and is referred to as the a quasi-inverse. At the same place \cite{hott-2013} gives an ``interface'' for -what an equivalence $\isEquiv : (A \to B) \to \MCU$ must supply: +what an equivalence $\isEquiv \tp (A \to B) \to \MCU$ must supply: % \begin{itemize} \item @@ -264,11 +264,11 @@ how to work with equivalences and 2) to use ad-hoc definitions of equivalences. The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is: % $$ -isEquiv\ f \defeq \prod_{b : B} \isContr\ (\fiber\ f\ b) +isEquiv\ f \defeq \prod_{b \tp B} \isContr\ (\fiber\ f\ b) $$ where $$ -\fiber\ f\ b \defeq \sum_{a \tp A} b \equiv f\ a +\fiber\ f\ b \defeq \sum_{a \tp A} \left( b \equiv f\ a \right) $$ % I give it's definition here mainly for completeness, because as I stated we can @@ -473,7 +473,7 @@ B$ is simply an arrow $f \tp \mathit{Arrow}\ A\ B$ and it's inverse $g \tp \mathit{Arrow}\ B\ A$. In the opposite category $g$ will play the role of the isomorphism and $f$ will be the inverse. Similarly we can go in the opposite direction. I name these maps $\mathit{shuffle} \tp (A \approxeq B) \to (A -\approxeq_{\bC} B)$ and $\mathit{shuffle}^{-1} : (A \approxeq_{\bC} B) \to (A +\approxeq_{\bC} B)$ and $\mathit{shuffle}^{-1} \tp (A \approxeq_{\bC} B) \to (A \approxeq B)$ respectively. As the inverse of $\idToIso_{\mathit{Op}}$ I will pick $\zeta \defeq \eta \comp @@ -670,7 +670,7 @@ proposition and then use $\lemPropF$. So we prove the generalization: % \begin{align} \label{eq:propAreInversesGen} -\prod_{g : B \to A} \isProp\ (\mathit{AreInverses}\ f\ g) +\prod_{g \tp B \to A} \isProp\ (\mathit{AreInverses}\ f\ g) \end{align} % But $\mathit{AreInverses}\ f\ g$ is a pair of equations on arrows, so we use @@ -716,8 +716,6 @@ that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying %% \prod_{X \tp Object} \prod_{f \tp \Arrow\ X\ A} \prod_{g \tp \Arrow\ X\ B}\\ %% \uexists_{f \x g \tp \Arrow\ X\ (A \x B)} \pi_1 \lll \pi \equiv f \x \pi_2 \lll \pi \equiv g -%% ump : ∀ {X : Object} (f : ℂ [ X , A ]) (g : ℂ [ X , B ]) -%% → ∃![ f×g ] (ℂ [ fst ∘ f×g ] ≡ f P.× ℂ [ snd ∘ f×g ] ≡ g) \end{align} % $\pi$ is called the product (arrow) of $f$ and $g$. diff --git a/doc/macros.tex b/doc/macros.tex index 0f719db..23ce2c3 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -5,7 +5,7 @@ \hbox{\scriptsize.}\hbox{\scriptsize.}}}% =} -\newcommand{\defeq}{\triangleq} +\newcommand{\defeq}{\mathrel{\triangleq}} %% Alternatively: %% \newcommand{\defeq}{≔} \newcommand{\bN}{\mathbb{N}} @@ -21,7 +21,7 @@ \newcommand{\comp}{\circ} \newcommand{\x}{\times} \newcommand\inv[1]{#1\raisebox{1.15ex}{$\scriptscriptstyle-\!1$}} -\newcommand{\tp}{\;\mathord{:}\;} +\newcommand{\tp}{\mathrel{:}} \newcommand{\Type}{\mathcal{U}} \usepackage{graphicx} diff --git a/doc/main.tex b/doc/main.tex index 7e8813f..b0946e1 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -4,7 +4,7 @@ \input{packages.tex} \input{macros.tex} -\title{Univalent Categories in Cubical Agda} +\title{Univalent Categories} \author{Frederik Hanghøj Iversen} %% \usepackage[ @@ -26,7 +26,7 @@ %% researchgroup=Programming Logic Group %% ]{chalmerstitle} \usepackage{chalmerstitle} -\subtitle{} +\subtitle{A formalization of category theory in Cubical Agda} \authoremail{hanghj@student.chalmers.se} \newcommand{\chalmers}{Chalmers University of Technology} \supervisor{Thierry Coquand} diff --git a/doc/packages.tex b/doc/packages.tex index c6ff2ae..5d789a2 100644 --- a/doc/packages.tex +++ b/doc/packages.tex @@ -15,7 +15,7 @@ \usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym} \usepackage[toc,page]{appendix} \usepackage{xspace} -%% \usepackage{geometry} +\usepackage{geometry} % \setlength{\parskip}{10pt}