summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGregor Kleen <gkleen@yggdrasil.li>2016-01-29 18:49:11 +0100
committerGregor Kleen <gkleen@yggdrasil.li>2016-01-29 18:49:11 +0100
commit60b2206e179317f9576fc9e89031ba9fd3892ec6 (patch)
tree7528207d3875c9a125c7f10560a12aacd02e83fa
parentfb55acfc7ce4bf2eebeff72e86fe7cedac7c55b1 (diff)
downloaddirty-haskell.org-60b2206e179317f9576fc9e89031ba9fd3892ec6.tar
dirty-haskell.org-60b2206e179317f9576fc9e89031ba9fd3892ec6.tar.gz
dirty-haskell.org-60b2206e179317f9576fc9e89031ba9fd3892ec6.tar.bz2
dirty-haskell.org-60b2206e179317f9576fc9e89031ba9fd3892ec6.tar.xz
dirty-haskell.org-60b2206e179317f9576fc9e89031ba9fd3892ec6.zip
Simmons 1.1
-rw-r--r--provider/posts/simmons-intro-to-cat-t/1.1.md38
1 files changed, 38 insertions, 0 deletions
diff --git a/provider/posts/simmons-intro-to-cat-t/1.1.md b/provider/posts/simmons-intro-to-cat-t/1.1.md
new file mode 100644
index 0000000..41aef99
--- /dev/null
+++ b/provider/posts/simmons-intro-to-cat-t/1.1.md
@@ -0,0 +1,38 @@
1---
2title: Exercises in Category Theory — 1.1
3published: 2016-01-29
4tags: Category Theory
5---
6
7<div class="corollary">
8Sets and functions do form a category $\ca{Set}$.
9
10<div class="proof">
11The objects of $\ca{Set}$ are sets and its arrows are functions.
12
13For any set $A$ we construct $id_A$ by restricting $id$ to $A$:
14$$id_A = id \upharpoonright A$$
15
16$\circ$ is indeed associative.
17</div>
18</div>
19
20<div class="corollary">
21Each [poset](https://en.wikipedia.org/wiki/Partially_ordered_set) is a category.
22
23<div class="proof">
24The objects of each poset are its elements and we construct an arrow $\leq: a \to b$ for every pair of objects $(a, b)$ iff $a \leq b$.
25
26Reflexivity ($a \leq a$) and transitivity ($a \leq b \land b \leq c \implies a \leq c$) provide a construction for $id_a$ and $\circ$, respectively.
27</div>
28</div>
29
30<div class="corollary">
31Each [monoid](https://en.wikipedia.org/wiki/Monoid) is a category.
32
33<div class="proof">
34The objects of each monoid are its elements and we construct for every pair of elements $(a, b)$ an arrow $\cdot b : a \to a \cdot b$.
35
36The existence of an identity element and associativity, as required by the monoid structure, immediately provide us with a construction for $id$ and associativity of $\circ$.
37</div>
38</div>