summaryrefslogtreecommitdiff
path: root/provider
diff options
context:
space:
mode:
Diffstat (limited to 'provider')
-rw-r--r--provider/posts/simmons-intro-to-cat-t/1.2.md5
1 files changed, 4 insertions, 1 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 c714f81..e180c6d 100644
--- a/provider/posts/simmons-intro-to-cat-t/1.2.md
+++ b/provider/posts/simmons-intro-to-cat-t/1.2.md
@@ -136,6 +136,7 @@ A \arrow[r, "f"] & B \arrow[r, "g"] & C \\
136\bar{\bar{A}} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{\bar{A}}}" description] & & \\ 136\bar{\bar{A}} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{\bar{A}}}" description] & & \\
137\end{tikzcd} 137\end{tikzcd}
138$$ 138$$
139where all restricted versions of $f$, $g$, and $h$ are total.
139 140
140Extending the above to three partial functions $f : A \to B$, $g : B \to C$, and $h : C \to D$: 141Extending the above to three partial functions $f : A \to B$, $g : B \to C$, and $h : C \to D$:
141$$ 142$$
@@ -160,7 +161,7 @@ $$
160\begin{aligned} 161\begin{aligned}
161\Phi : \ca{Pfn} & \to \ca{Set_\bot} \\ 162\Phi : \ca{Pfn} & \to \ca{Set_\bot} \\
162A & \mapsto A \cup \{ \bot_A \} \\ 163A & \mapsto A \cup \{ \bot_A \} \\
163\begin{tikzcd} 164f\ \text{s.t.} \begin{tikzcd}
164A \arrow[r, "f"] & B \\ 165A \arrow[r, "f"] & B \\
165\bar{A} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{A}}" description] & 166\bar{A} \arrow[u, hook] \arrow[ru, "\rest{f}{\bar{A}}" description] &
166\end{tikzcd} & \mapsto \begin{aligned} 167\end{tikzcd} & \mapsto \begin{aligned}
@@ -176,5 +177,7 @@ A & \mapsto A - \{ \bot \} \\
176f & \mapsto \rest{f}{\left ( A - \{ \bot \} \right )} 177f & \mapsto \rest{f}{\left ( A - \{ \bot \} \right )}
177\end{aligned} 178\end{aligned}
178$$ 179$$
180where $\rest{f}{\bar{A}}$ is total.
179</div> 181</div>
180</div> 182</div>
183