Revise everything

abstract.tex

@@ -2,20 +2,22 @@ \chapter{Abstract}
 \label{chap:abstract}
 
 We study some of the applications of category theory to functional
-programming in Haskell and Agda. More specifically, we describe and
-explain the concepts of category theory needed for conceptualizing and
-better understanding algebraic data types and folds, functors, monads,
-and parametrically polymorphic functions. With this purpose, we give a
-detailed account of categories, functors and endofunctors, natural
-transformations, monads and Kleisli triples, algebras and initial
-algebras over endofunctors, among others. In addition, we explore all
-of these concepts from the standpoints of categories and programming
-in Haskell, and, in some cases, Agda. In other words, we examine
-functional programming through category theory.
+programming, particularly in the context of the Haskell functional
+programming language, and the Agda dependently typed functional
+programming language and proof assistant. More specifically, we
+describe and explain the concepts of category theory needed for
+conceptualizing and better understanding algebraic data types and
+folds, functors, monads, and parametrically polymorphic functions.
+With this purpose, we give a detailed account of categories, functors
+and endofunctors, natural transformations, monads and Kleisli triples,
+algebras and initial algebras over endofunctors, among others. In
+addition, we explore all of these concepts from the standpoints of
+categories and programming in Haskell, and, in some cases, Agda. In
+other words, we examine functional programming through category
+theory.
 
 \vspace{1em}
 \noindent
-Keywords: Agda, category, category theory, functional programming,
-functor, Haskell.
+Keywords: Agda, category theory, functional programming, Haskell.
 
 \clearemptydoublepage

algebras.tex

@@ -558,7 +558,11 @@ \section{Algebras and Initial Algebras}
   $\func{L}^{A}$-\alg. Let $(B,[n,c])$ be an algebra over
   $\func{L}^{A}$, that is, a set $A$ and functions $n: 1 \to B$ and
   $c: A \times B \to B$. Then we need a unique $\func{L}^{A}$-algebra
-  homomorphism $\fold(n,c): (\listof{A},[\nil,\cons]) \to (B,[n,c])$,
+  homomorphism
+  \begin{equation*}
+    \fold(n,c): (\listof{A},[\nil,\cons]) \to (B,[n,c])
+    \text{,}
+  \end{equation*}
   that is, a function $\foldr(n,c): \listof{A} \to B$ such that
   \begin{equation*}
     \foldr(n,c) \comp [\nil,\cons] = [n,c] \comp \funcM{L}^{A}(\foldr(n,c))

categories.tex

@@ -19,7 +19,7 @@ \chapter{Categories}
 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 type by itself.}, and, as functions, take the
+  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
@@ -693,7 +693,8 @@ \section{A Category for Agda}
 type \textagda{Set₂}, and so on. The first universe, \textagda{Set₀}
 or \textagda{Set}, which is called the universe of small types, and
 the second universe, \textagda{Set₁}, will be the only universes
-necessary for our development \parencite[§ 2.1]{sicardramirez-2014}.
+necessary for our development \parencites[57,
+  61]{bove-dybjer-2009}[231]{norell-2009}.
 
 Let us now construct a category analogous to \hask, the category of
 Haskell types and functions, in Agda. The objects of this category are

introduction.tex

@@ -16,9 +16,9 @@ \chapter{Introduction}
 \parencites[vii]{maclane-1998}[1]{marquis-2013}[1154]{wolfram-2002}.
 
 In computer science, category theory allows us to formulate
-definitions and theories of concepts, or to analyze the elegance and
-coherence of existing formulations, to carry out proofs, to discover
-and exploit relations with other fields, to deal with abstraction and
+definitions and theories of concepts, or to analyze the coherence of
+existing formulations, to carry out proofs, to discover and exploit
+relations with other fields, to deal with abstraction and
 representation independence, to formulate conjectures and research
 directions, and to unify concepts \parencites[49--50]{goguen-1991}.
 Moreover, category theory contributes to areas such as automata
@@ -34,13 +34,13 @@ \chapter{Introduction}
 \textcite[50--51]{yorgey-2009}, several concepts of functional
 programming languages, such as Agda \parencites{norell-2007}{agda},
 Haskell \parencite{peytonjones-2003}, Miranda \parencite{turner-1985},
