From fe3df38118b6ca97087bf07c68dc06a5f64288ee Mon Sep 17 00:00:00 2001 From: Rachel Lambda Samuelsson Date: Sun, 24 Dec 2023 22:44:40 +0100 Subject: [PATCH] update draft --- _drafts/the-algebra-in-algebraic-datatypes.md | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/_drafts/the-algebra-in-algebraic-datatypes.md b/_drafts/the-algebra-in-algebraic-datatypes.md index 6e7a9b8..e81ee29 100644 --- a/_drafts/the-algebra-in-algebraic-datatypes.md +++ b/_drafts/the-algebra-in-algebraic-datatypes.md @@ -118,11 +118,22 @@ Now of course this all seems very abstract, and it is. The strenght of category # Thinking with functions -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. +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 the individual types to functions between them, as category is all about arrows rather than objects. +In category theory we define many things using commuting diagrams, and products are no exception. In categary theory, the product of objects $$A$$ and $$B$$ is an object $$A \times B$$, with two arrows $$fst : A \times B \to A$$ and $$snd : A \times B \to B$$, and the requirment that for any C, and f, g, there is an arrow k, such that the following arrow commutes. + +{% details What is a commuting diagram %} +A commuting diagram is one in which all ways of walking from one point to another, composing functions along the way, are equal. In the diagram below this means that $$f = fst \circ k$$, and that $$g = snd \circ k$$. +{% enddetails %} + +{% cd Product diagram s:40 %} +& \ar[ddl, "f"'] C \ar[dd, dotted, "k"] \ar[ddr, "g"] & \\ +& & \\ +A & \ar[l, "fst"] A \times B \ar[r, "snd"'] & B +{% endcd %} -* Explain commuting diagrams somewhere here? * Products + Coproducts +* Explain commuting diagrams somewhere here? * Initial objects * Generalized elements