From 9deed79e33b9380ca90fbf3f2a64234f4e17945f Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Wed, 3 Feb 2016 20:23:16 +0100
Subject: CatT 1.2.7

---
 provider/posts/simmons-intro-to-cat-t/1.2.md | 30 ++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

(limited to 'provider')

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 @@ $$
 $$
 </div>
 </div>
+
+<div class="exercise">
+Consider the category $\ca{Set_\bot}$ of pointed sets.
+
+Show that $\ca{Set_\bot}$ and $\ca{Pfn}$ are "essentially the same" category.
+
+<div class="proof">
+The idea is to identify the undefined parts of a partial functions image with $\bot$:
+$$
+\begin{aligned}
+\Phi : \ca{Pfn} & \to \ca{Set_\bot} \\
+A & \mapsto A \cup \{ \bot_A \} \\
+\begin{tikzcd}
+A \arrow[r, "f"] & B \\
+\bar{A} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{A}}" description] & 
+\end{tikzcd} & \mapsto \begin{aligned}
+\Phi(f) : A \cup \{ \bot_A \} & \to B \cup \{ \bot_B \} \\
+\bot_A & \mapsto \bot_B \\
+a & \mapsto \begin{cases}
+f(a) & \quad x \in \bar{A} \\
+\bot & \quad \text{else}
+\end{cases}
+\end{aligned} \\
+\Phi^\leftarrow : \ca{Set_\bot} & \to \ca{Pfn} \\
+A & \mapsto A - \{ \bot \} \\
+f & \mapsto \rest{f}{\left ( A - \{ \bot \} \right )}
+\end{aligned}
+$$
+</div>
+</div>
-- 
cgit v1.2.3