-and ML \parencite{milner-1984}, are based on concepts of category
-theory, but one can be a perfectly competent functional programmer
-without knowledge of these theoretical foundations. In spite of that,
-category theory can be applied to functional programming with the
-purpose of, for instance, better understanding concepts such as
-algebraic data types, applicative functors, functors, monads, and
-polymorphism, and thus becoming a better programmer.
+ML \parencite{milner-1984}, among others, are based on concepts of
+category theory, but one can be a perfectly competent functional
+programmer without knowledge of these theoretical foundations. In
+spite of that, category theory can be applied to functional
+programming with the purpose of, for instance, better understanding
+concepts such as algebraic data types, applicative functors, functors,
+monads, and polymorphism, and thus becoming a better programmer.
 
 In this regard, we aim to explore the category-theoretical foundations
 of some of the concepts of functional programming listed above. In

main.tex

@@ -13,10 +13,10 @@
 \include{acknowledgements}
 \include{epigraph}
 
-\input{contents}
-
 \include{abstract}
 
+\input{contents}
+
 \mainmatter
 
 \include{introduction}

monads.tex

@@ -49,8 +49,8 @@ \chapter{Monads and Kleisli Triples}
 In the remainder of this chapter, we define the concepts of monad and
 Kleisli triple, prove their equivalence, and study both constructs in
 Haskell and Agda. We should note that, terminologically,
-category-theoretical monads and monads in functional programming,
-which actually correspond to Kleisli triples, are not the same thing.
+category-theoretical monads and monads in Haskell, which actually
+correspond to Kleisli triples, are not the same thing.
 
 \section{Monads and Kleisli Triples}
 \label{sec:monads}
@@ -678,10 +678,10 @@ \section{Monads and Kleisli Triples in Haskell}
 monoid form), Kleisli triples (monads in extension form), and monads
 in clone form. Kleisli triples are easier to justify from a
 computational point of view and correspond to the representation that
-is found in functional programming languages like Haskell and Agda. On
-the other hand, monads have some mathematical advantages and are more
-intuitive in some cases. In this section, we describe both
-representations in Haskell.
+is found in functional programming languages like Haskell and the Agda
+standard library. On the other hand, monads have some mathematical
+advantages and are more intuitive in some cases. In this section, we
+describe both representations in Haskell.
 
 \subsection{Monads in Haskell}
 
@@ -1150,8 +1150,8 @@ \subsection{Kleisli Triples in Haskell}
   \parencites[273]{lipovaca-2011}[88]{peytonjones-2003}[30]{yorgey-2009}.
   Besides, the \texthaskell{error} function is closely related to
   \texthaskell{undefined}\footnote{See \parencite[§
-      3.1]{peytonjones-2003}.}, which we discussed in Convention
-  \ref{con:hask}.
+      3.1]{peytonjones-2003}.}, which we discussed in
+  Convention~\ref{con:hask}.
 
 \end{remark}
 

preamble.tex

@@ -189,11 +189,10 @@
 \theoremstyle{definition}
 
 \newtheorem{definition}{Definition}[chapter]
-
 \newtheorem{example}{Example}[section]
-\newtheorem{examples}[example]{Examples}
 
-\newtheorem*{example*}{Example}
+\newtheorem{convention}{Convention}
+\newtheorem{remark}{Remark}[chapter]
 
 \theoremstyle{plain}
 
@@ -203,12 +202,6 @@
 
 \theoremstyle{remark}
 
-\newtheorem{convention}{Convention}
-\newtheorem{notation}{Notation}[chapter]
-\newtheorem{note}{Note}
-\newtheorem{remark}{Remark}[chapter]
-
-\newtheorem*{remark*}{Remark}
 \newtheorem*{terminology}{Terminology}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

title.tex

@@ -15,7 +15,7 @@
     \vspace*{\fill}
 
     {\large Supervisor:}
-    {\large Andrés Sicard-Ramírez}
+    {\large Andrés Sicard Ramírez}
 
     \vspace*{\fill}