mirror of
https://github.com/hmemcpy/milewski-ctfp-pdf.git
synced 2024-11-22 11:32:00 +03:00
Compare commits
8 Commits
7a47ac107d
...
065a6dd76b
Author | SHA1 | Date | |
---|---|---|---|
|
065a6dd76b | ||
|
1bd3e36e5a | ||
|
d13765c717 | ||
|
8765d97d13 | ||
|
f6b98020e9 | ||
|
c46c3669d4 | ||
|
42a1a120b0 | ||
|
702e284dd4 |
2
.github/workflows/release.yaml
vendored
2
.github/workflows/release.yaml
vendored
@ -80,7 +80,7 @@ jobs:
|
||||
|
||||
steps:
|
||||
- name: Download build assets (${{ matrix.packages }}.pdf)
|
||||
uses: actions/download-artifact@v2
|
||||
uses: actions/download-artifact@v4.1.7
|
||||
with:
|
||||
name: ctfp
|
||||
path: ctfp
|
||||
|
@ -33,9 +33,10 @@ feature-flags.
|
||||
|
||||
Afterwards, type `nix flake show` in the root directory of the project to see
|
||||
all the available versions of this book. Then type `nix build .#<edition>` to
|
||||
build the edition you want (Haskell, Scala, OCaml, Reason and their printed
|
||||
versions). For example, to build the Scala edition you'll have to type
|
||||
`nix build .#ctfp-scala`.
|
||||
build the edition you want (Scala, OCaml, Reason and their printed versions).
|
||||
For example, to build the Scala edition you'll have to type
|
||||
`nix build .#ctfp-scala`. For Haskell (the original version) that is just
|
||||
`nix build .#ctfp`.
|
||||
|
||||
Upon successful compilation, the PDF file will be placed in the `result`
|
||||
directory.
|
||||
|
@ -1,3 +1 @@
|
||||
trait Coend[P[_, _]] {
|
||||
def paa[A]: P[A, A]
|
||||
}
|
||||
trait Coend[P[_, _]] { type A; val p: P[A, A] }
|
||||
|
@ -336,13 +336,13 @@ the end:
|
||||
We can use the product-exponential adjunction:
|
||||
\[\int_a \int_i \Set(\cat{A}(K i, a),\ (F' a)^{D i})\]
|
||||
The exponential is isomorphic to the corresponding hom-set:
|
||||
\[\int_a \int_i \Set(\cat{A}(K i, a),\ \cat{A}(D i, F' a))\]
|
||||
\[\int_a \int_i \Set(\cat{A}(K i, a),\ \Set(D i, F' a))\]
|
||||
There is a theorem called the Fubini theorem that allows us to swap the
|
||||
two ends:
|
||||
\[\int_i \int_a \Set(\cat{A}(K i, a),\ A(D i, F' a))\]
|
||||
\[\int_i \int_a \Set(\cat{A}(K i, a),\ \Set(D i, F' a))\]
|
||||
The inner end represents the set of natural transformations between two
|
||||
functors, so we can use the Yoneda lemma:
|
||||
\[\int_i \cat{A}(D i, F' (K i))\]
|
||||
\[\int_i \Set(D i, F' (K i))\]
|
||||
This is indeed the set of natural transformations that forms the right
|
||||
hand side of the adjunction we set out to prove:
|
||||
\[[\cat{I}, \Set](D, F' \circ K)\]
|
||||
|
@ -63,7 +63,7 @@ the roadmap:
|
||||
Lawvere theory $\cat{L}$: an object in the category $\cat{Law}$.
|
||||
\item
|
||||
Model $M$ of a Lawvere category: an object in the category\\
|
||||
$\cat{Mod}(\cat{Law}, \Set)$.
|
||||
$\cat{Mod}(\cat{L}, \Set)$.
|
||||
\end{enumerate}
|
||||
|
||||
\begin{figure}[H]
|
||||
@ -352,7 +352,7 @@ $n$. We can implement $F$ as the representable functor:
|
||||
\[\cat{L}(n, -) \Colon \cat{L} \to \Set\]
|
||||
To show that it's indeed free, all we have to do is to prove that it's a
|
||||
left adjoint to the forgetful functor:
|
||||
\[\cat{Mod}(\cat{L}(n, -), M) \cong \Set(n, U(M))\]
|
||||
\[\cat{Mod}(\cat{L}, \Set)(\cat{L}(n, -), M) \cong \Set(n, U(M))\]
|
||||
Let's simplify the right hand side:
|
||||
\[\Set(n, U(M)) \cong \Set(n, M 1) \cong (M 1)^n \cong M n\]
|
||||
(I used the fact that a set of morphisms is isomorphic to the
|
||||
|
@ -157,7 +157,7 @@ diagrams commute:
|
||||
\centering
|
||||
\begin{tikzcd}[column sep=large, row sep=large]
|
||||
L \arrow[rd, equal] \arrow[r, "L \circ \eta"]
|
||||
& L \circ R \circ L \arrow[d, "\epsilon \circ L"] \\
|
||||
& L \circ R \circ L \arrow[d, "\varepsilon \circ L"] \\
|
||||
& L
|
||||
\end{tikzcd}
|
||||
\end{subfigure}%
|
||||
@ -166,7 +166,7 @@ diagrams commute:
|
||||
\centering
|
||||
\begin{tikzcd}[column sep=large, row sep=large]
|
||||
R \arrow[rd, equal] \arrow[r, "\eta \circ R"]
|
||||
& R \circ L \circ R \arrow[d, "R \circ \epsilon"] \\
|
||||
& R \circ L \circ R \arrow[d, "R \circ \varepsilon"] \\
|
||||
& R
|
||||
\end{tikzcd}
|
||||
\end{subfigure}
|
||||
|
@ -330,7 +330,7 @@ with a comonad. They make the following diagrams commute:
|
||||
\centering
|
||||
\begin{tikzcd}[column sep=large, row sep=large]
|
||||
a \arrow[rd, equal]
|
||||
& Wa \arrow[l, "\epsilon_a"'] \\
|
||||
& Wa \arrow[l, "\varepsilon_a"'] \\
|
||||
& a \arrow[u, "\mathit{coa}"']
|
||||
\end{tikzcd}
|
||||
\end{subfigure}%
|
||||
|
Loading…
Reference in New Issue
Block a user