From 98b71ac2679653a1782319487e52bb570e692498 Mon Sep 17 00:00:00 2001 From: Masahiro Kitagawa Date: Tue, 31 Jan 2023 00:34:37 +0900 Subject: [PATCH] Fix minor typos (#304) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * typo (date -> data) * Replace double colon with LaTeX \Colon * typo (\eta_aa -> \eta_a) * Replace \emph{} with \cat{} * Add missing colon * typo (× -> \times) * typo (C -> $\cat{C}$) * fixup! 38f8fe8e41038b2fab7fa068a78cff4fd2676e7438f8fe8e41038b2fab7fa068a78cff4fd2676e74 --- src/content/1.9/function-types.tex | 4 ++-- src/content/3.10/ends-and-coends.tex | 2 +- src/content/3.14/lawvere-theories.tex | 10 +++++----- src/content/3.7/comonads.tex | 2 +- src/content/3.9/algebras-for-monads.tex | 14 +++++++------- 5 files changed, 16 insertions(+), 16 deletions(-) diff --git a/src/content/1.9/function-types.tex b/src/content/1.9/function-types.tex index 334bedeb..ba598fa4 100644 --- a/src/content/1.9/function-types.tex +++ b/src/content/1.9/function-types.tex @@ -320,7 +320,7 @@ \section{Exponentials} specified by a pair of values: one corresponding to \code{False}, and one corresponding to \code{True}. The set of all possible functions from \code{Bool} to, say, \code{Int} is the set of all pairs of -\code{Int}s. This is the same as the product \code{Int} × \code{Int} or, +\code{Int}s. This is the same as the product \code{Int} \times \code{Int} or, being a little creative with notation, \code{Int}\textsuperscript{2}. For another example, let's look at the C++ type \code{char}, which @@ -330,7 +330,7 @@ \section{Exponentials} Functions like \code{isupper} or \code{isspace} are implemented using tables, which are equivalent to tuples of 256 Boolean values. A tuple is a product type, so we are dealing with products of 256 -Booleans: \code{bool × bool × bool × ... × bool}. We know from +Booleans: \code{bool \times bool \times bool \times ... \times bool}. We know from arithmetics that an iterated product defines a power. If you ``multiply'' \code{bool} by itself 256 (or \code{char}) times, you get \code{bool} to the power of \code{char}, or \code{bool}\textsuperscript{\code{char}}. diff --git a/src/content/3.10/ends-and-coends.tex b/src/content/3.10/ends-and-coends.tex index 4730c9a9..7b7a2f41 100644 --- a/src/content/3.10/ends-and-coends.tex +++ b/src/content/3.10/ends-and-coends.tex @@ -15,7 +15,7 @@ \[\cat{C}(-, =) \Colon \cat{C}^{op}\times{}\cat{C} \to \Set\] In general, any functor like this may be interpreted as establishing a relation between objects in a category. A relation may also involve two -different categories \emph{C} and \emph{D}. A functor, which describes +different categories $\cat{C}$ and $\cat{D}$. A functor, which describes such a relation, has the following signature and is called a profunctor: \[p \Colon \cat{D}^{op}\times{}\cat{C} \to \Set\] Mathematicians say that it's a profunctor from $\cat{C}$ to $\cat{D}$ diff --git a/src/content/3.14/lawvere-theories.tex b/src/content/3.14/lawvere-theories.tex index cfa9924d..4e8f0ed9 100644 --- a/src/content/3.14/lawvere-theories.tex +++ b/src/content/3.14/lawvere-theories.tex @@ -112,8 +112,8 @@ \section{Lawvere Theories} identified through isomorphisms. Using the category $\cat{F}$ we can formally define a \newterm{Lawvere -theory} as a category $\cat{L}$ equipped with a special functor -\[I_{\cat{L}} :: \Fop \to \cat{L}\] +theory} as a category $\cat{L}$ equipped with a special functor: +\[I_{\cat{L}} \Colon \Fop \to \cat{L}\] This functor must be a bijection on objects and it must preserve finite products (products in $\Fop$ are the same as coproducts in $\cat{F}$): @@ -496,7 +496,7 @@ \section{Monads as Coends} \begin{tikzcd} & a^n \times \cat{L}(m, 1) \arrow[dl, "\langle f {,} \id \rangle"'] - \arrow[dr, "\langle \id {,} f \rangle"] + \arrow[dr, "\langle \id {,} f \rangle"] & \\ a^m \times \cat{L}(m, 1) & \scalebox{2.5}[1]{\sim} @@ -518,7 +518,7 @@ \section{Monads as Coends} \[a^n \times \cat{L}(n, 1)\] when we lift $\langle \id, f \rangle$. This doesn't mean, however, that all elements of $a^n \times \cat{L}(n, 1)$ can be -identified with $a × \cat{L}(1, 1)$. That's because not all elements +identified with $a \times \cat{L}(1, 1)$. That's because not all elements of $\cat{L}(n, 1)$ can be reached from $\cat{L}(1, 1)$. Remember that we can only lift morphisms from $\cat{F}$. A non-trivial $n$-ary operation in $\cat{L}$ cannot be constructed by lifting a morphism @@ -579,7 +579,7 @@ \section{Lawvere Theory of Side Effects} \begin{tikzcd} & a^n \times \cat{L}(0, 1) \arrow[dl, "\langle f {,} \id \rangle"'] - \arrow[dr, "\langle \id {,} f \rangle"] + \arrow[dr, "\langle \id {,} f \rangle"] & \\ a^0 \times \cat{L}(0, 1) & \scalebox{2.5}[1]{\sim} diff --git a/src/content/3.7/comonads.tex b/src/content/3.7/comonads.tex index 25013fdd..67879dfb 100644 --- a/src/content/3.7/comonads.tex +++ b/src/content/3.7/comonads.tex @@ -377,7 +377,7 @@ \section{The Store Comonad} The \code{Store} comonad plays an important role as the theoretical basis for the \code{Lens} library. Conceptually, the \code{Store s a} comonad encapsulates the idea of ``focusing'' (like -a lens) on a particular substructure of the date type \code{a} using +a lens) on a particular substructure of the data type \code{a} using the type \code{s} as an index. In particular, a function of the type: \src{snippet38} diff --git a/src/content/3.9/algebras-for-monads.tex b/src/content/3.9/algebras-for-monads.tex index bcba2528..070280bd 100644 --- a/src/content/3.9/algebras-for-monads.tex +++ b/src/content/3.9/algebras-for-monads.tex @@ -29,7 +29,7 @@ object --- the carrier $a$ --- together with the morphism: \[alg \Colon m\ a \to a\] The first thing to notice is that the algebra goes in the opposite -direction to $\eta_aa$. The intuition is that $\eta_a$ creates a +direction to $\eta_a$. The intuition is that $\eta_a$ creates a trivial expression from a value of type $a$. The first coherence condition that makes the algebra compatible with the monad ensures that evaluating this expression using the algebra whose carrier is $a$ @@ -52,7 +52,7 @@ \begin{subfigure} \centering \begin{tikzcd}[column sep=large, row sep=large] - a \arrow[rd, equal] \arrow[r, "\eta_a"] + a \arrow[rd, equal] \arrow[r, "\eta_a"] & Ta \arrow[d, "alg"] \\ & a \end{tikzcd} @@ -196,7 +196,7 @@ \section{T-algebras} \begin{subfigure} \centering \begin{tikzcd}[column sep=large, row sep=large] - Ta \arrow[rd, equal] \arrow[r, "T \eta_a"] + Ta \arrow[rd, equal] \arrow[r, "T \eta_a"] & T(Ta) \arrow[d, "\mu_a"] \\ & Ta \end{tikzcd} @@ -205,7 +205,7 @@ \section{T-algebras} \begin{subfigure} \centering \begin{tikzcd}[column sep=large, row sep=large] - a \arrow[rd, equal] \arrow[r, "\eta_a"] + a \arrow[rd, equal] \arrow[r, "\eta_a"] & Ta \arrow[d, "f"] \\ & a \end{tikzcd} @@ -220,7 +220,7 @@ \section{T-algebras} \[F^T \dashv U^T\] Every adjunction gives rise to a monad. The round trip \[U^T \circ F^T\] -is the endofunctor in C that gives rise to the corresponding monad. +is the endofunctor in $\cat{C}$ that gives rise to the corresponding monad. Let's see what its action on an object $a$ is. The free algebra created by $F^T$ is $(T\ a, \mu_a)$. The forgetful functor $U^T$ drops the evaluator. So, indeed, we have: @@ -292,7 +292,7 @@ \section{The Kleisli Category} \src{snippet06} We can also define a functor $G$ from $\cat{C}_T$ back to $\cat{C}$. It takes an object $a$ from the Kleisli -category and maps it to an object $T\ a$ in $\cat{C}$. Its action +category and maps it to an object $T\ a$ in $\cat{C}$. Its action on a morphism $f_{\cat{K}}$ corresponding to a Kleisli arrow: \[f \Colon a \to T\ b\] is a morphism in $\cat{C}$: @@ -329,7 +329,7 @@ \section{Coalgebras for Comonads} \begin{subfigure} \centering \begin{tikzcd}[column sep=large, row sep=large] - a \arrow[rd, equal] + a \arrow[rd, equal] & Wa \arrow[l, "\epsilon_a"'] \\ & a \arrow[u, "coa"'] \end{tikzcd}