diff --git a/src/content/1.2/Types and Functions.tex b/src/content/1.2/Types and Functions.tex index 0f5337f8..977a3a78 100644 --- a/src/content/1.2/Types and Functions.tex +++ b/src/content/1.2/Types and Functions.tex @@ -120,11 +120,11 @@ \section{What Are Types?}\label{what-are-types} sets tricky. There are problems with polymorphic functions that involve circular definitions, and with the fact that you can't have a set of all sets; but as I promised, I won't be a stickler for math. The great thing -is that there is a category of sets, which is called \textbf{Set}, and -we'll just work with it. In \textbf{Set}, objects are sets and morphisms +is that there is a category of sets, which is called $\Set$, and +we'll just work with it. In $\Set$, objects are sets and morphisms (arrows) are functions. -\textbf{Set} is a very special category, because we can actually peek +$\Set$ is a very special category, because we can actually peek inside its objects and get a lot of intuitions from doing that. For instance, we know that an empty set has no elements. We know that there are special one-element sets. We know that functions map elements of one @@ -180,12 +180,12 @@ \section{What Are Types?}\label{what-are-types} functions, which return valid results for every possible argument. Because of the bottom, you'll see the category of Haskell types and -functions referred to as \textbf{Hask} rather than \textbf{Set}. From +functions referred to as \textbf{Hask} rather than $\Set$. From the theoretical point of view, this is the source of never-ending complications, so at this point I will use my butcher's knife and terminate this line of reasoning. From the pragmatic point of view, it's okay to ignore non-terminating functions and bottoms, and treat -\textbf{Hask} as bona fide \textbf{Set}.\footnote{Nils Anders Danielsson, +\textbf{Hask} as bona fide $\Set$.\footnote{Nils Anders Danielsson, John Hughes, Patrik Jansson, Jeremy Gibbons, \href{http://www.cs.ox.ac.uk/jeremy.gibbons/publications/fast+loose.pdf}{ Fast and Loose Reasoning is Morally Correct}. This paper provides justification for ignoring bottoms in most contexts.} diff --git a/src/content/1.3/Categories Great and Small.tex b/src/content/1.3/Categories Great and Small.tex index 37448b36..6f214239 100644 --- a/src/content/1.3/Categories Great and Small.tex +++ b/src/content/1.3/Categories Great and Small.tex @@ -170,7 +170,7 @@ \section{Monoid as Set}\label{monoid-as-set} mappend s1 s2 = (++) s1 s2 \end{Verbatim} The former translates into equality of morphisms in the category -\textbf{Hask} (or \textbf{Set}, if we ignore bottoms, which is the name +\textbf{Hask} (or $\Set$, if we ignore bottoms, which is the name for never-ending calculations). Such equations are not only more succinct, but can often be generalized to other categories. The latter is called \newterm{extensional} equality, and states the fact that for any diff --git a/src/content/1.5/Products and Coproducts.tex b/src/content/1.5/Products and Coproducts.tex index a0998a98..c5d91318 100644 --- a/src/content/1.5/Products and Coproducts.tex +++ b/src/content/1.5/Products and Coproducts.tex @@ -639,7 +639,7 @@ \section{Asymmetry}\label{asymmetry} from the terminal end. This is not an intrinsic property of sets, it's a property of functions, -which we use as morphisms in \textbf{Set}. Functions are, in general, +which we use as morphisms in $\Set$. Functions are, in general, asymmetric. Let me explain. A function must be defined for every element of its domain set (in diff --git a/src/content/1.8/Functoriality.tex b/src/content/1.8/Functoriality.tex index b7e1c077..df3c0924 100644 --- a/src/content/1.8/Functoriality.tex +++ b/src/content/1.8/Functoriality.tex @@ -611,7 +611,7 @@ \section{Profunctors}\label{profunctors} We've seen that the function-arrow operator is contravariant in its first argument and covariant in the second. Is there a name for such a -beast? It turns out that, if the target category is \textbf{Set}, such a +beast? It turns out that, if the target category is $\Set$, such a beast is called a \newterm{profunctor}. Because a contravariant functor is equivalent to a covariant functor from the opposite category, a profunctor is defined as:\\ diff --git a/src/content/1.9/Function Types.tex b/src/content/1.9/Function Types.tex index 2d050258..3f110417 100644 --- a/src/content/1.9/Function Types.tex +++ b/src/content/1.9/Function Types.tex @@ -12,7 +12,7 @@ \code{a->b} is more than that: it's a set of morphisms between objects \code{a} and \code{b}. A set of morphisms between two objects in any category is called a hom-set. It just so happens that -in the category \textbf{Set} every hom-set is itself an object in the +in the category $\Set$ every hom-set is itself an object in the same category ---because it is, after all, a \newterm{set}. The same is not true of other categories where hom-sets are external to @@ -26,7 +26,7 @@ \end{wrapfigure} \noindent -It's the self-referential nature of the category \textbf{Set} that makes +It's the self-referential nature of the category $\Set$ that makes function types special. But there is a way, at least in some categories, to construct objects that represent hom-sets. Such objects are called \newterm{internal} hom-sets. @@ -35,7 +35,7 @@ \section{Universal Construction}\label{universal-construction} Let's forget for a moment that function types are sets and try to construct a function type, or more generally, an internal hom-set, from -scratch. As usual, we'll take our cues from the \textbf{Set} category, +scratch. As usual, we'll take our cues from the $\Set$ category, but carefully avoid using any properties of sets, so that the construction will automatically work for other categories. @@ -52,7 +52,7 @@ \section{Universal Construction}\label{universal-construction} The obvious pattern that connects these three types is called \newterm{function application} or \newterm{evaluation}. Given a candidate for a function type, let's call it \code{z} (notice that, if we are not in -the category \textbf{Set}, this is just an object like any other +the category $\Set$, this is just an object like any other object), and the argument type \code{a} (an object), the application maps this pair to the result type \code{b} (an object). We have three objects, two of them fixed (the ones representing the argument type and @@ -77,7 +77,7 @@ \section{Universal Construction}\label{universal-construction} well talk about the whole \newterm{product} of the function type \code{z} and the argument type \code{a}. The product \code{z×a} is an object, and we can pick, as our application morphism, an arrow \code{g} from -that object to \code{b}. In \textbf{Set}, \code{g} would be the +that object to \code{b}. In $\Set$, \code{g} would be the function that maps every pair \code{(f,\ x)} to \code{f\ x}. So that's the pattern: a product of two objects \code{z} and @@ -102,7 +102,7 @@ \section{Universal Construction}\label{universal-construction} Let's review the universal construction. We start with a pattern of objects and morphisms. That's our imprecise query, and it usually yields -lots and lots of hits. In particular, in \textbf{Set}, pretty much +lots and lots of hits. In particular, in $\Set$, pretty much everything is connected to everything. We can take any object \code{z}, form its product with \code{a}, and there's going to be a function from it to \code{b} (except when \code{b} is an empty set). @@ -202,7 +202,7 @@ \section{Universal Construction}\label{universal-construction} \noindent Of course, there is no guarantee that such an object \code{a\ensuremath{\Rightarrow}b} exists for any pair of objects \code{a} and \code{b} in a given category. -But it always does in \textbf{Set}. Moreover, in \textbf{Set}, this +But it always does in $\Set$. Moreover, in $\Set$, this object is isomorphic to the hom-set \emph{Set(a, b)}. This is why, in Haskell, we interpret the function type @@ -219,7 +219,7 @@ \section{Currying}\label{currying} g :: z × a -> b \end{Verbatim} Being a morphism from a product comes as close as it gets to being a -function of two variables. In particular, in \textbf{Set}, \code{g} is +function of two variables. In particular, in $\Set$, \code{g} is a function from pairs of values, one from the set \code{z} and one from the set \code{a}. @@ -230,7 +230,7 @@ \section{Currying}\label{currying} \begin{Verbatim}[commandchars=\\\{\}] h :: z -> (a⇒b) \end{Verbatim} -In \textbf{Set}, this just means that \code{h} is a function that +In $\Set$, this just means that \code{h} is a function that takes one variable of type \code{z} and returns a function from \code{a} to \code{b}. That makes \code{h} a higher order function. Therefore the universal construction establishes a one-to-one @@ -408,7 +408,7 @@ \section{Cartesian Closed Although I will continue using the category of sets as a model for types and functions, it's worth mentioning that there is a larger family of categories that can be used for that purpose. These categories are -called \newterm{cartesian closed}, and \textbf{Set} is just one example of +called \newterm{cartesian closed}, and $\Set$ is just one example of such a category. A cartesian closed category must contain: @@ -442,7 +442,7 @@ \section{Cartesian Closed (b + c) × a = b × a + c × a \end{Verbatim} is called a \newterm{bicartesian closed} category. We'll see in the next -section that bicartesian closed categories, of which \textbf{Set} is a +section that bicartesian closed categories, of which $\Set$ is a prime example, have some interesting properties. \section{Exponentials and Algebraic Data @@ -468,8 +468,8 @@ \subsection{Zeroth Power}\label{zeroth-power} set of morphisms going from the initial object to an arbitrary object \code{a}. By the definition of the initial object, there is exactly one such morphism, so the hom-set \emph{C(0, a)} is a singleton set. A -singleton set is the terminal object in \textbf{Set}, so this identity -trivially works in \textbf{Set}. What we are saying is that it works in +singleton set is the terminal object in $\Set$, so this identity +trivially works in $\Set$. What we are saying is that it works in any bicartesian closed category. In Haskell, we replace 0 with \code{Void}; 1 with the unit type @@ -492,7 +492,7 @@ \subsection{Powers of One}\label{powers-of-one} \begin{Verbatim}[commandchars=\\\{\}] 1\textsuperscript{a} = 1 \end{Verbatim} -This identity, when interpreted in \textbf{Set}, restates the definition +This identity, when interpreted in $\Set$, restates the definition of the terminal object: There is a unique morphism from any object to the terminal object. In general, the internal hom-object from \code{a} to the terminal object is isomorphic to the terminal object itself. @@ -510,7 +510,7 @@ \subsection{First Power}\label{first-power} This is a restatement of the observation that morphisms from the terminal object can be used to pick ``elements'' of the object \code{a}. The set of such morphisms is isomorphic to the object -itself. In \textbf{Set}, and in Haskell, the isomorphism is between +itself. In $\Set$, and in Haskell, the isomorphism is between elements of the set \code{a} and functions that pick those elements, \code{()->a}. diff --git a/src/content/2.2/Limits and Colimits.tex b/src/content/2.2/Limits and Colimits.tex index e59a130a..e4ee69df 100644 --- a/src/content/2.2/Limits and Colimits.tex +++ b/src/content/2.2/Limits and Colimits.tex @@ -210,7 +210,7 @@ \section{Limit as a Natural Isomorphism}\label{limit-as-a-natural-isomorphism} But what are the functors that are related by this transformation? One functor is the mapping of \code{c} to the set -\code{C(c, Lim D)}. It's a functor from \mathtext{C} to \textbf{Set} --- +\code{C(c, Lim D)}. It's a functor from \mathtext{C} to $\Set$ --- it maps objects to sets. In fact it's a contravariant functor. Here's how we define its action on morphisms: Let's take a morphism \code{f} from \code{c'} to \code{c}: @@ -311,13 +311,13 @@ \section{Limit as a Natural Isomorphism}\label{limit-as-a-natural-isomorphism} c -> Nat(\ensuremath{\Delta_c}, D) \end{Verbatim} What I have just done is to show you that we have two (contravariant) -functors from \mathtext{C} to \textbf{Set}. I haven't made any assumptions +functors from \mathtext{C} to $\Set$. I haven't made any assumptions --- these functors always exist. Incidentally, the first of these functors plays an important role in category theory, and we'll see it again when we talk about Yoneda's lemma. There is a name for contravariant functors from any category -\mathtext{C} to \textbf{Set}: they are called ``presheaves''. This one is +\mathtext{C} to $\Set$: they are called ``presheaves''. This one is called a \newterm{representable presheaf}. The second functor is also a presheaf. @@ -337,7 +337,7 @@ \section{Limit as a Natural Isomorphism}\label{limit-as-a-natural-isomorphism} I'm not going to go through the proof of this statement. The procedure is pretty straightforward if not tedious. When dealing with natural transformations, you usually focus on components, which are morphisms. -In this case, since the target of both functors is \textbf{Set}, the +In this case, since the target of both functors is $\Set$, the components of the natural isomorphism will be functions. These are higher order functions, because they go from the hom-set to the set of natural transformations. Again, you can analyze a function by @@ -409,7 +409,7 @@ \section{Examples of Limits}\label{examples-of-limits} f . p = g . p \end{Verbatim} The way to think about it is that, if we restrict our attention to -\textbf{Set}, the image of the function \code{p} selects a subset of +$\Set$, the image of the function \code{p} selects a subset of \code{a}. When restricted to this subset, the functions \code{f} and \code{g} are equal. @@ -680,7 +680,7 @@ \section{Continuity}\label{continuity} \end{Verbatim} When its second argument is fixed, the hom-set functor (which becomes the representable presheaf) maps colimits in \mathtext{C} to limits in -\textbf{Set}; and when its first argument is fixed, it maps limits to +$\Set$; and when its first argument is fixed, it maps limits to limits. In Haskell, a hom-functor is the mapping of any two types to a function diff --git a/src/content/2.3/Free Monoids.tex b/src/content/2.3/Free Monoids.tex index 30be3030..0abeaafa 100644 --- a/src/content/2.3/Free Monoids.tex +++ b/src/content/2.3/Free Monoids.tex @@ -155,7 +155,7 @@ \section{Free Monoid Universal Construction}\label{free-monoid-universal-constru \textbf{Mon} to sets, but we can also map morphisms of \textbf{Mon} (homomorphisms) to functions. Again, this seems sort of trivial, but it will become useful soon. This mapping of objects and morphisms from -\textbf{Mon} to \textbf{Set} is in fact a functor. Since this functor +\textbf{Mon} to $\Set$ is in fact a functor. Since this functor ``forgets'' the monoidal structure --- once we are inside a plain set, we no longer distinguish the unit element or care about multiplication --- it's called a \newterm{forgetful functor}. Forgetful functors come up @@ -183,17 +183,17 @@ \section{Free Monoid Universal Construction}\label{free-monoid-universal-constru those blobs. Here's how it works: We start with a set of generators, \code{x}. That's a set in -\textbf{Set}. +$\Set$. The pattern we are going to match consists of a monoid \code{m} --- an -object of \textbf{Mon} --- and a function \code{p} in \textbf{Set}: +object of \textbf{Mon} --- and a function \code{p} in $\Set$: \begin{Verbatim}[commandchars=\\\{\}] p :: x -> U m \end{Verbatim} where \code{U} is our forgetful functor from \textbf{Mon} to -\textbf{Set}. This is a weird heterogeneous pattern --- half in -\textbf{Mon} and half in \textbf{Set}. +$\Set$. This is a weird heterogeneous pattern --- half in +\textbf{Mon} and half in $\Set$. The idea is that the function \code{p} will identify the set of generators inside the X-ray image of \code{m}. It doesn't matter that diff --git a/src/content/2.4/Representable Functors.tex b/src/content/2.4/Representable Functors.tex index 081c61a5..c63fc533 100644 --- a/src/content/2.4/Representable Functors.tex +++ b/src/content/2.4/Representable Functors.tex @@ -3,7 +3,7 @@ mathematics --- at least it used to be. Category theory tries to step away from set theory, to some extent. For instance, it's a known fact that the set of all sets doesn't exist, but the category of all sets, -\textbf{Set}, does. So that's good. On the other hand, we assume that +$\Set$, does. So that's good. On the other hand, we assume that morphisms between any two objects in a category form a set. We even called it a hom-set. To be fair, there is a branch of category theory where morphisms don't form sets. Instead they are objects in another @@ -46,14 +46,14 @@ \section{The Hom Functor}\label{the-hom-functor} Every category comes equipped with a canonical family of mappings to -\textbf{Set}. Those mappings are in fact functors, so they preserve the +$\Set$. Those mappings are in fact functors, so they preserve the structure of the category. Let's build one such mapping. Let's fix one object \code{a} in \emph{C} and pick another object \code{x} also in \emph{C}. The hom-set \code{C(a, x)} is a set, an -object in \textbf{Set}. When we vary \code{x}, keeping \code{a} -fixed, \code{C(a, x)} will also vary in \textbf{Set}. Thus we have a -mapping from \code{x} to \textbf{Set}. +object in $\Set$. When we vary \code{x}, keeping \code{a} +fixed, \code{C(a, x)} will also vary in $\Set$. Thus we have a +mapping from \code{x} to $\Set$. \begin{figure}[H] \centering @@ -163,16 +163,16 @@ \section{The Hom Functor}\label{the-hom-functor} \section{Representable Functors}\label{representable-functors} We've seen that, for every choice of an object \code{a} in \emph{C}, -we get a functor from \emph{C} to \textbf{Set}. This kind of -structure-preserving mapping to \textbf{Set} is often called a +we get a functor from \emph{C} to $\Set$. This kind of +structure-preserving mapping to $\Set$ is often called a \newterm{representation}. We are representing objects and morphisms of -\emph{C} as sets and functions in \textbf{Set}. +\emph{C} as sets and functions in $\Set$. The functor \code{C(a, -)} itself is sometimes called representable. More generally, any functor \code{F} that is naturally isomorphic to the hom-functor, for some choice of \code{a}, is called \newterm{representable}. Such functor must necessarily be -\textbf{Set}-valued, since \code{C(a, -)} is. +$\Set$-valued, since \code{C(a, -)} is. I said before that we often think of isomorphic sets as identical. More generally, we think of isomorphic \newterm{objects} in a category as @@ -203,7 +203,7 @@ \section{Representable Functors}\label{representable-functors} natural transformation. Let's look at the component of α at some object \code{x}. It's a -function in \textbf{Set}: +function in $\Set$: \begin{Verbatim}[commandchars=\\\{\}] α\textsubscript{x} :: C(a, x) -> F x @@ -248,7 +248,7 @@ \section{Representable Functors}\label{representable-functors} α ◦ β = id = β ◦ α \end{Verbatim} We will see later that a natural transformation from \code{C(a, -)} -to any \textbf{Set}-valued functor always exists (Yoneda's lemma) but it +to any $\Set$-valued functor always exists (Yoneda's lemma) but it is not necessarily invertible. Let me give you an example in Haskell with the list functor and @@ -328,7 +328,7 @@ \section{Representable Functors}\label{representable-functors} Representability for contravariant functors is similarly defined, except that we keep the second argument of \code{C(-, a)} fixed. Or, equivalently, we may consider functors from \emph{C}\textsuperscript{op} -to \textbf{Set}, because \code{C\textsuperscript{op}(a, -)} is the same as +to $\Set$, because \code{C\textsuperscript{op}(a, -)} is the same as \code{C(-, a)}. There is an interesting twist to representability. Remember that @@ -370,7 +370,7 @@ \section{Challenges}\label{challenges} \tightlist \item Show that the hom-functors map identity morphisms in \emph{C} to - corresponding identity functions in \textbf{Set}. + corresponding identity functions in $\Set$. \item Show that \code{Maybe} is not representable. \item diff --git a/src/content/2.5/The Yoneda Lemma.tex b/src/content/2.5/The Yoneda Lemma.tex index fd4f4a57..9f9234d5 100644 --- a/src/content/2.5/The Yoneda Lemma.tex +++ b/src/content/2.5/The Yoneda Lemma.tex @@ -13,10 +13,10 @@ group of some set). The setting for the Yoneda lemma is an arbitrary category \emph{C} -together with a functor \code{F} from \emph{C} to \textbf{Set}. We've -seen in the previous section that some \textbf{Set}-valued functors are +together with a functor \code{F} from \emph{C} to $\Set$. We've +seen in the previous section that some $\Set$-valued functors are representable, that is isomorphic to a hom-functor. The Yoneda lemma -tells us that all \textbf{Set}-valued functors can be obtained from +tells us that all $\Set$-valued functors can be obtained from hom-functors through natural transformations, and it explicitly enumerates all such transformations. @@ -27,7 +27,7 @@ connected to it through a morphism. The more arrows between objects in the source and the target categories there are, the more constraints you have for transporting the components of natural transformations. -\textbf{Set} happens to be a very arrow-rich category. +$\Set$ happens to be a very arrow-rich category. The Yoneda lemma tells us that a natural transformation between a hom-functor and any other functor \code{F} is completely determined by @@ -41,11 +41,11 @@ also seen that it maps any morphism \code{f} from \code{x} to \code{y} to \code{C(a, f)}. -The second functor is an arbitrary \textbf{Set}-valued functor +The second functor is an arbitrary $\Set$-valued functor \code{F}. Let's call the natural transformation between these two functors -\code{α}. Because we are operating in \textbf{Set}, the components of +\code{α}. Because we are operating in $\Set$, the components of the natural transformation, like \code{αx} or \code{αy}, are just regular functions between sets: @@ -127,7 +127,7 @@ Nat(C(a, -), F) \ensuremath{\cong} F a \end{Verbatim} Or, if we use the notation \code{{[}C, Set{]}} for the functor -category between \emph{C} and \textbf{Set}, the set of natural +category between \emph{C} and $\Set$, the set of natural transformation is just a hom-set in that category, and we can write: \begin{Verbatim}[commandchars=\\\{\}] @@ -140,7 +140,7 @@ thing is that the whole natural transformation crystallizes from just one nucleation site: the value we assign to it at \code{id\textsubscript{a}}. It spreads from that point following the naturality condition. It floods -the image of \emph{C} in \textbf{Set}. So let's first consider what the +the image of \emph{C} in $\Set$. So let's first consider what the image of \emph{C} is under \code{C(a, -)}. Let's start with the image of \code{a} itself. Under the hom-functor @@ -231,17 +231,17 @@ transformation: it can only be \code{absurd}. One way of understanding the Yoneda lemma is to realize that natural -transformations between \textbf{Set}-valued functors are just families +transformations between $\Set$-valued functors are just families of functions, and functions are in general lossy. A function may collapse information and it may cover only parts of its codomain. The only functions that are not lossy are the ones that are invertible --- the isomorphisms. It follows then that the best structure-preserving -\textbf{Set}-valued functors are the representable ones. They are either +$\Set$-valued functors are the representable ones. They are either the hom-functors or the functors that are naturally isomorphic to hom-functors. Any other functor \code{F} is obtained from a hom-functor through a lossy transformation. Such a transformation may not only lose information, but it may also cover only a small part of -the image of the functor \code{F} in \textbf{Set}. +the image of the functor \code{F} in $\Set$. \section{Yoneda in Haskell}\label{yoneda-in-haskell} @@ -344,7 +344,7 @@ \section{Co-Yoneda}\label{co-yoneda} Equivalently, we can derive the co-Yoneda lemma by fixing the target object of our hom-functors instead of the source. We get the -contravariant hom-functor from \emph{C} to \textbf{Set}: +contravariant hom-functor from \emph{C} to $\Set$: \code{C(-, a)}. The contravariant version of the Yoneda lemma establishes one-to-one correspondence between natural transformations from this functor to any other contravariant functor \code{F} and the diff --git a/src/content/2.6/Yoneda Embedding.tex b/src/content/2.6/Yoneda Embedding.tex index 44542eab..32f7a28b 100644 --- a/src/content/2.6/Yoneda Embedding.tex +++ b/src/content/2.6/Yoneda Embedding.tex @@ -1,11 +1,11 @@ \lettrine[lhang=0.17]{W}{e've seen previously} that, when we fix an object \code{a} in the category \emph{C}, the mapping \code{C(a, -)} is a (covariant) -functor from \emph{C} to \textbf{Set}. +functor from \emph{C} to $\Set$. \begin{Verbatim}[commandchars=\\\{\}] x -> C(a, x) \end{Verbatim} -(The codomain is \textbf{Set} because the hom-set C(a, x) is a +(The codomain is $\Set$ because the hom-set C(a, x) is a \emph{set}.) We call this mapping a hom-functor --- we have previously defined its action on morphisms as well. @@ -20,7 +20,7 @@ categories in \hyperref[natural-transformations]{Natural Transformations}). Let's use the notation \code{{[}C, Set{]}} for the -functor category from \emph{C} to \textbf{Set}. You may also recall that +functor category from \emph{C} to $\Set$. You may also recall that hom-functors are the prototypical \hyperref[chap-representable-functors]{representable functors}. @@ -109,14 +109,14 @@ \section{The Embedding}\label{the-embedding} This is a very useful result because mathematicians know a lot about the category of functors, especially functors whose codomain is -\textbf{Set}. We can get a lot of insight about an arbitrary category +$\Set$. We can get a lot of insight about an arbitrary category \emph{C} by embedding it in the functor category. Of course there is a dual version of the Yoneda embedding, sometimes called the co-Yoneda embedding. Observe that we could have started by fixing the target object (rather than the source object) of each hom-set, \code{C(-, a)}. That would give us a contravariant -hom-functor. Contravariant functors from \emph{C} to \textbf{Set} are +hom-functor. Contravariant functors from \emph{C} to $\Set$ are our familiar presheaves (see, for instance, \hyperref[limits-and-colimits]{Limits and Colimits}). The co-Yoneda embedding defines the embedding of a @@ -259,7 +259,7 @@ \section{Preorder Example}\label{preorder-example} \section{Naturality}\label{naturality} The Yoneda lemma establishes the isomorphism between the set of natural -transformations and an object in \textbf{Set}. Natural transformations +transformations and an object in $\Set$. Natural transformations are morphisms in the functor category \code{{[}C, Set{]}}. The set of natural transformation between any two functors is a hom-set in that category. The Yoneda lemma is the isomorphism: @@ -276,7 +276,7 @@ \section{Naturality}\label{naturality} Let's think for a moment what this means. A natural isomorphism is an invertible \newterm{natural transformation} between two functors. And indeed, the right hand side of our isomorphism is a functor. It's a -functor from \code{{[}C, Set{]} × C} to \textbf{Set}. Its action on +functor from \code{{[}C, Set{]} × C} to $\Set$. Its action on a pair \code{(F, a)} is a set --- the result of evaluating the functor \code{F} at the object \code{a}. This is called the evaluation functor. diff --git a/src/content/3.10/Ends and Coends.tex b/src/content/3.10/Ends and Coends.tex index a4132d11..5ceb17c6 100644 --- a/src/content/3.10/Ends and Coends.tex +++ b/src/content/3.10/Ends and Coends.tex @@ -131,7 +131,7 @@ \section{Ends}\label{ends} profunctor. Instead of a cone, we have a wedge. The base of a wedge is formed by diagonal elements of a profunctor \code{p}. The apex of the wedge is an object (here, a set, since we are considering -\textbf{Set}-valued profunctors), and the sides are a family of +$\Set$-valued profunctors), and the sides are a family of functions mapping the apex to the sets in the base. You may think of this family as one polymorphic function --- a function that's polymorphic in its return type: @@ -241,8 +241,8 @@ \section{Ends}\label{ends} diamond when we realize that \code{\ensuremath{\Delta}\textsubscript{c}} lifts all morphisms to one identity function. -Ends can also be defined for target categories other than \textbf{Set}, -but here we'll only consider \textbf{Set}-valued profunctors and their +Ends can also be defined for target categories other than $\Set$, +but here we'll only consider $\Set$-valued profunctors and their ends. \section{Ends as Equalizers}\label{ends-as-equalizers} diff --git a/src/content/3.11/Kan Extensions.tex b/src/content/3.11/Kan Extensions.tex index 3a9e7b46..18028034 100644 --- a/src/content/3.11/Kan Extensions.tex +++ b/src/content/3.11/Kan Extensions.tex @@ -346,12 +346,12 @@ \section{Kan Extensions as Ends}\label{kan-extensions-as-ends} The real power of Kan extensions comes from the fact that they can be calculated using ends (and coends). For simplicity, we'll restrict our attention to the case where the target category \emph{C} is -\textbf{Set}, but the formulas can be extended to any category. +$\Set$, but the formulas can be extended to any category. Let's revisit the idea that a Kan extension can be used to extend the action of a functor outside of its original domain. Suppose that \code{K} embeds \emph{I} inside \emph{A}. Functor \code{D} maps -\emph{I} to \textbf{Set}. We could just say that for any object +\emph{I} to $\Set$. We could just say that for any object \code{a} in the image of \code{K}, that is \code{a = K i}, the extended functor maps \code{a} to \code{D i}. The problem is, what to do with those objects in \emph{A} that are outside of the image of diff --git a/src/content/3.12/Enriched Categories.tex b/src/content/3.12/Enriched Categories.tex index 09dc18c4..23fe37d5 100644 --- a/src/content/3.12/Enriched Categories.tex +++ b/src/content/3.12/Enriched Categories.tex @@ -10,7 +10,7 @@ form a set. If they don't form a set, we have to rethink a few definitions. In particular, what does it mean to compose morphisms if we can't even pick them from a set? The solution is to bootstrap ourselves -by replacing hom-sets, which are objects in \textbf{Set}, with +by replacing hom-sets, which are objects in $\Set$, with \newterm{objects} from some other category \emph{V}. The difference is that, in general, objects don't have elements, so we are no longer allowed to talk about individual morphisms. We have to define all @@ -38,7 +38,7 @@ \section{Why Monoidal Category?}\label{why-monoidal-category} When constructing an enriched category we have to keep in mind that we should be able to recover the usual definitions when we replace the -monoidal category with \textbf{Set} and hom-objects with hom-sets. The +monoidal category with $\Set$ and hom-objects with hom-sets. The best way to accomplish this is to start with the usual definitions and keep reformulating them in a point-free manner --- that is, without naming elements of sets. @@ -153,7 +153,7 @@ \section{Monoidal Category}\label{monoidal-category} \end{Verbatim} A monoidal category in which both are defined is called biclosed. An example of a category that is not biclosed is the category of -endofunctors in \textbf{Set}, with functor composition serving as tensor +endofunctors in $\Set$, with functor composition serving as tensor product. That's the category we used to define monads. \section{Enriched Category}\label{enriched-category} @@ -419,11 +419,11 @@ \section{Self Enrichment}\label{self-enrichment} We know that this hom-set contains the left identity \code{λ\textsubscript{a}}. We can define \code{j\textsubscript{a}} as its image under the adjunction. -A practical example of self-enrichment is the category \textbf{Set} that +A practical example of self-enrichment is the category $\Set$ that serves as the prototype for types in programming languages. We've seen before that it's a closed monoidal category with respect to cartesian -product. In \textbf{Set}, the hom-set between any two sets is itself a -set, so it's an object in \textbf{Set}. We know that it's isomorphic to +product. In $\Set$, the hom-set between any two sets is itself a +set, so it's an object in $\Set$. We know that it's isomorphic to the exponential set, so the external and the internal homs are equivalent. Now we also know that, through self-enrichment, we can use the exponential set as the hom-object and express composition in terms @@ -441,8 +441,8 @@ \section{Relation to 2-Categories}\label{relation-to-2-categories} But notice that functors between two categories form a category too; so, in \textbf{Cat}, we really have a \newterm{hom-category} rather than a -hom-set. It turns out that, just like \textbf{Set} can be treated as a -category enriched over \textbf{Set}, \textbf{Cat} can be treated as a +hom-set. It turns out that, just like $\Set$ can be treated as a +category enriched over $\Set$, \textbf{Cat} can be treated as a category enriched over \textbf{Cat}. Even more generally, just like -every category can be treated as enriched over \textbf{Set}, every +every category can be treated as enriched over $\Set$, every 2-category can be considered enriched over \textbf{Cat}. \ No newline at end of file diff --git a/src/content/3.13/Topoi.tex b/src/content/3.13/Topoi.tex index 22a79dc6..8222619e 100644 --- a/src/content/3.13/Topoi.tex +++ b/src/content/3.13/Topoi.tex @@ -25,7 +25,7 @@ things like continuity. And the conventional approach to topology is, you guessed it, through set theory. In particular, the notion of a subset is central to topology. Not surprisingly, category theorists -generalized this idea to categories other than \textbf{Set}. The type of +generalized this idea to categories other than $\Set$. The type of category that has just the right properties to serve as a replacement for set theory is called a \newterm{topos} (plural: topoi), and it provides, among other things, a generalized notion of a subset. @@ -128,7 +128,7 @@ \section{Subobject Classifier}\label{subobject-classifier} define what a subobject is, but also define the special object \code{Ω} without talking about elements. The idea is that we want the morphism \code{true} to represent a ``generic'' subobject. In -\textbf{Set}, it picks a single-element subset from a two-element set +$\Set$, it picks a single-element subset from a two-element set \code{Ω}. This is as generic as it gets. It's clearly a proper subset, because \code{Ω} has one more element that's \emph{not} in that subset. @@ -137,7 +137,7 @@ \section{Subobject Classifier}\label{subobject-classifier} from the terminal object to the \emph{classifying object} \code{Ω}. But we have to define the classifying object. We need a universal property that links this object to the characteristic function. It turns -out that, in \textbf{Set}, the pullback of \code{true} along the +out that, in $\Set$, the pullback of \code{true} along the characteristic function \code{χ} defines both the subset \code{a} and the injective function that embeds it in \code{b}. Here's the pullback diagram: @@ -162,7 +162,7 @@ \section{Subobject Classifier}\label{subobject-classifier} \code{f} is injective. This pullback diagram can be used to define the classifying object in -categories other than \textbf{Set}. Such a category must have a terminal +categories other than $\Set$. Such a category must have a terminal object, which will let us define the monomorphism \code{true}. It must also have pullbacks --- the actual requirement is that it must have all finite limits (a pullback is an example of a finite limit). Under those @@ -220,14 +220,14 @@ \section{Topos}\label{topos} Has a subobject classifier \code{Ω}. \end{enumerate} -This set of properties makes a topos a shoe-in for \textbf{Set} in most +This set of properties makes a topos a shoe-in for $\Set$ in most applications. It also has additional properties that follow from its definition. For instance, a topos has all finite colimits, including the initial object. It would be tempting to define the subobject classifier as a coproduct (sum) of two copies of the terminal object --that's what it is in -\textbf{Set}--- but we want to be more general than that. Topoi in which +$\Set$--- but we want to be more general than that. Topoi in which this is true are called Boolean. \section{Topoi and Logic}\label{topoi-and-logic} diff --git a/src/content/3.14/Lawvere Theories.tex b/src/content/3.14/Lawvere Theories.tex index b6b68e20..4cb15ffa 100644 --- a/src/content/3.14/Lawvere Theories.tex +++ b/src/content/3.14/Lawvere Theories.tex @@ -31,7 +31,7 @@ \section{Universal Algebra}\label{universal-algebra} universally quantified. This definition of a universal algebra can be extended to categories -other than \textbf{Set}, if we replace operations (functions) with +other than $\Set$, if we replace operations (functions) with morphisms. Instead of a set, we select an object \code{a} (called a generic object). A unary operation is just an endomorphism of \code{a}. But what about other arities (\newterm{arity} is the number of @@ -216,9 +216,9 @@ \section{Models of Lawvere Theories}\label{models-of-lawvere-theories} essence of being a monoid. It must be valid for all monoids. A particular monoid becomes a model of such a theory. A model is defined as a functor from the Lawvere theory \textbf{L} to the category of sets -\textbf{Set}. (There are generalizations of Lawvere theories that use +$\Set$. (There are generalizations of Lawvere theories that use other categories for models but here I'll just concentrate on -\textbf{Set}.) Since the structure of \textbf{L} depends heavily on +$\Set$.) Since the structure of \textbf{L} depends heavily on products, we require that such a functor preserve finite products. A model of \textbf{L}, also called the algebra over the Lawvere theory \textbf{L}, is therefore defined by a functor: @@ -232,7 +232,7 @@ \section{Models of Lawvere Theories}\label{models-of-lawvere-theories} products would eliminate most interesting theories. The preservation of products by models means that the image of -\code{M} in \textbf{Set} is a sequence of sets generated by powers of +\code{M} in $\Set$ is a sequence of sets generated by powers of the set \code{M 1} --- the image of the object \code{1} from \textbf{L}. Let's call this set \code{a}. (This set is sometimes called a \newterm{sort}, and such algebra is called single-sorted. There @@ -243,7 +243,7 @@ \section{Models of Lawvere Theories}\label{models-of-lawvere-theories} a × a -> a \end{Verbatim} As with any functor, it's possible that multiple morphisms in \textbf{L} -are collapsed to the same function in \textbf{Set}. +are collapsed to the same function in $\Set$. Incidentally, the fact that all laws are universally quantified equalities means that every Lawvere theory has a trivial model: a @@ -286,12 +286,12 @@ \section{Models of Lawvere Theories}\label{models-of-lawvere-theories} \textbf{F}\textsuperscript{op}. Such model is completely determined by its value at \code{1}, \code{M 1}. Since \code{M 1} can be any set, there are as many of these models as there are sets in -\textbf{Set}. Moreover, every morphism in \code{Mod(F\textsuperscript{op}, Set)} (a +$\Set$. Moreover, every morphism in \code{Mod(F\textsuperscript{op}, Set)} (a natural transformation between functors \code{M} and \code{N}) is uniquely determined by its component at \code{M 1}. Conversely, every function \code{M 1 -> N 1} induces a natural transformation between the two models \code{M} and \code{N}. -Therefore \code{Mod(F\textsuperscript{op}, Set)} is equivalent to \textbf{Set}. +Therefore \code{Mod(F\textsuperscript{op}, Set)} is equivalent to $\Set$. \section{The Theory of Monoids}\label{the-theory-of-monoids} @@ -373,7 +373,7 @@ \section{Lawvere Theories and Monads}\label{lawvere-theories-and-monads} Mod(L, Set) -> Mod(F\textsuperscript{op}, Set) \end{Verbatim} But, as we discussed, the category of models of -\textbf{F}\textsubscript{op} is equivalent to \textbf{Set}, so we get +\textbf{F}\textsubscript{op} is equivalent to $\Set$, so we get the forgetful functor: \begin{Verbatim}[commandchars=\\\{\}] @@ -410,7 +410,7 @@ \section{Lawvere Theories and Monads}\label{lawvere-theories-and-monads} \end{Verbatim} Together, the forgetful and the free functor define a \hyperref[monads-categorically]{monad} -\code{T = U◦F} on \textbf{Set}. Thus every Lawvere theory generates +\code{T = U◦F} on $\Set$. Thus every Lawvere theory generates a monad. It turns out that the category of @@ -424,7 +424,7 @@ \section{Lawvere Theories and Monads}\label{lawvere-theories-and-monads} The connection between monads and Lawvere theories doesn't go both ways, though. Only finitary monads lead to Lawvere thories. A finitary monad -is based on a finitary functor. A finitary functor on \textbf{Set} is +is based on a finitary functor. A finitary functor on $\Set$ is fully determined by its action on finite sets. Its action on an arbitrary set \code{a} can be evaluated using the following coend: @@ -446,7 +446,7 @@ \section{Lawvere Theories and Monads}\label{lawvere-theories-and-monads} \begin{Verbatim}[commandchars=\\\{\}] T\textsubscript{L} a = ∫ \textsuperscript{n} a\textsuperscript{n} × L(n, 1) \end{Verbatim} -Conversely, given any finitary monad \code{T} on \textbf{Set}, we can +Conversely, given any finitary monad \code{T} on $\Set$, we can construct a Lawvere theory. We start by constructing a Kleisli category for \code{T}. As you may remember, a morphism in a Kleisli category from \code{a} to \code{b} is given by a morphism in the underlying @@ -526,7 +526,7 @@ \section{Monads as Coends}\label{monads-as-coends} by the functor \code{I\textsubscript{L}}). Let's check the functoriality of \code{L(m, 1)} as a functor from -\textbf{F} to \textbf{Set}. We want to lift a function +\textbf{F} to $\Set$. We want to lift a function \code{f :: m -> n}, so our goal is to implement a function from \code{L(m, 1)} to \code{L(n, 1)}. Corresponding to the function \code{f} there is a morphism in \textbf{L} from @@ -695,8 +695,8 @@ \section{Challenges}\label{challenges} binary operations can be generated using the corresponding Kleisli arrows. \item - \textbf{FinSet} is a subcategory of \textbf{Set} and there is a - functor that embeds it in \textbf{Set}. Any functor on \textbf{Set} + \textbf{FinSet} is a subcategory of $\Set$ and there is a + functor that embeds it in $\Set$. Any functor on $\Set$ can be restricted to \textbf{FinSet}. Show that a finitary functor is the left Kan extension of its own restriction. \end{enumerate} diff --git a/src/content/3.15/Monads, Monoids, and Categories.tex b/src/content/3.15/Monads, Monoids, and Categories.tex index 65805aa1..463a1bdd 100644 --- a/src/content/3.15/Monads, Monoids, and Categories.tex +++ b/src/content/3.15/Monads, Monoids, and Categories.tex @@ -17,10 +17,10 @@ \section{Bicategories}\label{bicategories} are used to defining sets in terms of elements. An empty set has no elements. A singleton set has one element. A cartesian product of two sets is a set of pairs, and so on. But when talking about the category -\textbf{Set} I asked you to forget about the contents of sets and +$\Set$ I asked you to forget about the contents of sets and instead concentrate on morphisms (arrows) between them. You were allowed, from time to time, to peek under the covers to see what a -particular universal construction in \textbf{Set} described in terms of +particular universal construction in $\Set$ described in terms of elements. The terminal object turned out to be a set with one element, and so on. But these were just sanity checks. @@ -31,7 +31,7 @@ \section{Bicategories}\label{bicategories} we forfeit the information about its action on the internals of a category (its objects and morphisms), just like we forfeit the information about the action of a function on elements of a set when we -treat it as an arrow in \textbf{Set}. But functors between any two +treat it as an arrow in $\Set$. But functors between any two categories also form a category. This time you are asked to consider something that was an arrow in one category to be an object in another. In a functor category functors are objects and natural transformations diff --git a/src/content/3.2/Adjunctions.tex b/src/content/3.2/Adjunctions.tex index 9b5d49d8..ad816490 100644 --- a/src/content/3.2/Adjunctions.tex +++ b/src/content/3.2/Adjunctions.tex @@ -311,7 +311,7 @@ \section{Adjunctions and Hom-Sets}\label{adjunctions-and-hom-sets} Naturality means that the source \code{d} can be varied smoothly across \emph{D}; and the target \code{c}, across \emph{C}. More precisely, we have a natural transformation \code{φ} between the -following two (covariant) functors from \emph{C} to \textbf{Set}. Here's +following two (covariant) functors from \emph{C} to $\Set$. Here's the action of these functors on objects: \begin{Verbatim}[commandchars=\\\{\}] @@ -406,12 +406,12 @@ \section{Adjunctions and Hom-Sets}\label{adjunctions-and-hom-sets} functor}. The reason for this is that, to the first approximation, we can treat the category of Haskell types as the category of sets. -When the right category \emph{D} is \textbf{Set}, the right adjoint -\code{R} is a functor from \emph{C} to \textbf{Set}. Such a functor is +When the right category \emph{D} is $\Set$, the right adjoint +\code{R} is a functor from \emph{C} to $\Set$. Such a functor is representable if we can find an object \code{rep} in \emph{C} such that the hom-functor \code{C(rep, \_)} is naturally isomorphic to \code{R}. It turns out that, if \code{R} is the right adjoint of -some functor \code{L} from \textbf{Set} to \emph{C}, such an object +some functor \code{L} from $\Set$ to \emph{C}, such an object always exists --- it's the image of the singleton set \code{()} under \code{L}: diff --git a/src/content/3.3/Free-Forgetful Adjunctions.tex b/src/content/3.3/Free-Forgetful Adjunctions.tex index c230c28a..e40427a4 100644 --- a/src/content/3.3/Free-Forgetful Adjunctions.tex +++ b/src/content/3.3/Free-Forgetful Adjunctions.tex @@ -6,7 +6,7 @@ sets, have no internal structure --- they have no elements. Still, those objects often carry the memory of sets, in the sense that there is a mapping --- a functor --- from a given category \emph{C} to -\textbf{Set}. A set corresponding to some object in \emph{C} is called +$\Set$. A set corresponding to some object in \emph{C} is called its \newterm{underlying set}. Monoids are such objects that have underlying sets --- sets of elements. @@ -140,7 +140,7 @@ \section{Some Intuitions}\label{some-intuitions} together multiple elements of a set. Also, their image may cover only part of their codomain. -An ``average'' hom-set in \textbf{Set} will contain a whole spectrum of +An ``average'' hom-set in $\Set$ will contain a whole spectrum of functions starting with the ones that are least lossy (e.g., injections or, possibly, isomorphisms) and ending with constant functions that collapse the whole domain to a single element (if there is one). @@ -148,7 +148,7 @@ \section{Some Intuitions}\label{some-intuitions} I tend to think of morphisms in an arbitrary category as being lossy too. It's just a mental model, but it's a useful one, especially when thinking of adjunctions --- in particular those in which one of the -categories is \textbf{Set}. +categories is $\Set$. Formally, we can only speak of morphisms that are invertible (isomorphisms) or non-invertible. It's that latter kind that may be @@ -166,7 +166,7 @@ \section{Some Intuitions}\label{some-intuitions} When we apply a forgetful functor \code{U} to an object \code{c} in \emph{C}, we think of it as revealing the ``internal structure'' of -\code{c}. In fact, if \emph{D} is \textbf{Set} we think of \code{U} +\code{c}. In fact, if \emph{D} is $\Set$ we think of \code{U} as \emph{defining} the internal structure of \code{c} --- its underlying set. (In an arbitrary category, we can't talk about the internals of an object other than through its connections to other diff --git a/src/content/3.5/Monads and Effects.tex b/src/content/3.5/Monads and Effects.tex index 22340eae..8f2679c0 100644 --- a/src/content/3.5/Monads and Effects.tex +++ b/src/content/3.5/Monads and Effects.tex @@ -97,7 +97,7 @@ \subsection{Partiality}\label{partiality} may be potentially non-terminating, all types in Haskell are assumed to be lifted. This is why we often talk about the category \textbf{Hask} of Haskell (lifted) types and functions rather than the simpler -\textbf{Set}. It is not clear, though, that \textbf{Hask} is a real +$\Set$. It is not clear, though, that \textbf{Hask} is a real category (see this \href{http://math.andrej.com/2016/08/06/hask-is-not-a-category/}{Andrej Bauer post}). diff --git a/src/content/3.6/Monads Categorically.tex b/src/content/3.6/Monads Categorically.tex index afce539c..841c3130 100644 --- a/src/content/3.6/Monads Categorically.tex +++ b/src/content/3.6/Monads Categorically.tex @@ -248,7 +248,7 @@ \section{Monoidal Categories}\label{monoidal-categories} \begin{Verbatim}[commandchars=\\\{\}] eta :: () -> m \end{Verbatim} -The singleton is the terminal object in \textbf{Set}, so it's natural to +The singleton is the terminal object in $\Set$, so it's natural to generalize this definition to any category that has a terminal object \code{t}: diff --git a/src/content/3.7/Comonads.tex b/src/content/3.7/Comonads.tex index 9df0a239..43dd8085 100644 --- a/src/content/3.7/Comonads.tex +++ b/src/content/3.7/Comonads.tex @@ -380,7 +380,7 @@ \section{Comonad Categorically}\label{comonad-categorically} split x = (x, x) \end{Verbatim} which shows that in Haskell (and, in general, in the category -\textbf{Set}) every object is a trivial comonoid. +$\Set$) every object is a trivial comonoid. Fortunately there are other more interesting monoidal categories in which to define comonoids. One of them is the category of endofunctors. diff --git a/src/content/3.8/F-Algebras.tex b/src/content/3.8/F-Algebras.tex index 9182a2d6..dc5ff810 100644 --- a/src/content/3.8/F-Algebras.tex +++ b/src/content/3.8/F-Algebras.tex @@ -9,7 +9,7 @@ μ :: m × m -> m η :: 1 -> m \end{Verbatim} -Here, 1 is the terminal object in \textbf{Set} --- the singleton set. +Here, 1 is the terminal object in $\Set$ --- the singleton set. The first function defines multiplication (it takes a pair of elements and returns their product), the second selects the unit element from \code{m}. Not every choice of two functions with these signatures @@ -34,7 +34,7 @@ \begin{Verbatim}[commandchars=\\\{\}] m \textsuperscript{m×m + 1} \end{Verbatim} -The plus sign stands for the coproduct in \textbf{Set}. We have just +The plus sign stands for the coproduct in $\Set$. We have just replaced a pair of functions with a single function --- an element of the set: @@ -204,7 +204,7 @@ \section{Recursion}\label{recursion} up with our \code{Expr}. Notice that \code{Expr} does not depend on \code{a}. The starting point of our journey doesn't matter, we always end up in the same place. This is not always true for an arbitrary -endofunctor in an arbitrary category, but in the category \textbf{Set} +endofunctor in an arbitrary category, but in the category $\Set$ things are nice. Of course, this is a hand-waving argument, and I'll make it more