Revise everything (2)

acknowledgements.tex

@@ -1,6 +1,8 @@
 \chapter{Acknowledgements}
 \label{chap:acknowledgements}
 
+Pending.
+
 %% I'm very grateful to my supervisor, Andrés Sicard-Ramírez, especially
 %% for introducing me to category theory and functional programming, to
 %% my parents, Ana María Isaza Builes and Carlos Fernando Villa Gómez,

algebras.tex

@@ -695,7 +695,7 @@ \section{Algebras and Initial Algebras in Haskell}
   In this case, explicit recursion yields the following definition:
   \begin{codehaskell}
 mult Zero     n = Zero
-mult (Succ m) n = add n (mul m n)
+mult (Succ m) n = add n (mult m n)
   \end{codehaskell}
 
 \end{example}
@@ -796,10 +796,10 @@ \section{Algebras and Initial Algebras in Haskell}
 length (Cons _ xs) = Succ (length xs)
 
 append Nil         ys = ys
-append (Cons x xs) ys = Cons x (concat xs ys)
+append (Cons x xs) ys = Cons x (append xs ys)
 
 map _ Nil         = Nil
-map f (Cons x xs) = Cons (f x) (fmap f xs)
+map f (Cons x xs) = Cons (f x) (map f xs)
   \end{codehaskell}
 
 \end{example}

categories.tex

@@ -18,13 +18,13 @@ \chapter{Categories}
 \ref{fig:category-haskell}, excluding composite functions. More
 specifically, as types, take the unit type, \texthaskell{()}, the
 Boolean type, \texthaskell{Bool}, and the natural number type,
-\texthaskell{Nat}\footnote{Note that Haskell does not have a natural
-  number data type by itself.}, and, as functions, take the
-constants-as-functions \texthaskell{()}, \texthaskell{True},
-\texthaskell{False}, and \texthaskell{Zero}, the functions
-\texthaskell{Succ}, \texthaskell{isZero}, and \texthaskell{not}, the
-identity functions, \texthaskell{id}, and composite functions such as
-\texthaskell{not . True}.
+\texthaskell{Nat}\footnote{Note that, at least in GHC 7.6.3, Haskell
+  does not have a natural number data type by itself.}, and, as
+functions, take the constants-as-functions \texthaskell{()},
+\texthaskell{True}, \texthaskell{False}, and \texthaskell{Zero}, the
+functions \texthaskell{Succ}, \texthaskell{isZero}, and
+\texthaskell{not}, the identity functions, \texthaskell{id}, and
+composite functions such as \texthaskell{not . True}.
 
 \begin{figure}[htb]
   \begin{center}

conclusions.tex

@@ -72,26 +72,27 @@ \subsection{Adjoints}
 \label{sec:future-adjoints}
 
 Category theory is based on the concepts of categories, functors, and
-natural transformations. While important, the fundamental notion of
-category theory is adjoints \parencite[11]{marquis-2013}, which
-``arise everywhere'' \parencite[vii]{maclane-1998}. Taking into
-account our approach, can we study the applications of adjoints with
-the purpose of better understanding functional programming? Based on
-\parencites[§ 13]{barr-wells-2012}[79--81]{elkins-2009}[§
-  2.4]{pierce-1991}{rydeheard-1986-adjunctions}[§
+natural transformations. Even though these ideas are important, a
+fundamental notion of category theory is adjoints
+\parencite[11]{marquis-2013}, which ``arise everywhere''
+\parencite[vii]{maclane-1998}. Taking into account our approach, can
+we study the applications of adjoints with the purpose of better
+understanding functional programming? Based on \parencites[§
+  13]{barr-wells-2012}[79--81]{elkins-2009}[§~2.4]{pierce-1991}{rydeheard-1986-adjunctions}[§
   6]{rydeheard-burstall-1988}, the answer seems to be yes. In
-addition, \textcite[§ 9]{awodey-2010} and \textcite[§
-  IV]{maclane-1998} seem to offer a good starting point.
+addition, \textcite[§ 9]{awodey-2010} and
+\textcite[§~IV]{maclane-1998} seem to offer a good starting point.
 
 \subsection{Applicative functors}
 \label{sec:future-monoidals}
 
 Based on \parencite{mcbride-paterson-2008}, we identified and studied
 monoidal categories and functors in order to be able to understand
-applicative functors from a category-theoretical point of view, but we
-did not include our results here. This seems to be a very relevant
-next step, particularly in the context of the ``current, and very
-likely to succeed,'' Haskell 2014 \texthaskell{Applicative => Monad}
+applicative functors from a category-theoretical point of view. We
+could use our results in a future project, which seems to be a very
+relevant next step, particularly in the context of the ``current, and
+very likely to succeed,'' Haskell 2014 \texthaskell{Applicative =>
+  Monad}
 proposal\footnote{\url{http://www.haskell.org/haskellwiki/Functor-Applicative-Monad_Proposal}.},
 which adds an \texthaskell{Applicative} constraint to the
 \texthaskell{Monad} type class and promotes \texthaskell{join} to
@@ -103,7 +104,7 @@ \subsection{Categories}
 
 In Section \ref{sec:category-haskell}, we described \hask, the
 category of Haskell types and functions, in order to be able to relate
-category theory to functional programming. We could have used the
+category theory to functional programming. We could use the
 \texthaskell{Category} type class instead
 \parencites[49--51]{yorgey-2009}[74--75]{elkins-2009}:
 \begin{codehaskell}
@@ -115,7 +116,7 @@ \subsection{Categories}
   id  = Prelude.id
   (.) = (Prelude..)
 \end{codehaskell}
-Likewise, we could have studied Kleisli categories
+Likewise, we could study Kleisli categories
 \parencite[59--60]{moggi-1991} in terms of this type class, which
 might be a more intuitive way to justify the Kleisli triple laws. In
 addition, the \texthaskell{Category} class would lead us to
@@ -136,8 +137,8 @@ \subsection{Folds}
 \subsection{Monoids}
 \label{sec:future-monoids}
 
-As an alternative to the ideas of Section \ref{sec:future-adjoints},
-``the fundamental notion of category theory is that of a monoid''
+As an alternative to the ideas of Section \ref{sec:future-adjoints}, a
+``fundamental notion of category theory is that of a monoid''
 \parencite[vii]{maclane-1998}, as described in Example
 \ref{ex:category-monoid}. In Haskell, monoids are defined by the
 \texthaskell{Monoid} type class:

introduction.tex

@@ -67,7 +67,7 @@ \section{Audience and Prerequisites}
 programmer. We assume a working knowledge of mathematics and
 functional programming in Haskell and Agda. If any further background
 material is required, some suggestions can be found in the references
-on page \pageref{sec:introduction-references} or in the references at
+in Section \ref{sec:introduction-references} or in the references at
 the end of each chapter.
 
 \section{Overview of the Project}
@@ -273,9 +273,10 @@ \section{Notes}
 
 \item
   The Agda code was tested with Agda 2.3.2.2 and the Agda standard
-  library 0.7. We omit a lot of details such as import declarations,
-  but all the code can be found in a Git repository which is available
-  at \url{https://github.com/jpvillaisaza/abel}.
+  library 0.7 \parencite{danielsson-2013}. We omit a lot of details
+  such as import declarations, but all the code can be found in a Git
+  repository which is available at
+  \url{https://github.com/jpvillaisaza/abel}.
 
 \end{itemize}