CatT 1.2.6

2 files changed, 31 insertions, 5 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 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>
diff --git a/provider/templates/preamble.tex b/provider/templates/preamble.tex
index 1f2c1e4..541b415 100644
--- a/provider/templates/preamble.tex
+++ b/provider/templates/preamble.tex
@@ -8,15 +8,16 @@
 
 \usetikzlibrary{cd}
 
-\newcommand*{\ca}[1]{\ensuremath{\mathbf{#1}}}
-\newcommand*{\idarr}[1]{\ensuremath{\mathrm{id}_{#1}}}
-
 \newcommand*{\id}{\ensuremath{\mathrm{id}}}
 \renewcommand{\implies}{\ensuremath{\rightarrow}}
 
 \newcommand*{\N}{\ensuremath{\mathbb{N}}}
+\newcommand*{\powerset}[1]{\raisebox{.15\baselineskip}{\Large\ensuremath{\wp}} \left ( #1 \right )}
+
+\newcommand*{\ca}[1]{\ensuremath{\mathbf{#1}}}
+\newcommand*{\idarr}[1]{\ensuremath{\mathrm{id}_{#1}}}
 \newcommand*{\arr}[3]{\begin{tikzcd}[ampersand replacement=\&]{#1} \rar{#2} \& {#3}\end{tikzcd}}
 \newcommand*{\Hom}[3]{\ensuremath{\mathrm{Hom}_{#1} \left [ #2, #3 \right ]}}
 \newcommand*{\End}[2]{\ensuremath{\mathrm{End}_{#1} \left [ #2 \right ]}}
 
-\newcommand*{\powerset}{\raisebox{.15\baselineskip}{\Large\ensuremath{\wp}}}
+\newcommand*{\rest}[2]{\ensuremath{#1 \upharpoonright #2}}