mirror of
https://github.com/hmemcpy/milewski-ctfp-pdf.git
synced 2024-11-25 07:52:03 +03:00
parent
8765d97d13
commit
d13765c717
@ -33,8 +33,8 @@ feature-flags.
|
|||||||
|
|
||||||
Afterwards, type `nix flake show` in the root directory of the project to see
|
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
|
all the available versions of this book. Then type `nix build .#<edition>` to
|
||||||
build the edition you want (Scala, OCaml, Reason and their printed
|
build the edition you want (Scala, OCaml, Reason and their printed versions).
|
||||||
versions). For example, to build the Scala edition you'll have to type
|
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-scala`. For Haskell (the original version) that is just
|
||||||
`nix build .#ctfp`.
|
`nix build .#ctfp`.
|
||||||
|
|
||||||
|
@ -63,7 +63,7 @@ the roadmap:
|
|||||||
Lawvere theory $\cat{L}$: an object in the category $\cat{Law}$.
|
Lawvere theory $\cat{L}$: an object in the category $\cat{Law}$.
|
||||||
\item
|
\item
|
||||||
Model $M$ of a Lawvere category: an object in the category\\
|
Model $M$ of a Lawvere category: an object in the category\\
|
||||||
$\cat{Mod}(\cat{Law}, \Set)$.
|
$\cat{Mod}(\cat{L}, \Set)$.
|
||||||
\end{enumerate}
|
\end{enumerate}
|
||||||
|
|
||||||
\begin{figure}[H]
|
\begin{figure}[H]
|
||||||
@ -352,7 +352,7 @@ $n$. We can implement $F$ as the representable functor:
|
|||||||
\[\cat{L}(n, -) \Colon \cat{L} \to \Set\]
|
\[\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
|
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:
|
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:
|
Let's simplify the right hand side:
|
||||||
\[\Set(n, U(M)) \cong \Set(n, M 1) \cong (M 1)^n \cong M n\]
|
\[\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
|
(I used the fact that a set of morphisms is isomorphic to the
|
||||||
|
Loading…
Reference in New Issue
Block a user