diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty index 76a8111..d224ac3 100644 --- a/doc/chalmerstitle.sty +++ b/doc/chalmerstitle.sty @@ -4,45 +4,85 @@ \newcommand*{\authoremail}[1]{\gdef\@authoremail{#1}} \newcommand*{\supervisor}[1]{\gdef\@supervisor{#1}} \newcommand*{\supervisoremail}[1]{\gdef\@supervisoremail{#1}} +\newcommand*{\supervisordepartment}[1]{\gdef\@supervisordepartment{#1}} \newcommand*{\cosupervisor}[1]{\gdef\@cosupervisor{#1}} \newcommand*{\cosupervisoremail}[1]{\gdef\@cosupervisoremail{#1}} +\newcommand*{\cosupervisordepartment}[1]{\gdef\@cosupervisordepartment{#1}} +\newcommand*{\examiner}[1]{\gdef\@examiner{#1}} +\newcommand*{\examineremail}[1]{\gdef\@examineremail{#1}} +\newcommand*{\examinerdepartment}[1]{\gdef\@examinerdepartment{#1}} \newcommand*{\institution}[1]{\gdef\@institution{#1}} +\newcommand*{\department}[1]{\gdef\@department{#1}} +\newcommand*{\researchgroup}[1]{\gdef\@researchgroup{#1}} \renewcommand*{\maketitle}{% \begin{titlepage} - +% TITLE PAGE +\newpage +\thispagestyle{empty} \begin{center} + \textsc{\LARGE Master's thesis \the\year}\\[4cm] % Report number is currently not in use + \textbf{\LARGE \@title} \\[1cm] + {\large \@subtitle}\\[1cm] + {\large \@author} + + \vfill + \centering + \includegraphics[width=0.2\pdfpagewidth]{logo_eng.pdf} + \vspace{5mm} + + Department of Computer Science and Engineering\\ + \emph{\@researchgroup}\\ + %Name of research group (if applicable)\\ + \textsc{\@institution} \\ + Gothenburg, Sweden \the\year \\ +\end{center} -{\scshape\LARGE Master thesis\\} +% IMPRINT PAGE (BACK OF TITLE PAGE) +\newpage +\thispagestyle{plain} +\vspace*{4.5cm} +\@title\\ +\@subtitle\\ +\textbf{Author:}\\ +\@author\\ +\href{mailto:\@authoremail>}{\texttt{<\@authoremail>}} +\setlength{\parskip}{1cm} -\vspace{0.5cm} +\copyright ~ \MakeUppercase{\@author}, \the\year. -{\LARGE\bfseries \@title\\} +\setlength{\parskip}{0.5cm} +\textbf{Supervisor:}\\ +\@supervisor\\ +\href{mailto:\@supervisoremail>}{\texttt{<\@supervisoremail>}}\\ +\@supervisordepartment -\vspace{2cm} +\textbf{Co-supervisor:}\\ +\@cosupervisor\\ +\href{mailto:\@cosupervisoremail>}{\texttt{<\@cosupervisoremail>}}\\ +\@cosupervisordepartment -{\Large \@author\\ \href{mailto:\@authoremail>}{\texttt{<\@authoremail>}} \\} +\textbf{Examiner:}\\ +\@examiner\\ +\href{mailto:\@examineremail>}{\texttt{<\@examineremail>}}\\ +\@examinerdepartment\setlength{\parskip}{1cm} -% \vspace{0.2cm} -% -% {\Large name and email adress of student 2\\} - -\vspace{1.0cm} - -{\large Supervisor: \@supervisor\\ \href{mailto:\@supervisoremail>}{\texttt{<\@supervisoremail>}}\\} - -\vspace{0.2cm} - -{\large Co-supervisor: \@cosupervisor\\ \href{mailto:\@cosupervisoremail>}{\texttt{<\@cosupervisoremail>}}\\} - -\vspace{1.5cm} +Master's Thesis \the\year\\ % Report number currently not in use +\@department\\ +%Division of Division name\\ +%Name of research group (if applicable)\\ +\@institution\\ +SE-412 96 Gothenburg\\ +Telephone +46 31 772 1000 \setlength{\parskip}{0.5cm} \vfill +% Caption for cover page figure if used, possibly with reference to further information in the report +%% Cover: Wind visualization constructed in Matlab showing a surface of constant wind speed along with streamlines of the flow. \setlength{\parskip}{0.5cm} -{\large \@institution\\\today\\} +%Printed by [Name of printing company]\\ +Gothenburg, Sweden \the\year -\end{center} -\end{titlepage} -} + +\end{titlepage}} diff --git a/doc/implementation.tex b/doc/implementation.tex index 02ca940..70af29a 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -691,6 +691,7 @@ are propositional in a proper category and equivalences preservehomotopy level, then we know that products also are propositions. But before we get to that, let's recall the definition of products. +\subsection{Products} Given a category $\bC$ and two objects $A$ and $B$ in $bC$ we define the product of $A$ and $B$ to be an object $A \x B$ in $\bC$ and two arrows $\pi_1 \tp A \x B \to A$ and $\pi_2 \tp A \x B \to B$ called the projections of the product. The projections must satisfy the following property: @@ -709,6 +710,54 @@ that there exists a unique arrow $\pi \tp \Arrow\ X\ (A \x B)$ satisfying $ $\pi$ is called the product (arrow) of $f$ and $g$. +\subsection{Pair category} + +\newcommand\pairA{\mathcal{A}} +\newcommand\pairB{\mathcal{B}} +Given a base category $\bC$ and two objects in this category $\pairA$ and +$\pairrB$ we can construct the ``pair category'': \TODO{This is a working title, + it's nice to have a name for this thing to refer back to} + +The type objects in this category will be an object in the underlying category, +$X$, and two arrows (also from the underlying category) +$\Arrow\ X\ \pairA$ and $\Arrow\ X\ \pairB$. + +\newcommand\pairf{\ensuremath{f}} +\newcommand\pairFst{\mathcal{\pi_1}} +\newcommand\pairSnd{\mathcal{\pi_2}} + +An arrow between objects $A ,\ a_0 ,\ a_1$ and $B ,\ b_0 ,\ b_1$ in this +category will consist of an arrow from the underlying category $\pairf \tp +\Arrow\ A\ B$ satisfying: +% +\begin{align} +\begin{split} +\label{eq:pairArrowLaw} +b_0 \lll f & \equiv a_0 \\ +b_1 \lll f & \equiv a_1 +\end{split} +\end{align} + +The identity morphism is the identity morphism from the underlying category. +This choice satisfies \ref{eq:pairArrowLaw} because of the right-identity law +from the underlying category. + +For composition of arrows $f \tp \Arrow\ A\ B$ and $g \tp \Arrow\ B\ C$ we +choose $g \lll f$ and we must now verify that it satisfies +\ref{eq:pairArrowLaw}: +% +\begin{align*} + c_0 \lll (f \lll g) + & \equiv + (c_0 \lll f) \lll g + && \text{Associativity} \\ + & \equiv + b_0 \lll g + && \text{$f$ satisfies \ref{eq:pairArrowLaw}} \\ + & \equiv + a_0 + && \text{$g$ satisfies \ref{eq:pairArrowLaw}} \\ +\end{align*} \section{Monads} diff --git a/doc/macros.tex b/doc/macros.tex index 6a2a0ee..d43b2c4 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -22,46 +22,46 @@ \newcommand{\tp}{\;\mathord{:}\;} \newcommand{\Type}{\mathcal{U}} -\newcommand{\var}[1]{\mathit{#1}} -\newcommand{\Hom}{\mathit{Hom}} -\newcommand{\fmap}{\mathit{fmap}} -\newcommand{\idFun}{\mathit{id}} -\newcommand{\Sets}{\mathit{Sets}} -\newcommand{\Set}{\mathit{Set}} -\newcommand{\hSet}{\mathit{hSet}} -\newcommand{\id}{\mathit{id}} -\newcommand{\isEquiv}{\mathit{isEquiv}} -\newcommand{\idToIso}{\mathit{idToIso}} -\newcommand{\isSet}{\mathit{isSet}} -\newcommand{\isContr}{\mathit{isContr}} -\newcommand\Object{\mathit{Object}} -\newcommand\Functor{\mathit{Functor}} -\newcommand\isProp{\mathit{isProp}} -\newcommand\propPi{\mathit{propPi}} -\newcommand\propSig{\mathit{propSig}} -\newcommand\PreCategory{\mathit{PreCategory}} -\newcommand\IsPreCategory{\mathit{IsPreCategory}} -\newcommand\isIdentity{\mathit{isIdentity}} -\newcommand\propIsIdentity{\mathit{propIsIdentity}} -\newcommand\IsCategory{\mathit{IsCategory}} -\newcommand\Gl{\mathit{\lambda}} -\newcommand\lemPropF{\mathit{lemPropF}} -\newcommand\isPreCategory{\mathit{isPreCategory}} -\newcommand\congruence{\mathit{cong}} -\newcommand\identity{\mathit{identity}} -\newcommand\isequiv{\mathit{isequiv}} -\newcommand\qinv{\mathit{qinv}} -\newcommand\fiber{\mathit{fiber}} -\newcommand\shuffle{\mathit{shuffle}} -\newcommand\Univalent{\mathit{Univalent}} -\newcommand\refl{\mathit{refl}} -\newcommand\isoToId{\mathit{isoToId}} +\newcommand{\var}[1]{\ensuremath{\mathit{#1}}} +\newcommand{\Hom}{\var{Hom}} +\newcommand{\fmap}{\var{fmap}} +\newcommand{\idFun}{\var{id}} +\newcommand{\Sets}{\var{Sets}} +\newcommand{\Set}{\var{Set}} +\newcommand{\hSet}{\var{hSet}} +\newcommand{\id}{\var{id}} +\newcommand{\isEquiv}{\var{isEquiv}} +\newcommand{\idToIso}{\var{idToIso}} +\newcommand{\isSet}{\var{isSet}} +\newcommand{\isContr}{\var{isContr}} +\newcommand\Object{\var{Object}} +\newcommand\Functor{\var{Functor}} +\newcommand\isProp{\var{isProp}} +\newcommand\propPi{\var{propPi}} +\newcommand\propSig{\var{propSig}} +\newcommand\PreCategory{\var{PreCategory}} +\newcommand\IsPreCategory{\var{IsPreCategory}} +\newcommand\isIdentity{\var{isIdentity}} +\newcommand\propIsIdentity{\var{propIsIdentity}} +\newcommand\IsCategory{\var{IsCategory}} +\newcommand\Gl{\var{\lambda}} +\newcommand\lemPropF{\var{lemPropF}} +\newcommand\isPreCategory{\var{isPreCategory}} +\newcommand\congruence{\var{cong}} +\newcommand\identity{\var{identity}} +\newcommand\isequiv{\var{isequiv}} +\newcommand\qinv{\var{qinv}} +\newcommand\fiber{\var{fiber}} +\newcommand\shuffle{\var{shuffle}} +\newcommand\Univalent{\var{Univalent}} +\newcommand\refl{\var{refl}} +\newcommand\isoToId{\var{isoToId}} \newcommand\rrr{\ggg} -\newcommand\fst{\mathit{fst}} -\newcommand\snd{\mathit{snd}} -\newcommand\Path{\mathit{Path}} -\newcommand\Category{\mathit{Category}} +\newcommand\fst{\var{fst}} +\newcommand\snd{\var{snd}} +\newcommand\Path{\var{Path}} +\newcommand\Category{\var{Category}} \newcommand\TODO[1]{TODO: \emph{#1}} \newcommand*{\QED}{\hfill\ensuremath{\square}}% \newcommand\uexists{\exists!} -\newcommand\Arrow{\mathit{Arrow}} +\newcommand\Arrow{\var{Arrow}} diff --git a/doc/main.tex b/doc/main.tex index bae31dd..f133be7 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -1,22 +1,34 @@ -\documentclass{report} +\documentclass[a4paper]{report} +%% \documentclass[compact,a4paper]{article} \input{packages.tex} \input{macros.tex} -\title{Univalent categories} +\title{Univalent categories in cubical Agda} +\subtitle{} \author{Frederik Hanghøj Iversen} \authoremail{hanghj@student.chalmers.se} +\newcommand{\chalmers}{Chalmers University of Technology} \supervisor{Thierry Coquand} \supervisoremail{coquand@chalmers.se} +\supervisordepartment{\chalmers} \cosupervisor{Andrea Vezzosi} \cosupervisoremail{vezzosi@chalmers.se} -\institution{Chalmers University of Technology} +\cosupervisordepartment{\chalmers} +\examiner{Andreas Abel} +\examineremail{abela@chalmers.se} +\examinerdepartment{\chalmers} +\institution{\chalmers} +\department{Department of Computer Science and Engineering} +\researchgroup{Programming Logic Group} \begin{document} +\pagenumbering{roman} \maketitle \tableofcontents - +% +\pagenumbering{arabic} \chapter{Introduction} \input{introduction.tex} @@ -27,7 +39,10 @@ \nocite{cubical-demo} \nocite{coquand-2013} \bibliography{refs} + \begin{appendices} +\setcounter{page}{1} +\pagenumbering{roman} %% \input{planning.tex} %% \input{halftime.tex} \end{appendices} diff --git a/doc/packages.tex b/doc/packages.tex index c55dad5..b786de2 100644 --- a/doc/packages.tex +++ b/doc/packages.tex @@ -1,7 +1,12 @@ \usepackage[utf8]{inputenc} \usepackage{natbib} -\usepackage[hidelinks]{hyperref} +\usepackage[ + hidelinks, + pdfusetitle, + pdfsubject={category theory}, + pdfkeywords={type theory, homotopy theory, category theory, agda}] + {hyperref} \usepackage{graphicx} @@ -10,6 +15,7 @@ \usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym} \usepackage[toc,page]{appendix} \usepackage{xspace} +%% \usepackage{geometry} % \setlength{\parskip}{10pt}