summaryrefslogtreecommitdiff
path: root/provider
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2016-02-03 20:23:16 +0100
committerGregor Kleen <gkleen@yggdrasil.li>2016-02-03 20:23:16 +0100
commit9deed79e33b9380ca90fbf3f2a64234f4e17945f (patch)
tree9cbc7594b626799c4d1ee3022c33b5102c8de0f6 /provider
parentd80fc58aab38a5af024e33f91a492c908fea94e2 (diff)
downloaddirty-haskell.org-9deed79e33b9380ca90fbf3f2a64234f4e17945f.tar
dirty-haskell.org-9deed79e33b9380ca90fbf3f2a64234f4e17945f.tar.gz
dirty-haskell.org-9deed79e33b9380ca90fbf3f2a64234f4e17945f.tar.bz2
dirty-haskell.org-9deed79e33b9380ca90fbf3f2a64234f4e17945f.tar.xz
dirty-haskell.org-9deed79e33b9380ca90fbf3f2a64234f4e17945f.zip
CatT 1.2.7
Diffstat (limited to 'provider')
-rw-r--r--provider/posts/simmons-intro-to-cat-t/1.2.md30
1 files changed, 30 insertions, 0 deletions
diff --git a/provider/posts/simmons-intro-to-cat-t/1.2.md b/provider/posts/simmons-intro-to-cat-t/1.2.md
index 19d71e4..c714f81 100644
--- a/provider/posts/simmons-intro-to-cat-t/1.2.md
+++ b/provider/posts/simmons-intro-to-cat-t/1.2.md
@@ -148,3 +148,33 @@ $$
148$$ 148$$
149</div> 149</div>
150</div> 150</div>
151
152<div class="exercise">
153Consider the category $\ca{Set_\bot}$ of pointed sets.
154
155Show that $\ca{Set_\bot}$ and $\ca{Pfn}$ are "essentially the same" category.
156
157<div class="proof">
158The idea is to identify the undefined parts of a partial functions image with $\bot$:
159$$
160\begin{aligned}
161\Phi : \ca{Pfn} & \to \ca{Set_\bot} \\
162A & \mapsto A \cup \{ \bot_A \} \\
163\begin{tikzcd}
164A \arrow[r, "f"] & B \\
165\bar{A} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{A}}" description] &
166\end{tikzcd} & \mapsto \begin{aligned}
167\Phi(f) : A \cup \{ \bot_A \} & \to B \cup \{ \bot_B \} \\
168\bot_A & \mapsto \bot_B \\
169a & \mapsto \begin{cases}
170f(a) & \quad x \in \bar{A} \\
171\bot & \quad \text{else}
172\end{cases}
173\end{aligned} \\
174\Phi^\leftarrow : \ca{Set_\bot} & \to \ca{Pfn} \\
175A & \mapsto A - \{ \bot \} \\
176f & \mapsto \rest{f}{\left ( A - \{ \bot \} \right )}
177\end{aligned}
178$$
179</div>
180</div>