summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2016-02-03 21:33:51 +0100
committerGregor Kleen <gkleen@yggdrasil.li>2016-02-03 21:33:51 +0100
commit5553a3223d07f73955465952d7765d47d3558d7b (patch)
tree53c3ae50c85cdc7c45ae12817a9728de29ba0e47
parent7f1293b7afa7574d93c07fd34dc472bb0979a98f (diff)
downloaddirty-haskell.org-5553a3223d07f73955465952d7765d47d3558d7b.tar
dirty-haskell.org-5553a3223d07f73955465952d7765d47d3558d7b.tar.gz
dirty-haskell.org-5553a3223d07f73955465952d7765d47d3558d7b.tar.bz2
dirty-haskell.org-5553a3223d07f73955465952d7765d47d3558d7b.tar.xz
dirty-haskell.org-5553a3223d07f73955465952d7765d47d3558d7b.zip
CatT 1.2.8
-rw-r--r--provider/posts/simmons-intro-to-cat-t/1.2.md18
1 files changed, 18 insertions, 0 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 faaf429..30d0492 100644
--- a/provider/posts/simmons-intro-to-cat-t/1.2.md
+++ b/provider/posts/simmons-intro-to-cat-t/1.2.md
@@ -181,3 +181,21 @@ where $\rest{f}{\bar{A}}$ is total.
181</div> 181</div>
182</div> 182</div>
183 183
184<div class="exercise">
185Verify that for every monoid $R$ both $R\ca{Set}$ and $\ca{Set}R$ are categories of structured sets.
186
187<div class="proof">
188Since the two proofs are perfectly analogous we cover only the case $R\ca{Set}$.
189
190 1. For every $R$-Set $A \in R\ca{Set}$ there exists $\idarr{A}$
191
192 $\id$ on $A$ is indeed a structure preserving function ($\forall a \in A, r \in R \ldotp \id(ra) = ra = r \id(a)$).
193
194 2. There exists an associative partial binary operation $\circ$ on the arrows of $R\ca{Set}$
195
196 Given three R-Sets $A$, $B$, and $C$ and two continuous maps $g : A \to B$ and $f : B \to C$ the map $f \circ g : A \to C$ is an arrow in $R\ca{Set}$, that is to say $\forall a \in A, r \in R$:
197 $$(f \circ g)(ra) = f(r g(a)) = r (f \circ g)(a)$$
198
199The format of the proof was chosen to demonstrate that $R\ca{Set}$ is indeed a structured set.
200</div>
201</div>