From 7faf0961c56f353c7d3bbab730e4e38c1a4e797d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Tue, 8 May 2018 00:25:34 +0200 Subject: [PATCH] Fix spelling mistakes --- doc/appendix.tex | 37 ++++++++ doc/chalmerstitle.sty | 1 + doc/conclusion.tex | 3 + doc/cubical.tex | 12 +-- doc/discussion.tex | 74 ++++++++++++++++ doc/implementation.tex | 187 +++++++++++++++++++++++------------------ doc/introduction.tex | 15 ++-- doc/main.tex | 5 +- doc/packages.tex | 4 + 9 files changed, 243 insertions(+), 95 deletions(-) create mode 100644 doc/appendix.tex create mode 100644 doc/conclusion.tex create mode 100644 doc/discussion.tex diff --git a/doc/appendix.tex b/doc/appendix.tex new file mode 100644 index 0000000..0c3affb --- /dev/null +++ b/doc/appendix.tex @@ -0,0 +1,37 @@ +\lstset{basicstyle=\footnotesize\ttfamily,breaklines=true,breakpages=true} +\def\fileps + { ../src/Cat.agda + , ../src/Cat/Categories/Cat.agda + , ../src/Cat/Categories/Cube.agda + , ../src/Cat/Categories/CwF.agda + , ../src/Cat/Categories/Fam.agda + , ../src/Cat/Categories/Free.agda + , ../src/Cat/Categories/Fun.agda + , ../src/Cat/Categories/Rel.agda + , ../src/Cat/Categories/Sets.agda + , ../src/Cat/Category.agda + , ../src/Cat/Category/CartesianClosed.agda + , ../src/Cat/Category/Exponential.agda + , ../src/Cat/Category/Functor.agda + , ../src/Cat/Category/Monad.agda + , ../src/Cat/Category/Monad/Kleisli.agda + , ../src/Cat/Category/Monad/Monoidal.agda + , ../src/Cat/Category/Monad/Voevodsky.agda + , ../src/Cat/Category/Monoid.agda + , ../src/Cat/Category/NaturalTransformation.agda + , ../src/Cat/Category/Product.agda + , ../src/Cat/Category/Yoneda.agda + , ../src/Cat/Equivalence.agda + , ../src/Cat/Prelude.agda + } + +\foreach \filep in \fileps { +\chapter{\filep} + %% \begin{figure}[htpb] + \lstinputlisting{\filep} + %% \caption{Source code for \texttt{\filep}} + %% \label{fig:\filep} + %% \end{figure} +} +%% \lstset{framextopmargin=50pt} +%% \lstinputlisting{../../src/Cat.agda} diff --git a/doc/chalmerstitle.sty b/doc/chalmerstitle.sty index 70681d9..631eaa8 100644 --- a/doc/chalmerstitle.sty +++ b/doc/chalmerstitle.sty @@ -40,6 +40,7 @@ \newcommand*{\subtitle}[1]{\gdef\@subtitle{#1}} \newgeometry{top=3cm, bottom=3cm,left=2.25 cm, right=2.25cm} \begingroup +\thispagestyle{empty} \usepackage{noto} \fontseries{sb} %% \fontfamily{noto}\selectfont diff --git a/doc/conclusion.tex b/doc/conclusion.tex new file mode 100644 index 0000000..834e579 --- /dev/null +++ b/doc/conclusion.tex @@ -0,0 +1,3 @@ +\chapter{Conclusion} + +\TODO{\ldots} diff --git a/doc/cubical.tex b/doc/cubical.tex index 9442b65..db3ffbb 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -56,7 +56,7 @@ the real numbers from $0$ to $1$. $P$ is a family of types over the index set $I$. I will sometimes refer to $P$ as the ``path-space'' of some path $p \tp \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 thoery. The intuition +$\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 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-) @@ -155,7 +155,7 @@ there is the notion of sets from set-theory, in Agda types are denoted \texttt{Set}. I will use it consistently to refer to a type $A$ as a set exactly if $\isSet\ A$ is inhabited. -The next step in the hierarchy is, as you might've guessed, the type: +The next step in the hierarchy is, as the reader might've guessed, the type: % \begin{equation} \begin{alignat}{2} @@ -166,7 +166,7 @@ The next step in the hierarchy is, as you might've guessed, the type: % And so it continues. In fact we can generalize this family of types by indexing them with a natural number. For historical reasons, though, the bottom of the -hierarchy, the contractible tyes, is said to be a \nomen{-2-type}, propositions +hierarchy, the contractible types, is said to be a \nomen{-2-type}, propositions are \nomen{-1-types}, (homotopical) sets are \nomen{0-types} and so on\ldots Just as with paths, homotopical sets are not at the center of focus for this @@ -181,12 +181,12 @@ Proposition: For any homotopic level $n$ this is a mere proposition. % \section{A few lemmas} Rather than getting into the nitty-gritty details of Agda I venture to take a -more ``combinators-based'' approach. That is, I will use theorems about paths +more ``combinator-based'' approach. That is, I will use theorems about paths already that have already been formalized. Specifically the results come from the Agda library \texttt{cubical} (\TODO{Cite}). I have used a handful of results from this library as well as contributed a few lemmas myself.\footnote{The module \texttt{Cat.Prelude} lists the upstream dependencies. As well my contribution to \texttt{cubical} can be found in the git logs \TODO{Cite}.} -These theorems are all purely related to homotopy theory and cubical agda and as +These theorems are all purely related to homotopy theory and cubical Agda and as such not specific to the formalization of Category Theory. I will present a few of these theorems here, as they will be used later in chapter \ref{ch:implementation} throughout. @@ -195,7 +195,7 @@ of these theorems here, as they will be used later in chapter \label{sec:pathJ} The induction principle for paths intuitively gives us a way to reason about a type-family indexed by a path by only considering if said path is $\refl$ (the -``base-case''). For \emph{based path induction}, that equaility is \emph{based} +``base-case''). For \emph{based path induction}, that equality is \emph{based} at some element $a \tp A$. Let a type $A \tp \MCU$ and an element of the type $a \tp A$ be given. $a$ is said to be the base of the induction. Given a family of types: diff --git a/doc/discussion.tex b/doc/discussion.tex new file mode 100644 index 0000000..62564e6 --- /dev/null +++ b/doc/discussion.tex @@ -0,0 +1,74 @@ +\chapter{Perspectives} +\section{Discussion} +In the previous chapter the practical aspects of proving things in Cubical Agda +were highlighted. I also demonstrated the usefulness of separating ``laws'' from +``data''. One of the reasons for this is that dependencies within types can lead +to very complicated goals. One technique for alleviating this was to prove that +certain types are mere propositions. + +\subsection{Computational properties} +Another aspect (\TODO{That I actually didn't highlight very well in the previous + chapter}) is the computational nature of paths. Say we have formalized this +common result about monads: + +\TODO{Some equation\ldots} + +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 +Haskell. Whereas the theory usually talks about monoidal monads. + +\TODO{Mention that with postulates we cannot do this} + +\subsection{Reusability of proofs} +The previous example also illustrate how univalence unifies two otherwise +disparate areas: The category-theoretic study of monads; and monads as in +functional programming. Univalence thus allows one to reuse proofs. You could +say that univalence gives the developer two proofs for the price of one. + +The introduction (section \ref{sec:context}) mentioned an often +employed-technique for enabling extensional equalities is to use the +setoid-interpretation. Nowhere in this formalization has this been necessary, +$\Path$ has been used globally in the project as propositional equality. One +interesting place where this becomes apparent is in interfacing with the Agda +standard library. Multiple definitions in the Agda standard library have been +designed with the setoid-interpretation in mind. E.g. the notion of ``unique +existential'' is indexed by a relation that should play the role of +propositional equality. Likewise for equivalence relations, they are indexed, +not only by the actual equivalence relation, but also by another relation that +serve as propositional equality. +%% Unfortunately we cannot use the definition of equivalences found in the +%% standard library to do equational reasoning directly. The reason for this is +%% that the equivalence relation defined there must be a homogenous relation, +%% but paths are heterogeneous relations. + +In the formalization at present a significant amount of energy has been put +towards proving things that would not have been needed in classical Agda. The +proofs that some given type is a proposition were provided as a strategy to +simplify some otherwise very complicated proofs (e.g. +\ref{eq:proof-prop-IsPreCategory} and \label{eq:productPath}). Often these +proofs would not be this complicated. If the J-rule holds definitionally the +proof-assistant can help simplify these goals considerably. The lack of the +J-rule has a significant impact on the complexity of these kinds of proofs. + +\TODO{Universe levels.} + +\section{Future work} +\subsection{Agda \texttt{Prop}} +Jesper Cockx' work extending the universe-level-laws for Agda and the +\texttt{Prop}-type. + +\subsection{Compiling Cubical Agda} +\label{sec:compiling-cubical-agda} +Compilation of program written in Cubical Agda is currently not supported. One +issue here is that the backends does not provide an implementation for the +cubical primitives (such as the path-type). This means that even though the +path-type gives us a computational interpretation of functional extensionality, +univalence, transport, etc., we do not have a way of actually using this to +compile our programs that use these primitives. It would be interesting to see +practical applications of this. The path between monads that this library +exposes could provide one particularly interesting case-study. + +\subsection{Higher inductive types} +This library has not explored the usefulness of higher inductive types in the +context of Category Theory. diff --git a/doc/implementation.tex b/doc/implementation.tex index a73beb7..a5ae42b 100644 --- a/doc/implementation.tex +++ b/doc/implementation.tex @@ -2,37 +2,52 @@ \label{ch:implementation} This implementation formalizes the following concepts: % -\begin{itemize} -\item Core categorical concepts -\subitem Categories -\subitem Functors -\subitem Products -\subitem Exponentials -\subitem Cartesian closed categories -\subitem Natural transformations -\subitem Yoneda embedding -\subitem Monads -\subsubitem Monoidal monads -\subsubitem Kleisli monads -\subsubitem Voevodsky's construction -\item Category of \ldots -\subitem Homotopy sets -\subitem Categories -- only data-part -\subitem Relations -- only data-part -\subitem Functors -- only as a precategory -\subitem Free category -\end{itemize} +\begin{enumerate}[i.] +\item Categories +\item Functors +\item Products +\item Exponentials +\item Cartesian closed categories +\item Natural transformations +\item Yoneda embedding +\item Monads +\item Categories + \begin{enumerate}[i.] + \item Opposite category + \item Category of sets + \item ``Pair category'' + \end{enumerate} +\end{enumerate} % -Since it is useful to distinguish between types with more or less (homotopical) -structure I have followed the following design-principle: I have split concepts -up into things that represent ``data'' and ``laws'' about this data. The idea is -that we can provide a proof that the laws are mere propositions. As an example a -category is defined to have two members: `raw` which is a collection of the data -and `isCategory` which asserts some laws about that data. +Furthermore the following items have been partly formalized: +% +\begin{enumerate}[i.] +\item The (higher) category of categories. +\item Category of relations +\item Category of functors and natural transformations -- only as a precategory +\item Free category +\item Monoidal objects +\item Monoidal categories +\end{enumerate} +% +As well as a range of various results about these. E.g. I have shown that the +category of sets has products. In the following I aim to demonstrate some of the +techniques employed in this formalization and in the interest of brevity I will +not detail all the things I have formalized. In stead, I have selected a parts +of this formalization that highlight some interesting proof techniques relevant +to doing proofs in Cubical Agda. + +One such technique that is pervasive to this formalization is the idea of +distinguishing types with more or less homotopical structure. To do this I have +followed the following design-principle: I have split concepts up into things +that represent ``data'' and ``laws'' about this data. The idea is that we can +provide a proof that the laws are mere propositions. As an example a category is +defined to have two members: `raw` which is a collection of the data and +`isCategory` which asserts some laws about that data. This allows me to reason about things in a more ``standard mathematical way'', where one can reason about two categories by simply focusing on the data. This -is acheived by creating a function embodying the ``equality principle'' for a +is achieved by creating a function embodying the ``equality principle'' for a given type. \section{Categories} @@ -45,7 +60,7 @@ on the topic. We, however, impose one further requirement on what it means to be a category, namely that the type of arrows form a set. Such categories are called \nomen{1-categories}. It's possible to relax this -requirement. This would lead to the notion of higher categorier (\cite[p. +requirement. This would lead to the notion of higher categories (\cite[p. 307]{hott-2013}). For the purpose of this project, however, this report will restrict itself to 1-categories. Making based on higher categories would be a very natural possible extension of this work. @@ -63,7 +78,7 @@ definitions: If we let $p$ be a witness to the identity law, which formally is: \end{equation} % Then we can construct the identity isomorphism $\var{idIso} \tp \identity, -\identity, p \tp A \approxeq A$ for any obejct $A$. Here $\approxeq$ denotes +\identity, p \tp A \approxeq A$ for any object $A$. Here $\approxeq$ denotes isomorphism on objects (whereas $\cong$ denotes isomorphism of types). This will be elaborated further on in sections \ref{sec:equiv} and \ref{sec:univalence}. Moreover, due to substitution for paths we can construct an isomorphism from @@ -121,7 +136,7 @@ f \lll \identity ≑ f \end{align} % $\lll$ denotes arrow composition (right-to-left), and reverse function -composition (left-to-right, diagramatic order) is denoted $\rrr$. The objects +composition (left-to-right, diagrammatic order) is denoted $\rrr$. The objects ($A$, $B$ and $C$) and arrow ($f$, $g$, $h$) are implicitly universally quantified. @@ -160,25 +175,32 @@ us the two obligations: $\isProp\ (\id \comp f \equiv f)$ and $\isProp\ (f \comp set. This example illustrates nicely how we can use these combinators to reason about -`canonical' types like $\sum$ and $\prod$. Similiar combinators can be defined +`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've defined ourselves. For instance, after we've 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. Since pre-categories are -not formulated with a chain of sigma-types we wont have any combinators -available to help us here. In stead we'll have to use the path-type directly. - -What we want to prove is: +that the type of pre-categories is also a proposition. Formally: % \begin{equation} \label{eq:propIsPreCategory} \isProp\ \IsPreCategory \end{equation} % -%% \begin{proof} +Where The definition of $\IsPreCategory$ is the triple: % -This is judgmentally the same as +\begin{align*} +\var{isAssociative} & \tp \var{IsAssociative}\\ +\var{isIdentity} & \tp \var{IsIdentity}\\ +\var{arrowsAreSets} & \tp \var{ArrowsAreSets} +\end{align*} +% +Each corresponding to the first three laws for categories. Note that since +$\IsPreCategory$ is not formulated with a chain of sigma-types we wont have any +combinators available to help us here. In stead we'll have to use the path-type +directly. + +\ref{eq:propIsPreCategory} is judgmentally the same as % $$ \prod_{a\ b \tp \IsPreCategory} a \equiv b @@ -202,12 +224,13 @@ 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 -\equiv b.\isIdentity$ we can elimiate it with $i$ and thus obtain $p\ i \tp +\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 $i$ becomes the triple: % \begin{equation} +\label{eq:proof-prop-IsPreCategory} \begin{aligned} & \var{propIsAssociative} && a.\var{isAssociative}\ && b.\var{isAssociative} && i \\ @@ -224,7 +247,7 @@ It is worth noting that proving this theorem with the regular inductive equality type would already not be possible, since we at least need extensionality (the projections are all $\prod$-types). Assuming we had functional extensionality available to us as an axiom, we would use functional extensionality (in -reverse?) to retreive the equalities in $a$ and $b$, pattern-match on them to +reverse?) to retrieve the equalities in $a$ and $b$, pattern-match on them to see that they are both $\var{refl}$ and then close the proof with $\var{refl}$. Of course this theorem is not so interesting in the setting of ITT since we know a priori that equality proofs are unique. @@ -234,7 +257,7 @@ instance, when we want to show that $\IsCategory$ is a mere proposition. $\IsCategory$ is a record with two fields, a witness to being a pre-category and the univalence condition. Recall that the univalence condition is indexed by the identity-proof. So to follow the same recipe as above, let $a\ b \tp -\IsCategory$ be given, to show them equal, we now need to give two paths. One homogenous: +\IsCategory$ be given, to show them equal, we now need to give two paths. One homogeneous: % $$ p \tp a.\isPreCategory \equiv b.\isPreCategory @@ -249,9 +272,9 @@ $$ Which depends on the choice of $p$. The first of these we can 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. So we need to +latter. This is because $\isProp$ talks about non-dependent paths. So we need to 'promote' the result that univalence is a proposition to a heterogeneous path. -To this end we can use $\lemPropF$, which wasintroduced in \ref{sec:lemPropF}. +To this end we can use $\lemPropF$, which was introduced in \ref{sec:lemPropF}. In this case $A = \var{IsIdentity}\ \identity$ and $B = \var{Univalent}$. We've shown that being a category is a proposition, a result that holds for any choice @@ -267,7 +290,7 @@ And this finishes the proof that being-a-category is a mere proposition (\ref{eq:propIsPreCategory}). When we have a proper category we can make precise the notion of ``identifying -isomorphic types'' \TODO{cite awodey here}. That is, we can construct the +isomorphic types'' \TODO{cite Awodey here}. That is, we can construct the function: % $$ @@ -322,7 +345,7 @@ The maps $\var{fromIso}$ and $\var{toIso}$ naturally extend to these maps: \end{align} % Having this interface gives us both: a way to think rather abstractly about how -to work with equivalences and a way to use ad-hoc definitions of equivalences. +to work with equivalences and a way to use ad hoc definitions of equivalences. The specific instantiation of $\isEquiv$ as defined in \cite{cubical-agda} is: % $$ @@ -394,7 +417,7 @@ 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. -I will now mention a few helpful thoerems that follow from univalence that will +I will now mention a few helpful theorems that follow from univalence that will become useful later. Obviously univalence gives us an isomorphism between $A \equiv B$ and $A @@ -427,7 +450,7 @@ then have the following two theorems: \var{coe}\ p_{\var{cod}}\ f \equiv \iota \lll f \end{align} % -I will give the proof of the first theorem here, the second one is analagous. +I will give the proof of the first theorem here, the second one is analogous. % \begin{align*} \var{coe}\ p_{\var{dom}}\ f @@ -467,11 +490,11 @@ The base-case therefore becomes: & \equiv f \lll \inv{(\var{idToIso}\ \widetilde{\refl})} \end{align*} % -The first step follows because reflixivity is a neutral element for coercions. +The first step follows because reflexivity is a neutral element for coercion. The second step is the identity law in the category. The last step has to do with the fact that $\var{idToIso}$ is constructed by substituting according to the supplied path and since reflexivity is also the neutral element for -substuitutions we arrive at the desired expression. To close the +substitutions we arrive at the desired expression. To close the based-path-induction we must supply the value ``at the other''. In this case this is simply $B \tp \Object$ and $p \tp A \equiv B$ which we have. @@ -552,7 +575,7 @@ follows: && \text{$\var{shuffle}$ is an isomorphism} \\ & \equiv \identity -&& \text{$\isoToId$ is an ismorphism} +&& \text{$\isoToId$ is an isomorphism} \end{align*} % The other direction is analogous. @@ -639,7 +662,7 @@ lemma: \end{align} % Which says that if two type-families are equivalent at all points, then pairs -with identitical first components and these families as second components will +with identical first components and these families as second components will also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq \var{Isomorphism}$. So we must finally prove: % @@ -648,7 +671,7 @@ also be equivalent. For our purposes $P \defeq \isEquiv\ A\ B$ and $Q \defeq \prod_{f \tp A \to B} \left( \isEquiv\ A\ B\ f \simeq \var{Isomorphism}\ f \right) \end{align} -First, lets proove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because +First, lets prove \ref{eq:equivPropSig}: Let $propP \tp \prod_{a \tp A} \isProp (P\ a)$ and $x\;y \tp \sum_{a \tp A} P\ a$ be given. Because of $\var{fromIsomorphism}$ it suffices to give an isomorphism between $x \equiv y$ and $\fst\ x \equiv \fst\ y$: % @@ -674,7 +697,7 @@ the two pairs: \end{align*} % The proof that these are indeed inverses has been omitted. \TODO{Do I really - want to ommit it?}\QED + want to omit it?}\QED Now to prove \ref{eq:equivSig}: Let $e \tp \prod_{a \tp A} \left( P\ a \simeq Q\ a \right)$ be given. To prove the equivalence, it suffices to give an @@ -839,14 +862,13 @@ arrows form a set. For instance, to prove associativity we must prove that (\overline{h} \lll \overline{g}) \lll \overline{f} \end{align} % -Herer $\lll$ refers to the `embellished' composition and $\overline{f}$, +Here $\lll$ refers to the `embellished' composition and $\overline{f}$, $\overline{g}$ and $\overline{h}$ are triples consisting of arrows from the underlying category ($f$, $g$ and $h$) and a pair of witnesses to \ref{eq:pairArrowLaw}. %% Luckily those winesses are paths in the hom-set of the %% underlying category which is a set, so these are mere propositions. -The proof -obligations is: +The proof obligations is consists of two things. The first one is: % \begin{align} \label{eq:productAssocUnderlying} @@ -855,15 +877,18 @@ h \lll (g \lll f) (h \lll g) \lll f \end{align} % -Which is provable by \TODO{What?} and that the witness to \ref{eq:pairArrowLaw} -for the left-hand-side and the right-hand-side are the same. The type of this -goal is quite involved, and I will not write it out in full, but at present it -suffices to show the type of the path-space. Note that the arrows in -\ref{eq:productAssoc} are arrows from $\mathcal{A} = (A , a_{\pairA} , a_{\pairB})$ -to $\mathcal{D} = (D , d_{\pairA} , d_{\pairB})$ where $a_{\pairA}$, $a_{\pairB}$, -$d_{\pairA}$ and $d_{\pairB}$ are arrows in the underlying category. Given that $p$ -is the chosen proof of \ref{eq:productAssocUnderlying} we then have that the -witness to \ref{eq:pairArrowLaw} vary over the type: +And the other proof obligation is that the witness to \ref{eq:pairArrowLaw} for +the left-hand-side and the right-hand-side are the same. + +The proof of the first goal comes directly from the underlying category. The +type of the second goal is very complicated. I will not write it out in full +here, but it suffices to show the type of the path-space. Note that the arrows +in \ref{eq:productAssoc} are arrows from $\mathcal{A} = (A , a_{\pairA} , +a_{\pairB})$ to $\mathcal{D} = (D , d_{\pairA} , d_{\pairB})$ where +$a_{\pairA}$, $a_{\pairB}$, $d_{\pairA}$ and $d_{\pairB}$ are arrows in the +underlying category. Given that $p$ is the chosen proof of +\ref{eq:productAssocUnderlying} we then have that the witness to +\ref{eq:pairArrowLaw} vary over the type: % \begin{align} \label{eq:productPath} @@ -979,7 +1004,7 @@ the implementation for the details). \TODO{Super complicated} \emph{Proposition} \ref{eq:univ-2} is isomorphic to \ref{eq:univ-3}: For this I -will swho two corrolaries of \ref{eq:coeCod}: For an isomorphism $(\iota, +will show two corollaries of \ref{eq:coeCod}: For an isomorphism $(\iota, \inv{\iota}, \var{inv}) \tp A \cong B$, arrows $f \tp \Arrow\ A\ X$, $g \tp \Arrow\ B\ X$ and a heterogeneous path between them, $q \tp \Path\ (\lambda i \to p_{\var{dom}}\ i)\ f\ g$, where $p_{\var{dom}} \tp \Arrow\ A\ X \equiv @@ -995,7 +1020,7 @@ g & \equiv f \lll \inv{\iota} % Proof: \TODO{\ldots} -Now we can prove the equiavalence in the following way: Given $(f, \inv{f}, +Now we can prove the equivalence in the following way: Given $(f, \inv{f}, \var{inv}_f) \tp X \cong Y$ and two heterogeneous paths % \begin{align*} @@ -1025,7 +1050,7 @@ Which, since $f$ is an isomorphism and $p_{\mathcal{A}}$ (resp. $p_{\mathcal{B}} is a path varying according to a path constructed from this isomorphism, this is exactly what \ref{eq:domain-twist-0} gives us. % -The other direction is quite analagous. We choose $\inv{f}$ as the morphism and +The other direction is quite analogous. We choose $\inv{f}$ as the morphism and prove that it satisfies \ref{eq:pairArrowLaw} with \ref{eq:domain-twist-1}. We must now show that this choice of arrows indeed form an isomorphism. Our @@ -1099,7 +1124,7 @@ The proof of the first one is: We have now constructed the maps between \ref{eq:univ-0} and \ref{eq:univ-1}. It remains to show that they are inverses of each other. To cut a long story short, the proof uses the fact that isomorphism-of is propositional and that arrows (in -both categories) are sets. The reader is refered to the implementation for the +both categories) are sets. The reader is referred to the implementation for the gory details. % \subsection{Propositionality of products} @@ -1137,7 +1162,7 @@ conditions will be equal since $f$ is unique. For the other direction we are now given a product $X, x_π’œ, x_ℬ$. Again this will be the terminal object. So now it remains that for any other object there -is aunique arrow from that object into $X, x_π’œ, x_ℬ$. Let $Y, y_π’œ, y_ℬ$ be +is a unique arrow from that object into $X, x_π’œ, x_ℬ$. Let $Y, y_π’œ, y_ℬ$ be another object. As the arrow $\Arrow\ Y\ X$ we choose the product-arrow $y_π’œ \x y_ℬ$. Since this is a product-arrow it satisfies \ref{eq:pairCondRev}. Let us name the witness to this $\phi_{y_π’œ \x y_ℬ}$. So we have picked as our center of @@ -1184,12 +1209,14 @@ That in any category: \end{align} % \section{Monads} -In this section I show two formulations of monads and then show that they are -the same. The two representations are referred to as the monoidal- and kleisli- -representation respectively. +In this section I present two formulations of monads. The two representations +are referred to as the monoidal- and Kleisli- representation respectively or +simply monoidal monads and Kleisli monads for short. We then show that the two +formulations are equivalent, which due to univalence gives us a path between the +two types. -We shall let a category $\bC$ be given. In the remainder all objects and arrows -will implicitly refer to objects and arrows in this category. +Let a category $\bC$ be given. In the remainder of this sections all objects and +arrows will implicitly refer to objects and arrows in this category. % \subsection{Monoidal formulation} The monoidal formulation of monads consists of the following data: @@ -1226,7 +1253,7 @@ they range over are universally quantified. \subsection{Kleisli formulation} % -The kleisli-formulation consists of the following data: +The Kleisli-formulation consists of the following data: % \begin{align} \label{eq:monad-kleisli-data} @@ -1262,18 +1289,18 @@ This data must satisfy: % Here likewise the arrows $f \tp \Arrow\ X\ (\EndoR\ Y)$ and $g \tp \Arrow\ Y\ (\EndoR\ Z)$ are universally quantified (as well as the objects they -range over). $\fish$ is the kleisli-arrow which is defined as $f \fish g \defeq +range over). $\fish$ is the Kleisli-arrow which is defined as $f \fish g \defeq f \rrr (\bind\ g)$ . (\TODO{Better way to typeset $\fish$?}) \subsection{Equivalence of formulations} % -In my implementation I proceede to show how the one formulation gives rise to +In my implementation I proceed to show how the one formulation gives rise to the other and vice-versa. For the present purpose I will briefly sketch some parts of this construction: The notation I have chosen here in the report 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 +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$. @@ -1283,7 +1310,7 @@ In the monoidal formulation we can define $\bind$: \bind \defeq \join \lll \fmap\ f \end{align} % -And likewise in the kleisli formulation we can define $\join$: +And likewise in the Kleisli formulation we can define $\join$: % \begin{align} \join \defeq \bind\ \identity diff --git a/doc/introduction.tex b/doc/introduction.tex index 99761fb..7a5d1a0 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -1,7 +1,7 @@ \chapter{Introduction} Functional extensionality and univalence is not expressible in \nomen{Intensional Martin LΓΆf Type Theory} (ITT). This poses a severe limitation -on both i. what is \emph{provable} and ii. the \emph{reusability} of proofs. +on both i. what is \emph{provable} and ii. the \emph{re-usability} of proofs. Recent developments have, however, resulted in \nomen{Cubical Type Theory} (CTT) which permits a constructive proof of these two important notions. @@ -54,7 +54,7 @@ not true.} There is no way to construct a proof asserting the obvious equivalence of $f$ and $g$ -- even though we can prove them equal for all points. This is exactly the notion of equality of functions that we are interested in; that they are equal for all inputs. We call this -\nomen{pointwise equality}, where the \emph{points} of a function refers +\nomen{point-wise equality}, where the \emph{points} of a function refers to it's arguments. In the context of category theory functional extensionality is e.g. needed to @@ -73,7 +73,7 @@ The proof obligation that this satisfies the identity law of functors \end{align*} % One needs functional extensionality to ``go under'' the function arrow and apply -the (left) identity law of the underlying category to proove $\idFun \comp g +the (left) identity law of the underlying category to prove $\idFun \comp g \equiv g$ and thus close the goal. % \subsection{Equality of isomorphic types} @@ -81,7 +81,7 @@ the (left) identity law of the underlying category to proove $\idFun \comp g Let $\top$ denote the unit type -- a type with a single constructor. In the propositions-as-types interpretation of type theory $\top$ is the proposition that is always true. The type $A \x \top$ and $A$ has an element for each $a : -A$. So in a sense they have the same shape (greek; \nomen{isomorphic}). The +A$. So in a sense they have the same shape (Greek; \nomen{isomorphic}). The second element of the pair does not add any ``interesting information''. It can be useful to identify such types. In fact, it is quite commonplace in mathematics. Say we look at a set $\{x \mid \phi\ x \land \psi\ x\}$ and somehow @@ -114,6 +114,7 @@ formulate this requirement within our formulation of categories by requiring the \emph{categories} themselves to be univalent as we shall see. \section{Context} +\label{sec:context} % The idea of formalizing Category Theory in proof assistants is not new. There are a multitude of these available online. Just as a first reference see this @@ -131,7 +132,7 @@ implementations of category theory in Agda: A formalization in Agda with univalence and functional extensionality as postulates. \item - \url{https://github.com/pcapriotti/agda-categories} + \url{https://github.com/HoTT/HoTT/tree/master/theories/Categories} A formalization in Coq in the homotopic setting \item @@ -160,11 +161,11 @@ canonical form. Another approach is to use the \emph{setoid interpretation} of type theory (\cite{hofmann-1995,huber-2016}). With this approach one works with -\nomen{extensionals sets} $(X, \sim)$, that is a type $X \tp \MCU$ and an +\nomen{extensional sets} $(X, \sim)$, that is a type $X \tp \MCU$ and an equivalence relation $\sim \tp X \to X \to \MCU$ on that type. Under the setoid interpretation the equivalence relation serve as a sort of ``local'' propositional equality. This approach has other drawbacks; it does not satisfy -all propositional equalites of type theory (\TODO{Citation needed}), is +all propositional equalities of type theory (\TODO{Citation needed}), is cumbersome to work with in practice (\cite[p. 4]{huber-2016}) and makes equational proofs less reusable since equational proofs $a \sim_{X} b$ are inherently `local' to the extensional set $(X , \sim)$. diff --git a/doc/main.tex b/doc/main.tex index a894748..bdf4b49 100644 --- a/doc/main.tex +++ b/doc/main.tex @@ -43,7 +43,6 @@ \researchgroup{Programming Logic Group} \bibliographystyle{plain} -\addtocontents{toc}{\protect\thispagestyle{empty}} %% \newtheorem{prop}{Proposition} \makeatletter \newcommand*{\rom}[1]{\expandafter\@slowroman\romannumeral #1@} @@ -52,13 +51,15 @@ \pagenumbering{roman} \maketitle - +\addtocontents{toc}{\protect\thispagestyle{empty}} \tableofcontents \pagenumbering{arabic} % \input{introduction.tex} \input{cubical.tex} \input{implementation.tex} +\input{discussion.tex} +\input{conclusion.tex} \nocite{cubical-demo} \nocite{coquand-2013} diff --git a/doc/packages.tex b/doc/packages.tex index f786c61..120699d 100644 --- a/doc/packages.tex +++ b/doc/packages.tex @@ -36,6 +36,8 @@ \usepackage{lmodern} +\usepackage{enumerate} + \usepackage{fontspec} \usepackage[light]{sourcecodepro} %% \setmonofont{Latin Modern Mono} @@ -52,3 +54,5 @@ \usepackage{unicode-math} %% \RequirePackage{kvoptions} + +\usepackage{pgffor}