From d80fc58aab38a5af024e33f91a492c908fea94e2 Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Wed, 3 Feb 2016 19:15:38 +0100
Subject: CatT 1.2.6

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

(limited to 'provider/posts')

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 b91cac4..19d71e4 100644
--- a/provider/posts/simmons-intro-to-cat-t/1.2.md
+++ b/provider/posts/simmons-intro-to-cat-t/1.2.md
@@ -91,7 +91,7 @@ We call the category comprised of such objects and arrows $\ca{RelH}$.
 </div>
 
 <div class="exercise">
-Topological spaces $(S, \mathcal{O}_S)$, where $S$ is a Set and $\mathcal{O}_S \subseteq \powerset(S)$, and continuous maps $f : S \to P$, that is $\forall V \in \mathcal{O}_T \ldotp f^\leftarrow(V) \in \mathcal{O}_S$, form a Category $\ca{Top}$.
+Topological spaces $(S, \mathcal{O}_S)$, where $S$ is a Set and $\mathcal{O}_S \subseteq \powerset{S}$, and continuous maps $f : S \to P$, that is $\forall V \in \mathcal{O}_T \ldotp f^\leftarrow(V) \in \mathcal{O}_S$, form a Category $\ca{Top}$.
 
  1. For every $(S, \mathcal{O}_S) \in \ca{Top}$ there exists $\idarr{(S, \mathcal{O}_S)}$
     <div class="proof">
@@ -123,3 +123,28 @@ We further define $m \circ m = m \ast m$.
 </div>
 </div>
 </div>
+
+<div class="exercise">
+Show that $\circ$ in $\ca{Pfn}$ is associative.
+
+<div class="proof">
+Consider the composition $g \circ f = \rest{g}{\bar{B}} \circ \rest{f}{\bar{\bar{A}}}$ of two partial functions $f : A \to B$ and $g : B \to C$:
+$$
+\begin{tikzcd}
+A \arrow[r, "f"] & B \arrow[r, "g"] & C \\
+\bar{A} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{A}}" description] & \bar{B} \arrow[u, hook] \arrow[ru, "\rest{g}{\bar{B}}" description] & \\
+\bar{\bar{A}} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{\bar{A}}}" description] & & \\
+\end{tikzcd}
+$$
+
+Extending the above to three partial functions $f : A \to B$, $g : B \to C$, and $h : C \to D$:
+$$
+\begin{aligned}
+(h \circ g) \circ f &= \rest{\left (\rest{h}{\bar{C}} \circ \rest{g}{\bar{\bar{B}}} \right )}{\bar{B}} \circ \rest{f}{\bar{\bar{A}}} \\
+&= \rest{h}{\bar{C}} \circ \rest{g}{\bar{\bar{B}}} \circ \rest{f}{\bar{\bar{A}}} \\
+&= \rest{h}{\bar{C}} \circ \rest{\left (\rest{g}{\bar{\bar{B}}} \circ \rest{f}{\bar{\bar{A}}} \right)}{\bar{\bar{A}}} \\
+&= h \circ (g \circ f)
+\end{aligned}
+$$
+</div>
+</div>
-- 
cgit v1.2.3