diff --git a/doc/cubical.tex b/doc/cubical.tex index a5d8135..6e07ac9 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -61,7 +61,7 @@ $I$. I will sometimes refer to $P$ as the \nomenindex{path space} of some path $ \Path\ P\ a\ b$. By this token $P\ 0$ then corresponds to the type at the left-endpoint and $P\ 1$ as the type at the right-endpoint. The type is called $\Path$ because it is connected with paths in homotopy theory. The intuition -behind this is that $\Path$ describes paths in $\MCU$ -- i.e. between types. For +behind this is that $\Path$ describes paths in $\MCU$ -- i.e.\ between types. For a path $p$ for the point $p\ i$ the index $i$ describes how far along the path one has moved. An inhabitant of $\Path\ P\ a_0\ a_1$ is a (dependent-) function, $p$, from the index-space to the path space: @@ -104,7 +104,7 @@ With this definition we can also recover reflexivity. That is, for any $A \tp Here the path space is $P \defeq \lambda i \to A$ and it satsifies $P\ i = A$ definitionally. So to inhabit it, is to give a path $I \to A$ which is judgmentally $a$ at either endpoint. This is satisfied by the constant path; -i.e. the path that stays at $a$ at any index $i$. +i.e.\ the path that stays at $a$ at any index $i$. It is also surpisingly easy to show functional extensionality with which we can construct a path between $f$ and $g$ -- the functions defined in the @@ -207,7 +207,7 @@ Then comes the set of homotopical sets: \end{equation} % I will not give an example of a set at this point. It turns out that proving -e.g. $\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}). +e.g.\ $\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}). There will be examples of sets later in this report. At this point it should be noted that the term ``set'' is somewhat conflated; there is the notion of sets from set-theory, in Agda types are denoted \texttt{Set}. I will use it diff --git a/doc/discussion.tex b/doc/discussion.tex index 771d4ef..58c687c 100644 --- a/doc/discussion.tex +++ b/doc/discussion.tex @@ -15,7 +15,7 @@ formalized this common result about monads: By transporting this to the Kleisli formulation we get a result that we can use to compute with. This is particularly useful because the Kleisli formulation -will be more familiar to programmers e.g. those coming from a background in +will be more familiar to programmers e.g.\ those coming from a background in Haskell. Whereas the theory usually talks about monoidal monads. \TODO{Mention that with postulates we cannot do this} diff --git a/doc/halftime.tex b/doc/halftime.tex index ca6d9a9..49cb880 100644 --- a/doc/halftime.tex +++ b/doc/halftime.tex @@ -3,7 +3,7 @@ I've written this as an appendix because 1) the aim of the thesis changed drastically from the planning report/proposal 2) partly I'm not sure how to structure my thesis. -My work so far has very much focused on the formalization, i.e. coding. It's +My work so far has very much focused on the formalization, i.e.\ coding. It's unclear to me at this point what I should have in the final report. Here I will describe what I have managed to formalize so far and what outstanding challenges I'm facing. diff --git a/doc/implementation.tex b/doc/implementation.tex index 94198b6..5cb5047 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -202,7 +202,7 @@ set. This example illustrates nicely how we can use these combinators to reason about `canonical' types like $\sum$ and $\prod$. Similar combinators can be defined at the other homotopic levels. These combinators are however not applicable in -situations where we want to reason about other types - e.g. types we have +situations where we want to reason about other types - e.g.\ types we have defined ourselves. For instance, after we have proven that all the projections of pre categories are propositions, then we would like to bundle this up to show that the type of pre categories is also a proposition. Formally: @@ -247,7 +247,7 @@ $$ So to give the continuous function $I \to \IsPreCategory$, which is our goal, we introduce $i \tp I$ and proceed by constructing an element of $\IsPreCategory$ by using the fact that all the projections are propositions to generate paths -between all projections. Once we have such a path e.g. $p \tp a.\isIdentity +between all projections. Once we have such a path e.g.\ $p \tp a.\isIdentity \equiv b.\isIdentity$ we can eliminate it with $i$ and thus obtain $p\ i \tp (p\ i).\isIdentity$. This element satisfies exactly that it corresponds to the corresponding projections at either endpoint. Thus the element we construct at @@ -436,7 +436,7 @@ That is, we must demonstrate that there is an isomorphism (on types) between equalities and isomorphisms (on arrows). It is worthwhile to dwell on this for a few seconds. This type looks very similar to univalence for types and is therefore perhaps a bit more intuitive to grasp the implications of. Of course -univalence for types (which is a proposition -- i.e. provable) does not imply +univalence for types (which is a proposition -- i.e.\ provable) does not imply univalence of all pre category since morphisms in a category are not regular functions -- in stead they can be thought of as a generalization hereof. The univalence criterion therefore is simply a way of restricting arrows to behave similarly to maps. @@ -551,7 +551,7 @@ same as the one in the underlying category (they have the same type). Function composition will be reverse function composition from the underlying category. I will refer to things in terms of the underlying category, unless they have an -over-bar. So e.g. $\idToIso$ is a function in the underlying category and the +over-bar. So e.g.\ $\idToIso$ is a function in the underlying category and the corresponding thing is denoted $\wideoverbar{\idToIso}$ in the opposite category. @@ -1333,7 +1333,7 @@ f \rrr (\bind\ g)$ . (\TODO{Better way to typeset $\fish$?}) \subsection{Equivalence of formulations} % The notation I have chosen here in the report -overloads e.g. $\pure$ to both refer to a natural transformation and an arrow. +overloads e.g.\ $\pure$ to both refer to a natural transformation and an arrow. This is of course not a coincidence as the arrow in the Kleisli formulation shall correspond exactly to the map on arrows from the natural transformation called $\pure$. diff --git a/doc/introduction.tex b/doc/introduction.tex index b29d6b5..2441614 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -185,16 +185,16 @@ will make it possible to prove more things and to reuse proofs and to try and compare some aspects of this formalization with the existing ones.\TODO{How can I live up to this?} -There are alternative approaches to working in a cubical setting where one can -still have univalence and functional extensionality. One option is to postulate -these as axioms. This approach, however, has other shortcomings, e.g.; you lose - -\nomenindex{canonicity} (\TODO{Pageno!} \cite{huber-2016}). Canonicity means that any -well typed term evaluates to a \emph{canonical} form. For example for a closed -term $e \tp \bN$ it will be the case that $e$ reduces to $n$ applications of -$\mathit{suc}$ to $0$ for some $n$; $e = \mathit{suc}^n\ 0$. Without canonicity -terms in the language can get ``stuck'' -- meaning that they do not reduce to a -canonical form. +There are alternative approaches to working in a cubical setting where +one can still have univalence and functional extensionality. One +option is to postulate these as axioms. This approach, however, has +other shortcomings, e.g. you lose \nomenindex{canonicity} +(\TODO{Pageno!} \cite{huber-2016}). Canonicity means that any well +typed term evaluates to a \emph{canonical} form. For example for a +closed term $e \tp \bN$ it will be the case that $e$ reduces to $n$ +applications of $\mathit{suc}$ to $0$ for some $n$; $e = +\mathit{suc}^n\ 0$. Without canonicity terms in the language can get +``stuck'' -- meaning that they do not reduce to a canonical form. Another approach is to use the \emph{setoid interpretation} of type theory (\cite{hofmann-1995,huber-2016}). With this approach one works diff --git a/doc/presentation.tex b/doc/presentation.tex new file mode 100644 index 0000000..40d345f --- /dev/null +++ b/doc/presentation.tex @@ -0,0 +1,236 @@ +\documentclass[a4paper,handout]{beamer} +\input{packages.tex} +\input{macros.tex} +\title{Univalent Categories} +\author{Frederik Hangh{\o}j Iversen} +\institute{Chalmers University of Technology} +\begin{document} +\frame{\titlepage} + +\begin{frame} + \frametitle{Motivating example} + \framesubtitle{Functional extensionality} +Consider the functions +\begin{align*} + \var{zeroLeft} & \defeq (n \tp \bN) \mto (0 + n \tp \bN) \\ + \var{zeroRight} & \defeq (n \tp \bN) \mto (n + 0 \tp \bN) +\end{align*} +\pause +We have +% +$$ +\prod_{n \tp \bN} n + 0 \equiv 0 + n +$$ +% +\pause +But not +% +$$ +\var{zeroLeft} \equiv \var{zeroRight} +$$ +% +\pause +We need +% +$$ +\funExt \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g +$$ + +\end{frame} +\begin{frame} + \frametitle{Motivating example} + \framesubtitle{Univalence} + Consider the set + $\{x \mid \phi\ x \land \psi\ x\}$ + \pause + + If we show $\forall x . \psi\ x \equiv \top$ + then we want to conclude + $\{x \mid \phi\ x \land \psi\ x\} \equiv \{x \mid \phi\ x\}$ + \pause + + We need univalence: + $$(A \simeq B) \simeq (A \equiv B)$$ + \pause +% + We will return to $\simeq$, but for not, think of it as an + isomorphism, so it induces maps: + \begin{align*} + \var{toPath} & \tp (A \simeq B) \to (A \equiv B) \\ + \var{toEquiv} & \tp (A \equiv B) \to (A \simeq B) + \end{align*} +\end{frame} +\begin{frame} + \frametitle{Paths} + \framesubtitle{Definition} +Heterogeneous paths +\begin{equation*} + \Path \tp (P \tp I → \MCU) → P\ 0 → P\ 1 → \MCU +\end{equation*} +\pause + For $P \tp I \to \MCU$, $A \tp \MCU$ and $a_0, a_1 \tp A$ + inhabitants of $\Path\ P\ a_0\ a_1$ are like functions +% +$$ +p \tp \prod_{i \tp I} P\ i +$$ +% +Which satisfy $p\ 0 & = a_0$ and $p\ 1 & = a_1$ +\pause + +Homogenous paths +$$ +a_0 \equiv a_1 \defeq \Path\ (\var{const}\ A)\ a_0\ a_1 +$$ +\end{frame} +\begin{frame} +\frametitle{Paths} +\framesubtitle{Functional extenstionality} +$$ +\funExt & \tp \prod_{a \tp A} f\ a \equiv g\ a \to f \equiv g +$$ +\pause +$$ +\funExt\ p \defeq λ i\ a → p\ a\ i +$$ +\pause +$$ +\funExt\ (\var{const}\ \refl) +\tp +\var{zeroLeft} \equiv \var{zeroRight} +$$ +\end{frame} +\begin{frame} + \frametitle{Paths} + \framesubtitle{Homotopy levels} +\begin{align*} +& \isContr && \tp \MCU \to \MCU \\ +& \isContr\ A && \defeq \sum_{c \tp A} \prod_{a \tp A} a \equiv c +\end{align*} +\pause +\begin{align*} +& \isProp && \tp \MCU \to \MCU \\ +& \isProp\ A && \defeq \prod_{a_0, a_1 \tp A} a_0 \equiv a_1 +\end{align*} +\pause +\begin{align*} +& \isSet && \tp \MCU \to \MCU \\ +& \isSet\ A && \defeq \prod_{a_0, a_1 \tp A} \isProp\ (a_0 \equiv a_1) +\end{align*} +\pause +\end{frame} +\begin{frame} +\frametitle{Paths} +\framesubtitle{A few lemmas} +Let $D$ be a type-family: +$$ +D \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} \MCU +$$ +% +\pause +And $d$ and in inhabitant of $D$ at $\refl$: +% +$$ +d \tp D\ a\ \refl +$$ +% +\pause +We then have the function: +% +\begin{equation} +\pathJ\ D\ d \tp \prod_{b \tp A} \prod_{p \tp a ≡ b} D\ a\ p +\end{equation} +\end{frame} +\begin{frame} +\frametitle{Paths} +\framesubtitle{A few lemmas} +Given +\begin{align*} + A & \tp \MCU \\ + P & \tp A \to \MCU \\ + \var{propP} & \tp \prod_{x \tp A} \isProp\ (P\ x) \\ + p & \tp a_0 \equiv a_1 \\ + p_0 & \tp P\ a_0 \\ + p_1 & \tp P\ a_1 +\end{align*} +% +We have +$$ +\lemPropF\ \var{propP}\ p +\tp +\Path\ (\lambda\; i \mto P\ (p\ i))\ p_0\ p_1 +$$ +% +\end{frame} +\begin{frame} +\frametitle{Paths} +\framesubtitle{A few lemmas} +$\prod$ preserves $\isProp$: +$$ +\mathit{propPi} +\tp +\left(\prod_{a \tp A} \isProp\ (P\ a)\right) +\to \isProp\ \left(\prod_{a \tp A} P\ a\right) +$$ +\pause +$\sum$ preserves $\isProp$: +$$ +\mathit{propSig} \tp \isProp\ A \to \left(\prod_{a \tp A} \isProp\ (P\ a)\right) \to \isProp\ \left(\sum_{a \tp A} P\ a\right) +$$ +\end{frame} +\begin{frame} +\frametitle{Categories} +\framesubtitle{Definition} +Data: +\begin{align*} + \Object & \tp \Type \\ + \Arrow & \tp \Object \to \Object \to \Type \\ + \identity & \tp \Arrow\ A\ A \\ + \lll & \tp \Arrow\ B\ C \to \Arrow\ A\ B \to \Arrow\ A\ C +\end{align*} +% +Laws: +% +$$ +h \lll (g \lll f) ≡ (h \lll g) \lll f +$$ +$$ +\identity \lll f ≡ f \x +f \lll \identity ≡ f +$$ +\pause +1-categories: +$$ +\isSet\ (\Arrow\ A\ B) +$$ +\pause +Univalent categories: +$$ +\isEquiv\ (A \equiv B)\ (A \approxeq B)\ \idToIso +$$ +\end{frame} +\begin{frame} +\frametitle{Categories} +\framesubtitle{Univalence} +\begin{align*} +\var{IsIdentity} & \defeq +\prod_{A\ B \tp \Object} \prod_{f \tp \Arrow\ A\ B} \phi\ f +%% \\ +%% & \mathrel{\ } \identity \lll f \equiv f \x f \lll \identity \equiv f +\end{align*} +where +$$ +\phi\ f \defeq \identity \lll f \equiv f \x f \lll \identity \equiv f +$$ +Let $\approxeq$ denote ismorphism of objects. We can then construct +the identity isomorphism in any category: +$$ +\identity , \identity , \var{isIdentity} \tp A \approxeq A +$$ +Likewise since paths are substitutive we can promote a path to an isomorphism: +$$ +\idToIso \tp A ≡ B → A ≊ B +$$ +For a category to be univalent we require this to be an equivalence: +\end{frame} +\end{document} diff --git a/doc/title.tex b/doc/title.tex new file mode 100644 index 0000000..83b90c0 --- /dev/null +++ b/doc/title.tex @@ -0,0 +1,95 @@ +%% FRONTMATTER +\frontmatter +%% \newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm} +\begingroup +\thispagestyle{empty} +{\Huge\thetitle}\\[.5cm] +{\Large A formalization of category theory in Cubical Agda}\\[6cm] +\begin{center} +\includegraphics[width=\linewidth,keepaspectratio]{isomorphism.png} +\end{center} +% Cover text +\vfill +%% \renewcommand{\familydefault}{\sfdefault} \normalfont % Set cover page font +{\Large\theauthor}\\[.5cm] +Master's thesis in Computer Science +\endgroup +%% \end{titlepage} + + +% BACK OF COVER PAGE (BLANK PAGE) +\newpage +%% \newgeometry{a4paper} % Temporarily change margins +%% \restoregeometry +\thispagestyle{empty} +\null + +%% \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 \thetitle} \\[1cm] + {\large \subtitle}\\[1cm] + {\large \theauthor} + + \vfill + \centering + \includegraphics[width=0.2\pdfpagewidth]{logo_eng.pdf} + \vspace{5mm} + + \textsc{Department of Computer Science and Engineering}\\ + \textsc{{\researchgroup}}\\ + %Name of research group (if applicable)\\ + \textsc{\institution} \\ + \textsc{Gothenburg, Sweden \the\year}\\ +\end{center} + + +% IMPRINT PAGE (BACK OF TITLE PAGE) +\newpage +\thispagestyle{plain} +\textit{\thetitle}\\ +\subtitle\\ +\copyright\ \the\year ~ \textsc{\theauthor} +\vspace{4.5cm} + +\setlength{\parskip}{0.5cm} +\textbf{Author:}\\ +\theauthor\\ +\href{mailto:\authoremail>}{\texttt{<\authoremail>}} + +\textbf{Supervisor:}\\ +\supervisor\\ +\href{mailto:\supervisoremail>}{\texttt{<\supervisoremail>}}\\ +\supervisordepartment + +\textbf{Co-supervisor:}\\ +\cosupervisor\\ +\href{mailto:\cosupervisoremail>}{\texttt{<\cosupervisoremail>}}\\ +\cosupervisordepartment + +\textbf{Examiner:}\\ +\examiner\\ +\href{mailto:\examineremail>}{\texttt{<\examineremail>}}\\ +\examinerdepartment + +\vfill +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}\\ +% 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} +%Printed by [Name of printing company]\\ +Gothenburg, Sweden \the\year + +%% \restoregeometry +%% \end{titlepage} + +\tableofcontents