diff options
Diffstat (limited to 'provider')
| -rw-r--r-- | provider/posts/simmons-intro-to-cat-t/1.2.md | 5 |
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 | $$ |
| 139 | where all restricted versions of $f$, $g$, and $h$ are total. | ||
| 139 | 140 | ||
| 140 | Extending the above to three partial functions $f : A \to B$, $g : B \to C$, and $h : C \to D$: | 141 | Extending 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} \\ |
| 162 | A & \mapsto A \cup \{ \bot_A \} \\ | 163 | A & \mapsto A \cup \{ \bot_A \} \\ |
| 163 | \begin{tikzcd} | 164 | f\ \text{s.t.} \begin{tikzcd} |
| 164 | A \arrow[r, "f"] & B \\ | 165 | A \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 \} \\ | |||
| 176 | f & \mapsto \rest{f}{\left ( A - \{ \bot \} \right )} | 177 | f & \mapsto \rest{f}{\left ( A - \{ \bot \} \right )} |
| 177 | \end{aligned} | 178 | \end{aligned} |
| 178 | $$ | 179 | $$ |
| 180 | where $\rest{f}{\bar{A}}$ is total. | ||
| 179 | </div> | 181 | </div> |
| 180 | </div> | 182 | </div> |
| 183 | |||
