fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Change title-page, write stuff about products

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-04-25 08:21:45 +02:00
parent 6b6e6672e0
commit 9a8b09e15f
5 changed files with 177 additions and 67 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

86
doc/chalmerstitle.sty
View file

@ -4,45 +4,85 @@
\newcommand*{\authoremail}[1]{\gdef\@authoremail{#1}} \newcommand*{\authoremail}[1]{\gdef\@authoremail{#1}}
\newcommand*{\supervisor}[1]{\gdef\@supervisor{#1}} \newcommand*{\supervisor}[1]{\gdef\@supervisor{#1}}
\newcommand*{\supervisoremail}[1]{\gdef\@supervisoremail{#1}} \newcommand*{\supervisoremail}[1]{\gdef\@supervisoremail{#1}}
\newcommand*{\supervisordepartment}[1]{\gdef\@supervisordepartment{#1}}
\newcommand*{\cosupervisor}[1]{\gdef\@cosupervisor{#1}} \newcommand*{\cosupervisor}[1]{\gdef\@cosupervisor{#1}}
\newcommand*{\cosupervisoremail}[1]{\gdef\@cosupervisoremail{#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*{\institution}[1]{\gdef\@institution{#1}}
\newcommand*{\department}[1]{\gdef\@department{#1}}
\newcommand*{\researchgroup}[1]{\gdef\@researchgroup{#1}}
\renewcommand*{\maketitle}{% \renewcommand*{\maketitle}{%
\begin{titlepage} \begin{titlepage}
% TITLE PAGE
\newpage
\thispagestyle{empty}
\begin{center} \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} Master's Thesis \the\year\\ % Report number currently not in use
% \@department\\
% {\Large name and email adress of student 2\\} %Division of Division name\\
%Name of research group (if applicable)\\
\vspace{1.0cm} \@institution\\
SE-412 96 Gothenburg\\
{\large Supervisor: \@supervisor\\ \href{mailto:\@supervisoremail>}{\texttt{<\@supervisoremail>}}\\} Telephone +46 31 772 1000 \setlength{\parskip}{0.5cm}
\vspace{0.2cm}
{\large Co-supervisor: \@cosupervisor\\ \href{mailto:\@cosupervisoremail>}{\texttt{<\@cosupervisoremail>}}\\}
\vspace{1.5cm}
\vfill \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}}
}

49
doc/implementation.tex
View file

@ -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, then we know that products also are propositions. But before we get to that,
let's recall the definition of products. 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 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 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: 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$. $\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} \section{Monads}

78
doc/macros.tex
View file

@ -22,46 +22,46 @@
\newcommand{\tp}{\;\mathord{:}\;} \newcommand{\tp}{\;\mathord{:}\;}
\newcommand{\Type}{\mathcal{U}} \newcommand{\Type}{\mathcal{U}}
\newcommand{\var}[1]{\mathit{#1}} \newcommand{\var}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\Hom}{\mathit{Hom}} \newcommand{\Hom}{\var{Hom}}
\newcommand{\fmap}{\mathit{fmap}} \newcommand{\fmap}{\var{fmap}}
\newcommand{\idFun}{\mathit{id}} \newcommand{\idFun}{\var{id}}
\newcommand{\Sets}{\mathit{Sets}} \newcommand{\Sets}{\var{Sets}}
\newcommand{\Set}{\mathit{Set}} \newcommand{\Set}{\var{Set}}
\newcommand{\hSet}{\mathit{hSet}} \newcommand{\hSet}{\var{hSet}}
\newcommand{\id}{\mathit{id}} \newcommand{\id}{\var{id}}
\newcommand{\isEquiv}{\mathit{isEquiv}} \newcommand{\isEquiv}{\var{isEquiv}}
\newcommand{\idToIso}{\mathit{idToIso}} \newcommand{\idToIso}{\var{idToIso}}
\newcommand{\isSet}{\mathit{isSet}} \newcommand{\isSet}{\var{isSet}}
\newcommand{\isContr}{\mathit{isContr}} \newcommand{\isContr}{\var{isContr}}
\newcommand\Object{\mathit{Object}} \newcommand\Object{\var{Object}}
\newcommand\Functor{\mathit{Functor}} \newcommand\Functor{\var{Functor}}
\newcommand\isProp{\mathit{isProp}} \newcommand\isProp{\var{isProp}}
\newcommand\propPi{\mathit{propPi}} \newcommand\propPi{\var{propPi}}
\newcommand\propSig{\mathit{propSig}} \newcommand\propSig{\var{propSig}}
\newcommand\PreCategory{\mathit{PreCategory}} \newcommand\PreCategory{\var{PreCategory}}
\newcommand\IsPreCategory{\mathit{IsPreCategory}} \newcommand\IsPreCategory{\var{IsPreCategory}}
\newcommand\isIdentity{\mathit{isIdentity}} \newcommand\isIdentity{\var{isIdentity}}
\newcommand\propIsIdentity{\mathit{propIsIdentity}} \newcommand\propIsIdentity{\var{propIsIdentity}}
\newcommand\IsCategory{\mathit{IsCategory}} \newcommand\IsCategory{\var{IsCategory}}
\newcommand\Gl{\mathit{\lambda}} \newcommand\Gl{\var{\lambda}}
\newcommand\lemPropF{\mathit{lemPropF}} \newcommand\lemPropF{\var{lemPropF}}
\newcommand\isPreCategory{\mathit{isPreCategory}} \newcommand\isPreCategory{\var{isPreCategory}}
\newcommand\congruence{\mathit{cong}} \newcommand\congruence{\var{cong}}
\newcommand\identity{\mathit{identity}} \newcommand\identity{\var{identity}}
\newcommand\isequiv{\mathit{isequiv}} \newcommand\isequiv{\var{isequiv}}
\newcommand\qinv{\mathit{qinv}} \newcommand\qinv{\var{qinv}}
\newcommand\fiber{\mathit{fiber}} \newcommand\fiber{\var{fiber}}
\newcommand\shuffle{\mathit{shuffle}} \newcommand\shuffle{\var{shuffle}}
\newcommand\Univalent{\mathit{Univalent}} \newcommand\Univalent{\var{Univalent}}
\newcommand\refl{\mathit{refl}} \newcommand\refl{\var{refl}}
\newcommand\isoToId{\mathit{isoToId}} \newcommand\isoToId{\var{isoToId}}
\newcommand\rrr{\ggg} \newcommand\rrr{\ggg}
\newcommand\fst{\mathit{fst}} \newcommand\fst{\var{fst}}
\newcommand\snd{\mathit{snd}} \newcommand\snd{\var{snd}}
\newcommand\Path{\mathit{Path}} \newcommand\Path{\var{Path}}
\newcommand\Category{\mathit{Category}} \newcommand\Category{\var{Category}}
\newcommand\TODO[1]{TODO: \emph{#1}} \newcommand\TODO[1]{TODO: \emph{#1}}
\newcommand*{\QED}{\hfill\ensuremath{\square}}% \newcommand*{\QED}{\hfill\ensuremath{\square}}%
\newcommand\uexists{\exists!} \newcommand\uexists{\exists!}
\newcommand\Arrow{\mathit{Arrow}} \newcommand\Arrow{\var{Arrow}}

23
doc/main.tex
View file

@ -1,22 +1,34 @@
\documentclass{report} \documentclass[a4paper]{report}
%% \documentclass[compact,a4paper]{article}
\input{packages.tex} \input{packages.tex}
\input{macros.tex} \input{macros.tex}
\title{Univalent categories} \title{Univalent categories in cubical Agda}
\subtitle{}
\author{Frederik Hanghøj Iversen} \author{Frederik Hanghøj Iversen}
\authoremail{hanghj@student.chalmers.se} \authoremail{hanghj@student.chalmers.se}
\newcommand{\chalmers}{Chalmers University of Technology}
\supervisor{Thierry Coquand} \supervisor{Thierry Coquand}
\supervisoremail{coquand@chalmers.se} \supervisoremail{coquand@chalmers.se}
\supervisordepartment{\chalmers}
\cosupervisor{Andrea Vezzosi} \cosupervisor{Andrea Vezzosi}
\cosupervisoremail{vezzosi@chalmers.se} \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} \begin{document}
\pagenumbering{roman}
\maketitle \maketitle
\tableofcontents \tableofcontents
%
\pagenumbering{arabic}
\chapter{Introduction} \chapter{Introduction}
\input{introduction.tex} \input{introduction.tex}
@ -27,7 +39,10 @@
\nocite{cubical-demo} \nocite{cubical-demo}
\nocite{coquand-2013} \nocite{coquand-2013}
\bibliography{refs} \bibliography{refs}
\begin{appendices} \begin{appendices}
\setcounter{page}{1}
\pagenumbering{roman}
%% \input{planning.tex} %% \input{planning.tex}
%% \input{halftime.tex} %% \input{halftime.tex}
\end{appendices} \end{appendices}

8
doc/packages.tex
View file

@ -1,7 +1,12 @@
\usepackage[utf8]{inputenc} \usepackage[utf8]{inputenc}
\usepackage{natbib} \usepackage{natbib}
\usepackage[hidelinks]{hyperref} \usepackage[
hidelinks,
pdfusetitle,
pdfsubject={category theory},
pdfkeywords={type theory, homotopy theory, category theory, agda}]
{hyperref}
\usepackage{graphicx} \usepackage{graphicx}
@ -10,6 +15,7 @@
\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym} \usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym}
\usepackage[toc,page]{appendix} \usepackage[toc,page]{appendix}
\usepackage{xspace} \usepackage{xspace}
%% \usepackage{geometry}
% \setlength{\parskip}{10pt} % \setlength{\parskip}{10pt}