mirror of
https://github.com/hmemcpy/milewski-ctfp-pdf.git
synced 2024-11-29 16:37:17 +03:00
Final corrections (#162)
* Wow. Such corrections. 🐶
* Other corrections for Chapter 30.
* Update errata.
This commit is contained in:
parent
f9fd861fc9
commit
cbcd92807e
20
errata.md
20
errata.md
@ -8,6 +8,14 @@
|
|||||||
|
|
||||||
* [#157](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/157) - Adding paragraph indent
|
* [#157](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/157) - Adding paragraph indent
|
||||||
|
|
||||||
|
### 12. Limits and Colimits
|
||||||
|
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical error
|
||||||
|
|
||||||
|
### 14. Representable Functors
|
||||||
|
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical error
|
||||||
|
|
||||||
### 18. Adjunctions
|
### 18. Adjunctions
|
||||||
|
|
||||||
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix spelling of "counit"
|
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix spelling of "counit"
|
||||||
@ -20,6 +28,11 @@
|
|||||||
### 20. Monads - Programmer's Definition
|
### 20. Monads - Programmer's Definition
|
||||||
|
|
||||||
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix grammatical error
|
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix grammatical error
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical error
|
||||||
|
|
||||||
|
### 22. Monads Categorically
|
||||||
|
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical error
|
||||||
|
|
||||||
### 23. Comonads
|
### 23. Comonads
|
||||||
|
|
||||||
@ -30,6 +43,7 @@
|
|||||||
* [#158](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/158) - fixed incorrect typesetting of `set`
|
* [#158](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/158) - fixed incorrect typesetting of `set`
|
||||||
* [#159](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/159) - fixed incorrect typesetting of category terms
|
* [#159](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/159) - fixed incorrect typesetting of category terms
|
||||||
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix spelling of "counit" and "morphisms", fix subscript spacing
|
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix spelling of "counit" and "morphisms", fix subscript spacing
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical errors
|
||||||
|
|
||||||
### 26. Ends and Coends
|
### 26. Ends and Coends
|
||||||
|
|
||||||
@ -43,7 +57,13 @@
|
|||||||
### 28. Enriched Categories
|
### 28. Enriched Categories
|
||||||
|
|
||||||
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix subscript spacing
|
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix subscript spacing
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical error
|
||||||
|
|
||||||
|
### 29. Topoi
|
||||||
|
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical error
|
||||||
|
|
||||||
### 30. Lawvere Theories
|
### 30. Lawvere Theories
|
||||||
|
|
||||||
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix spelling of "coequalizer"
|
* [#160](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/160) - Fix spelling of "coequalizer"
|
||||||
|
* [#162](https://github.com/hmemcpy/milewski-ctfp-pdf/pull/162) - Fix grammatical errors and a typesetting error
|
||||||
|
@ -83,7 +83,7 @@ identities) in $\cat{2}$.
|
|||||||
A generalization of this construction to categories other than
|
A generalization of this construction to categories other than
|
||||||
$\cat{2}$ --- ones that, for instance, contain non-trivial morphisms
|
$\cat{2}$ --- ones that, for instance, contain non-trivial morphisms
|
||||||
--- will impose naturality conditions on the transformation between
|
--- will impose naturality conditions on the transformation between
|
||||||
$\Delta_c$ and $D$. We call such transformation a \emph{cone},
|
$\Delta_c$ and $D$. We call such a transformation a \emph{cone},
|
||||||
because the image of $\Delta$ is the apex of a cone/pyramid whose sides are
|
because the image of $\Delta$ is the apex of a cone/pyramid whose sides are
|
||||||
formed by the components of the natural transformation. The image of $D$
|
formed by the components of the natural transformation. The image of $D$
|
||||||
forms the base of the cone.
|
forms the base of the cone.
|
||||||
|
@ -139,7 +139,7 @@ $\cat{C}$ as sets and functions in $\Set$.
|
|||||||
The functor $\cat{C}(a, -)$ itself is sometimes called representable.
|
The functor $\cat{C}(a, -)$ itself is sometimes called representable.
|
||||||
More generally, any functor $F$ that is naturally isomorphic to
|
More generally, any functor $F$ that is naturally isomorphic to
|
||||||
the hom-functor, for some choice of $a$, is called
|
the hom-functor, for some choice of $a$, is called
|
||||||
\newterm{representable}. Such functor must necessarily be
|
\newterm{representable}. Such a functor must necessarily be
|
||||||
$\Set$-valued, since $\cat{C}(a, -)$ is.
|
$\Set$-valued, since $\cat{C}(a, -)$ is.
|
||||||
|
|
||||||
I said before that we often think of isomorphic sets as identical. More
|
I said before that we often think of isomorphic sets as identical. More
|
||||||
|
@ -299,7 +299,7 @@ preorder). The monoidal structure is given by addition, with zero
|
|||||||
serving as the unit object. In other words, the tensor product of two
|
serving as the unit object. In other words, the tensor product of two
|
||||||
numbers is their sum.
|
numbers is their sum.
|
||||||
|
|
||||||
A metric space is a category enriched over such monoidal category. A
|
A metric space is a category enriched over such a monoidal category. A
|
||||||
hom-object $\cat{C}(a, b)$ from object $a$ to $b$ is a
|
hom-object $\cat{C}(a, b)$ from object $a$ to $b$ is a
|
||||||
non-negative (possibly infinite) number that we will call the distance
|
non-negative (possibly infinite) number that we will call the distance
|
||||||
from $a$ to $b$. Let's see what we get for identity and
|
from $a$ to $b$. Let's see what we get for identity and
|
||||||
|
@ -9,7 +9,7 @@ of Haskell's type system with dependent types, or the exploration on
|
|||||||
homotopy type theory in programming.
|
homotopy type theory in programming.
|
||||||
|
|
||||||
So far I've been casually identifying types with \emph{sets} of values.
|
So far I've been casually identifying types with \emph{sets} of values.
|
||||||
This is not strictly correct, because such approach doesn't take into
|
This is not strictly correct, because such an approach doesn't take into
|
||||||
account the fact that, in programming, we \emph{compute} values, and the
|
account the fact that, in programming, we \emph{compute} values, and the
|
||||||
computation is a process that takes time and, in extreme cases, might
|
computation is a process that takes time and, in extreme cases, might
|
||||||
not terminate. Divergent computations are part of every Turing-complete
|
not terminate. Divergent computations are part of every Turing-complete
|
||||||
|
@ -139,7 +139,7 @@ $1 \times 1$ (or $1^2$) in $\cat{L}$. In this sense, the category
|
|||||||
$\cat{F}$ behaves like the logarithm of $\cat{L}$.
|
$\cat{F}$ behaves like the logarithm of $\cat{L}$.
|
||||||
|
|
||||||
Among morphisms in $\cat{L}$ we have those transferred by the functor
|
Among morphisms in $\cat{L}$ we have those transferred by the functor
|
||||||
$I_{\cat{L}}$ from $\cat{F}$. They play structural role in $\cat{L}$. In
|
$I_{\cat{L}}$ from $\cat{F}$. They play a structural role in $\cat{L}$. In
|
||||||
particular coproduct injections $i_k$ become product projections
|
particular coproduct injections $i_k$ become product projections
|
||||||
$p_k$. A useful intuition is to imagine the projection:
|
$p_k$. A useful intuition is to imagine the projection:
|
||||||
\[p_k \Colon 1^n \to 1\]
|
\[p_k \Colon 1^n \to 1\]
|
||||||
@ -219,7 +219,7 @@ The preservation of products by models means that the image of
|
|||||||
$M$ in $\Set$ is a sequence of sets generated by powers of
|
$M$ in $\Set$ is a sequence of sets generated by powers of
|
||||||
the set $M\ 1$ --- the image of the object $1$ from
|
the set $M\ 1$ --- the image of the object $1$ from
|
||||||
$\cat{L}$. Let's call this set $a$. (This set is sometimes
|
$\cat{L}$. Let's call this set $a$. (This set is sometimes
|
||||||
called a \emph{sort}, and such algebra is called \newterm{single-sorted}. There
|
called a \emph{sort}, and such an algebra is called \newterm{single-sorted}. There
|
||||||
exist generalizations of Lawvere theories to multi-sorted algebras.) In
|
exist generalizations of Lawvere theories to multi-sorted algebras.) In
|
||||||
particular, binary operations from $\cat{L}$ are mapped to functions:
|
particular, binary operations from $\cat{L}$ are mapped to functions:
|
||||||
\[a \times a \to a\]
|
\[a \times a \to a\]
|
||||||
@ -252,7 +252,7 @@ The functors that define models form a category of models,
|
|||||||
$\cat{Mod}(\cat{L}, \Set)$, with natural transformations as morphisms.
|
$\cat{Mod}(\cat{L}, \Set)$, with natural transformations as morphisms.
|
||||||
|
|
||||||
Consider a model for the trivial Lawvere category
|
Consider a model for the trivial Lawvere category
|
||||||
$\Fop$. Such model is completely determined by
|
$\Fop$. Such a model is completely determined by
|
||||||
its value at $1$, $M\ 1$. Since $M\ 1$ can be any
|
its value at $1$, $M\ 1$. Since $M\ 1$ can be any
|
||||||
set, there are as many of these models as there are sets in
|
set, there are as many of these models as there are sets in
|
||||||
$\Set$. Moreover, every morphism in $\cat{Mod}(\Fop, \Set)$ (a
|
$\Set$. Moreover, every morphism in $\cat{Mod}(\Fop, \Set)$ (a
|
||||||
@ -279,7 +279,7 @@ elegant construction.
|
|||||||
Every monoid must have a unit, so we have to have a special morphism
|
Every monoid must have a unit, so we have to have a special morphism
|
||||||
$\eta$ in $\cat{L}_{\cat{Mon}}$ that goes from $0$ to
|
$\eta$ in $\cat{L}_{\cat{Mon}}$ that goes from $0$ to
|
||||||
$1$. Notice that there can be no corresponding morphism in
|
$1$. Notice that there can be no corresponding morphism in
|
||||||
$\cat{F}$. Such morphism would go in the opposite direction, from
|
$\cat{F}$. Such a morphism would go in the opposite direction, from
|
||||||
$1$ to $0$ which, in $\cat{FinSet}$, would be a function
|
$1$ to $0$ which, in $\cat{FinSet}$, would be a function
|
||||||
from the singleton set to the empty set. No such function exists.
|
from the singleton set to the empty set. No such function exists.
|
||||||
|
|
||||||
@ -334,7 +334,7 @@ $\cat{L}$.
|
|||||||
Another way of deriving $U$ is by exploiting the fact that
|
Another way of deriving $U$ is by exploiting the fact that
|
||||||
$\Fop$ is the initial object in $\cat{Law}$. It
|
$\Fop$ is the initial object in $\cat{Law}$. It
|
||||||
means that, for any Lawvere theory $\cat{L}$, there is a unique
|
means that, for any Lawvere theory $\cat{L}$, there is a unique
|
||||||
functor $\Fop \to L$. This functor induces the
|
functor $\Fop \to \cat{L}$. This functor induces the
|
||||||
opposite functor on models (since models are functors \emph{from}
|
opposite functor on models (since models are functors \emph{from}
|
||||||
theories to sets):
|
theories to sets):
|
||||||
\[\cat{Mod}(\cat{L}, \Set) \to \cat{Mod}(\Fop, \Set)\]
|
\[\cat{Mod}(\cat{L}, \Set) \to \cat{Mod}(\Fop, \Set)\]
|
||||||
|
@ -85,7 +85,7 @@ We have previously arrived at the
|
|||||||
\hyperref[kleisli-categories]{writer
|
\hyperref[kleisli-categories]{writer
|
||||||
monad} by embellishing regular functions. The particular embellishment
|
monad} by embellishing regular functions. The particular embellishment
|
||||||
was done by pairing their return values with strings or, more generally,
|
was done by pairing their return values with strings or, more generally,
|
||||||
with elements of a monoid. We can now recognize that such embellishment
|
with elements of a monoid. We can now recognize that such an embellishment
|
||||||
is a functor:
|
is a functor:
|
||||||
|
|
||||||
\src{code/haskell/snippet02.hs}
|
\src{code/haskell/snippet02.hs}
|
||||||
|
@ -524,7 +524,7 @@ This is indeed the implementation of \code{join} for the
|
|||||||
|
|
||||||
It turns out that not only every adjunction gives rise to a monad, but
|
It turns out that not only every adjunction gives rise to a monad, but
|
||||||
the converse is also true: every monad can be factorized into a
|
the converse is also true: every monad can be factorized into a
|
||||||
composition of two adjoint functors. Such factorization is not unique
|
composition of two adjoint functors. Such a factorization is not unique
|
||||||
though.
|
though.
|
||||||
|
|
||||||
We'll talk about the other endofunctor $L \circ R$ in the next
|
We'll talk about the other endofunctor $L \circ R$ in the next
|
||||||
|
@ -15,7 +15,7 @@ every adjunction \hyperref[monads-categorically]{defines
|
|||||||
a monad} (and a comonad). The question is: Can every monad (comonad) be
|
a monad} (and a comonad). The question is: Can every monad (comonad) be
|
||||||
derived from an adjunction? The answer is positive. There is a whole
|
derived from an adjunction? The answer is positive. There is a whole
|
||||||
family of adjunctions that generate a given monad. I'll show you two
|
family of adjunctions that generate a given monad. I'll show you two
|
||||||
such adjunction.
|
such adjunctions.
|
||||||
Let's review the definitions. A monad is an endofunctor $m$
|
Let's review the definitions. A monad is an endofunctor $m$
|
||||||
equipped with two natural transformations that satisfy some coherence
|
equipped with two natural transformations that satisfy some coherence
|
||||||
conditions. The components of these transformations at $a$ are:
|
conditions. The components of these transformations at $a$ are:
|
||||||
@ -165,7 +165,7 @@ the pair $(T\ a, \mu_a)$. So in order to define the component of
|
|||||||
the counit $\varepsilon$ at $(a, f)$, we need the right morphism in
|
the counit $\varepsilon$ at $(a, f)$, we need the right morphism in
|
||||||
the Eilenberg-Moore category, or a homomorphism of T-algebras:
|
the Eilenberg-Moore category, or a homomorphism of T-algebras:
|
||||||
\[(T\ a, \mu_a) \to (a, f)\]
|
\[(T\ a, \mu_a) \to (a, f)\]
|
||||||
Such homomorphism should map the carrier $T\ a$ to $a$.
|
Such a homomorphism should map the carrier $T\ a$ to $a$.
|
||||||
Let's just resurrect the forgotten evaluator $f$. This time we'll
|
Let's just resurrect the forgotten evaluator $f$. This time we'll
|
||||||
use it as a homomorphism of T-algebras. Indeed, the same commuting
|
use it as a homomorphism of T-algebras. Indeed, the same commuting
|
||||||
diagram that makes $f$ a T-algebra may be re-interpreted to show
|
diagram that makes $f$ a T-algebra may be re-interpreted to show
|
||||||
|
Loading…
Reference in New Issue
Block a user