update draft

_drafts/the-algebra-in-algebraic-datatypes.md

@@ -20,7 +20,7 @@ We shall make the following intepretation:
 
 * `a -> b`, the function type is interpteted as $b^a$.
 
-We will motivate this interpretation by considering the cardinality, or the number of elements of a type. For example, `()` has cardinality 1, and `Bool` has cardinality two. Now then, what is the cardinality of `Either a b`, given that `a` and `b` have cardinalities $n$ and $m$? Well, there are two ways of constructing a value of `Either a b`, `Left :: a -> Either a b` or `Right :: b -> Either a b`. We can construct $n$ elements using `Left`, since we have $n$ elements of `a`, and $m$ elements using right, as there are $m$ elements of `b`. Then in total we can construct $m + n$ elements of `Either a b`. Likewise we will see that in the case of `(a, b)` we will have $n$ choices for the first element, and then for each element of type `a` we will have another $m$ choices for the element of type `b`, yielding $n \cdot m$ elements in total. The function type being exponentiation might seem more archaic, but by defining equality of functions and using some basic combinatronics we can make perfect sense of it. If we consider two functions equal given that for every input they give the same output (a principle known as function extensionality) we will see that the way to enumerate the amount of elements of a function type is to enumerate how many different ways we can pick outputs for all our inputs. Consider then, any function `f :: a -> b` for each of the $n$ elements `αᵢ : a` we can choose $m$ different elements of `b` to send `f αⱼ` to. Thus we are making $n$ repeated choices of $m$ elements, yielding $m^n$ different options.
+We will motivate this interpretation by considering the cardinality, or the number of elements of a type. For example, `()` has cardinality 1, and `Bool` has cardinality two. Now then, what is the cardinality of `Either a b`, given that `a` and `b` have cardinalities $n$ and $m$? Well, there are two ways of constructing a value of `Either a b`, `Left :: a -> Either a b` or `Right :: b -> Either a b`. We can construct $n$ elements using `Left`, since we have $n$ elements of `a`, and $m$ elements using right, as there are $m$ elements of `b`. Then in total we can construct $m + n$ elements of `Either a b`. Likewise we will see that in the case of `(a, b)` we will have $n$ choices for the first element, and then for each element of type `a` we will have another $m$ choices for the element of type `b`, yielding $n \cdot m$ elements in total. The function type being exponentiation might seem more arcane, but by defining equality of functions and using some basic combinatronics we can make perfect sense of it. If we consider two functions equal given that for every input they give the same output (a principle known as function extensionality) we will see that the way to enumerate the amount of elements of a function type is to enumerate how many different ways we can pick outputs for all our inputs. Consider then, any function `f :: a -> b` for each of the $n$ elements `αᵢ : a` we can choose $m$ different elements of `b` to send `f αⱼ` to. Thus we are making $n$ repeated choices of $m$ elements, yielding $m^n$ different options.
 
 If we let `| a |` denote the cardinality of `a`, then we can write what we just learned quite succintly.
 
@@ -98,21 +98,42 @@ g = uncurry
 
 This time I shall be evil and leave finding the inverses as an exercise for you as well!
 
+# Categories
+
+In order to start formalising our notion of algebra in Haskell we will begin to view Haskell lens of category theory. Category theory is the studies of categories, which is defined to be the following
+
+* A collection of objects
+
+* For every ordered pair of objects a set of arrows from the first to the second object
+
+* For every object $a$ an arrow $id_a : a \to a$
+
+* A composition operation, denoted by $\circ$ such that if we have arrows $g : a \to b$ and $f : b \to c$ then there is another arrow $f \circ g : a \to c$
+
+Additionally, the follwing requirements are made
+
+* For any arrow $f : a \to b$ we have that $f \circ id_a = f$ and $id_b \circ f = f$
+* For three arrows $h : a \to b$, $g : b \to c$ and $f : a \to b$ we have that $f \circ (g \circ h) = (f \circ g) \circ h$
+
+Now of course this all seems very abstract, and it is. The strenght of category theory is how general it is, letting us make precise concepts such as sums and products which pop up all over math. In order to make category theory less abstract we will use Haskell as an example, since it's what we'll mainly be working with in this post.
+
 # Thinking with functions
-* What is a category?
-  * All about morphisms
+
+Now that we've unconvered some interesting algebraic properties of types in Haskell we'll begin viewing these from a category theoretic perspective, which will let us make these notions formal. In doing so we'll need to switch our perspective from types to functions, as category is all about arrows rather than objects.
+
+
 * Explain commuting diagrams somewhere here?
-  * Products
+* Products + Coproducts
 
 * Initial objects
 * Generalized elements
 
-Now that we've unconvered some interesting algebraic properties of types in Haskell we'll begin working our way towards category theory, which let's us make these notions formal. In doing so we'll need to switch our perspective from types to functions, as category is all about inspecting connections between things rather than the objects themselfs.
-
 We do however, of course, want to be able to talk about elements of types still, however we will do so using functions. An element of the type `a` will be modelled by a function of type `() -> a`, Using our cardinality view we can see this makes sense as `| () -> a | = | a | ^ | () | = | a | ^ 1 = | a |`.
 
+  * Products
   * Sums
   * Exponents
+  * Quick detour on limits
 
 # Functors in category theory
 * Functors
@@ -137,7 +158,18 @@ We do however, of course, want to be able to talk about elements of types still,
 # Writing foldr
 * Recovering `foldr`
 
-# ???
+# Co algebras and streams
+  
+# Caveats
+
+* Haskell pattern matching + recursion more general
+  * Bottom
+
+# Notes
+* Notation/Terminology
+  * Morphism instead of arrow
+  * Mjau?
+
 * Recommendations
   * Category theory for programmers
   * Ther are many category theory books
@@ -149,4 +181,8 @@ We do however, of course, want to be able to talk about elements of types still,
   * relate monoid example from before
   * multiplication given by composition instead of $\times$
   
+  
+
+* General recursion
+
 {% endkatexmm %}