Reset repository to leave only Milewski notes. History of the old repo can be seen in file HISTORY

4 years ago · 2440e19905
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1,7 @@

 # files marked for deletion
 z.*

 share

 TODO
--- a/+ 55
+++ b/+ 55
@@ -0,0 +1,55 @@


 This contains the history of the initial repository
 Re-initialized the repo to remove heavy files and supplementary content about categories.


 * b9e1091 - (2019-01-27 22:07:00 +0100) Remove all content different from Milewski notes - Thierry (HEAD -> master, origin/master)
 * 6f18b62 - (2018-12-09 16:58:15 +0100) Début notes conférence Laurent Lafforgue sur la notion de vérité selon Grothendieck - Thierry (larzac/master)
 * 14cd705 - (2018-11-27 11:11:58 +0100) Typos on topo sur les topos - Thierry
 * 314abef - (2018-11-27 10:51:17 +0100) Small tweaks - Thierry
 * 23ebbfb - (2018-11-17 23:55:45 +0100) Clean CSS, format Milewski until 2.1 - Thierry
 * ec7164e - (2018-11-17 10:21:26 +0100) Notes from Connes -un topo sur les topos - Thierry
 * c36c8d5 - (2018-11-10 17:08:21 +0100) Modify tags and style for navigation + integration to tig12.net - Thierry
 * 5f6a4bd - (2018-10-22 01:57:15 +0200) Begin Caramello, Introduction to categorical logic - Thierry
 * 4971eb0 - (2018-10-08 09:36:49 +0200) French course, intro categories - Thierry
 * da21e81 - (2018-09-22 18:36:33 +0200) Prepare caramello, complete milewski part III list, corrections on milewski part I - Thierry
 * c5f4447 - (2018-08-09 19:29:39 +0200) Restructure directories ; prepare french course - Thierry
 * 1cf4add - (2018-08-01 15:04:04 +0200) Modify index.html and README - Thierry
 * 7a2fd43 - (2018-07-30 17:56:34 +0200) Add README - Thierry
 * 5194c43 - (2018-07-30 02:12:57 +0200) Format 2.1 and 2.2 - Thierry
 * 9f7bab1 - (2018-06-15 02:17:05 +0200) Continue 7.2 - Thierry
 * ab48c36 - (2018-06-14 08:50:25 +0200) Continue 7.2 - Thierry
 * c84ab5e - (2018-06-06 00:24:00 +0200) Start 7.2: Monoidal Categories, Functoriality of ADTs, Profunctors - Thierry
 * 2c26946 - (2018-06-05 09:52:03 +0200) End 7.1 - Thierry
 * cb36f11 - (2018-06-04 14:09:48 +0200) Continue 7.1 - Thierry
 * aacf03f - (2018-06-02 19:37:48 +0200) Start 7.1: Functoriality, bifunctors - Thierry
 * b4d24f2 - (2018-06-02 18:02:47 +0200) End 6.2 - Thierry
 * 15a3ec7 - (2018-06-01 21:14:25 +0200) Continue 6.2 - Thierry
 * 96ed4a3 - (2018-05-31 21:00:07 +0200) End 6.1, begin 6.2: Functors in programming - Thierry
 * 48a642a - (2018-05-31 08:20:58 +0200) Begin 6.1 - Functors - Thierry
 * 5def260 - (2018-05-30 03:57:39 +0200) Format code and fix typos - Thierry
 * c7feffa - (2018-05-29 21:23:00 +0200) Format code - Thierry
 * c8f42df - (2018-05-29 17:18:17 +0200) Fix typos - Thierry
 * a331619 - (2018-05-29 15:13:44 +0200) 5.2: Algebraic data types - Thierry
 * 8c24c85 - (2018-05-29 12:08:00 +0200) 5.1: Coproducts, sum types - Thierry
 * 6b8f353 - (2018-05-29 09:07:44 +0200) End 4.2 - Thierry
 * 91f9de8 - (2018-05-28 17:03:07 +0200) Start 4.2 : Products - Thierry
 * 322d285 - (2018-05-28 12:00:57 +0200) End 4.1 - Thierry
 * 02fe188 - (2018-05-26 02:27:59 +0200) Adapt index - Thierry
 * e1b35fd - (2018-05-26 01:51:06 +0200) Change repository name - Thierry
 * fb21cec - (2018-05-26 01:48:26 +0200) Corections to 3.2 Kleisli - Thierry
 * 9995419 - (2018-05-24 17:32:02 +0200) Begin 4.1: Terminal and initial objects - Thierry
 * 7ba2a7e - (2018-05-24 12:44:30 +0200) Refactor index - Thierry
 * cdab767 - (2018-05-24 12:13:02 +0200) Add navigation between pages, prepare following pages - Thierry
 * e9bd396 - (2018-05-23 22:10:27 +0200) End 3.2 - Thierry
 * 39e849e - (2018-05-23 12:04:06 +0200) Begin 3.2 : Kleisli category - Thierry
 * 6c8a965 - (2018-05-23 09:00:59 +0200) End 3.1 - Thierry
 * 9556c4a - (2018-05-23 00:13:35 +0200) Continue 3.1 - Thierry
 * bc4ada8 - (2018-05-21 23:36:12 +0200) Begin 3.1 : Examples of categories, orders, monoids - Thierry
 * 4701a0c - (2018-05-21 09:07:37 +0200) 2.2 Monomorphisms, simple types - Thierry
 * 6f412fa - (2018-05-20 23:32:05 +0200) End 2.1 - Thierry
 * ad3144a - (2018-05-19 23:22:26 +0200) Continue 2.1 - Thierry
 * bad8438 - (2018-05-18 09:26:36 +0200) Continue 2.1 - Thierry
 * 24c9857 - (2018-05-18 00:24:32 +0200) Begin 2.1 functions, epimorphisms - Thierry
 * 47bcbed - (2018-05-17 15:18:13 +0200) Initial commit, en/1.1 and 1.2 - Thierry
--- a/+ 4
+++ b/+ 4
@@ -0,0 +1,4 @@

 These are notes and screenshots of video courses on categories published by Bartosz Milewski on youtube.
 See index.html for links to the original resources.

--- a/index.html
+++ b/index.html
@@ -0,0 +1,177 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body class="index">                                                                         

 <nav class="prevnext">
    <a class="top" title="Index" href="../categories.html">&uarr;</a>
    <a class="next" title="Next" href="younotes1/1.1-motivation-philosophy.html">&rarr;</a>
 </nav>

 <h1>Category Theory for programmers</h1>

 <h2>Notes and screenshots from Bartosz Milewski's youtube videos</h2>
 <div style="float:left;">
 <h2>Part I</h2>
 <ul>
    <li>
        <b><a href="younotes1/1.1-motivation-philosophy.html">I-1.1: Motivation and Philosophy</a></b> - 46:46
    </li>
    <li>
        <b><a href="younotes1/1.2-what-is-a-category.html">I-1.2: What is a category?</a></b> - 48:18
    </li>
    <li>
        <b><a href="younotes1/2.1-functions-epimorphisms.html">I-2.1: Functions, epimorphisms</a></b> - 46:14
    </li>
    <li>
        <b><a href="younotes1/2.2-monomorphisms-simple-types.html">I-2.2: Monomorphisms, simple types</a></b> - 24:34
    </li>
    <li>
        <b><a href="younotes1/3.1-examples-orders-monoids.html">I-3.1: Examples of categories, orders, monoids</a></b> - 48:26
    </li>
    <li>
        <b><a href="younotes1/3.2-kleisli-category.html">I-3.2: Kleisli category</a></b> - 41:58
    </li>
    <li>
        <b><a href="younotes1/4.1-terminal-and-initial-objects.html">I-4.1: Terminal and initial objects</a></b> - 47:47
    </li>
    <li>
        <b><a href="younotes1/4.2-products.html">I-4.2: Products</a></b> - 34:49
    </li>
    <li>
        <b><a href="younotes1/5.1-coproducts-sum-types.html">I-5.1: Coproducts, sum types</a></b> - 36:47
    </li>
    <li>
        <b><a href="younotes1/5.2-algebraic-data-types.html">I-5.2: Algebraic data types</a></b> - 33:14
    </li>
    <li>
        <b><a href="younotes1/6.1-functors.html">I-6.1: Functors</a></b> - 54:10
    </li>
    <li>
        <b><a href="younotes1/6.2-functors-in-programming.html">I-6.2: Functors in programming</a></b> - 51:36
    </li>
    <li>
        <b><a href="younotes1/7.1-functoriality-bifunctors.html">I-7.1: Functoriality, bifunctors</a></b> - 56:32
    </li>
    <li>
        <b><a href="younotes1/7.2-monoidal-categories-functoriality-of-adts-profunctors.html">I-7.2: Monoidal Categories, Functoriality of ADTs, Profunctors</a></b> - 49:15
    </li>
    <li>
    
 <div style="margin:1em;">--- end of current notes ---</div>

        <b><a href="younotes1/8.1-function-objects-exponentials.html">I-8.1: Function objects, exponentials</a></b> - 45:25
    </li>
    <li>
        <b><a href="younotes1/8.2-type-algebra-curry-howard-lambek-isomorphism.html">I-8.2: Type algebra, Curry-Howard-Lambek isomorphism</a></b> - 20:56
    </li>
    <li>
        <b><a href="younotes1/9.1-natural-transformations.html">I-9.1: Natural transformations</a></b> - 51:27
    </li>
    <li>
        <b><a href="younotes1/9.2-bicategories.html">I-9.2: bicategories</a></b> - 43:04
    </li>
    <li>
        <b><a href="younotes1/10.1-monads.html">I-10.1: Monads</a></b> - 1:15:29
    </li>
    <li>
        <b><a href="younotes1/10.2-monoid-in-the-category-of-endofunctors.html">I-10.2: Monoid in the category of endofunctors</a></b> - 32:57
    </li>
 </ul>

 <h2>Part II</h2>
 <ul>
    <li><b><a href="younotes2/">II-1.1: Declarative vs Imperative Approach</a></b> - 36:17</li>
    <li><b><a href="younotes2/">II-1.2: Limits</a></b> - 48:26</li>
    <li><b><a href="younotes2/">II-2.1: Limits, Higher order functors</a></b> - 42:36</li>
    <li><b><a href="younotes2/">II-2.2: Limits, Naturality</a></b> - 28:53</li>
    <li><b><a href="younotes2/">II-3.1: Examples of Limits and Colimits</a></b> - 41:48</li>
    <li><b><a href="younotes2/">II-3.2: Free Monoids</a></b> - 36:54</li>
    <li><b><a href="younotes2/">II-4.1: Representable Functors</a></b> - 50:19</li>
    <li><b><a href="younotes2/">II-4.2: The Yoneda Lemma</a></b> - 36:11</li>
    <li><b><a href="younotes2/">II-5.1: Yoneda Embedding</a></b> - 50:53</li>
    <li><b><a href="younotes2/">II-5.2: Adjunctions</a></b> - 40:36</li>
    <li><b><a href="younotes2/">II-6.1: Examples of Adjunctions</a></b> - 48:25</li>
    <li><b><a href="younotes2/">II-6.2: Free-Forgetful Adjunction, Monads from Adjunctions</a></b> - 37:15</li>
    <li><b><a href="younotes2/">II-7.1: Comonads</a></b> - 37:39</li>
    <li><b><a href="younotes2/">II-7.2: Comonads Categorically and Examples</a></b> - 44:05</li>
    <li><b><a href="younotes2/">II-8.1: F-Algebras, Lambek's lemma</a></b> - 51:39</li>
    <li><b><a href="younotes2/">II-8.2: Catamorphisms and Anamorphisms</a></b> - 42:27</li>
    <li><b><a href="younotes2/">II-9.1: Lenses</a></b> - 41:5911</li>
    <li><b><a href="younotes2/">II-9.2: Lenses categorically</a></b> - 43:42</li>
 </ul>

 <h2>Part III</h2>
 <ul>
    <li><b><a href="">III-1.1: Overview part 1</a></b> - 26:59</li>
    <li><b><a href="">III-1.2: Overview part 2</a></b> - 28:12</li>
    <li><b><a href="">III-2.1: String Diagrams part 1</a></b> - 29:08</li>
    <li><b><a href="">III-2.2: String Diagrams part 2</a></b> - 32:15</li>
    <li><b><a href="">III-3.1: Adjunctions and monads</a></b> - 25:48</li>
    <li><b><a href="">III-3.2: Monad Algebras</a></b> - 28:31</li>
    <li><b><a href="">III-4.1, Monad algebras part 2</a></b> - 26:55</li>
    <li><b><a href="">III-4.2, Monad algebras part 3</a></b> - 29:02</li>
    <li><b><a href="">III-5.1, Eilenberg Moore and Lawvere</a></b> - 29:55</li>
    <li><b><a href="">III-5.2, Lawvere Theories</a></b> - 29:26</li>
    <li><b><a href="">III-6.1, Profunctors</a></b> - 29:14</li>
    <li><b><a href="">III-6.2, Ends</a></b> - 34:26</li>
    <li><b><a href="">III-7.1, Natural transformations as ends</a></b> - 33:36</li>
    <li><b><a href="">III-7.2, Coends</a></b> - 43:15</li>
 </ul>

 </div>


 <div style="float:left;">
 <center><h2>Original resources
 <br>from Bartosz Milewski</h2></center>

 <ul>
    <li>
        <a href="https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_">Youtube playlist - Part I</a> (20 videos, ~ 15h).
    </li>
    <li>                               
        <a href="https://www.youtube.com/playlist?list=PLbgaMIhjbmElia1eCEZNvsVscFef9m0dm">Youtube playlist - Part II</a> (18 videos, ~ 10h30).
    </li>
    <li>
        <a href="https://www.youtube.com/playlist?list=PLbgaMIhjbmEn64WVX4B08B4h2rOtueWIL">Youtube playlist - Part III</a> (18 videos, ~ 7h).
    </li>
    <li>
        <a href="http://www.lulu.com/shop/bartosz-milewski/category-theory-for-programmers/hardcover/product-23389988.html">Paper book at lulu.com</a> (452 pages)
    </li>
    <li>
        <a href="https://github.com/hmemcpy/milewski-ctfp-pdf">PDF book</a> (~ 500 pages)
    </li>
    <li>
        <a href="https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/">Category Theory for Programmers : blog pages</a>
    </li>
    <li>
        <a href="https://github.com/hmemcpy/milewski-ctfp-pdf.git">Repository containing the tex source of the pdf book</a>
    </li>
 </ul>


 </div>
 <br style="clear:left;">

 <h2>About these notes</h2>

 <div style="font-family:Times New Roman, Times, serif;">
 Started in 2018 by Thierry Graff.
 <br>There are notes until part I, chapter 7.2 ; for the moment, I stopped watching the videos (because I bought the book).
 <br>You can download these notes from the git repository : <a href="https://gitea.larzac.info/tig12/categories">gitea.larzac.info/tig12/categories</a>.
 <br>
 <br>The notes are written in english but I use french conventions for capitalization and spaces.
 <br>- The characters <code>; : ? !</code> are preceeded and followed by a white space.</li>
 <br>- Names of months, weekdays, languages etc. are not capitalized.</li>
 </div>

 </body>
 </html>
--- a/static/style.css
+++ b/static/style.css
@@ -0,0 +1,235 @@
 /* ================ General styles ================ */
 body{
    margin:0;
    padding:0.5rem;
    background:#eee;
    font-family:Arial,Helvetica,sans-serif;
 }

 a{text-decoration:none;}

 pre{
    margin:1rem 2rem;
    background:lightgrey;
    font-size:1rem;
    padding:.5rem;
 }
 pre.normal{background:none;}
 code.color{background:lightgrey;}
 .pre{white-space:pre;}

 img{display: block; background:white;}
 img.center{border:none;margin:auto;}

 ul.spaced>li,ol.spaced>li{padding-bottom:0.8rem;}
 ul.naked>li,ol.naked>li{list-style-type:none;}

 table.border{border-collapse:collapse;}
 table.border td{border: 1px solid #a2a9b1;}
 .vertical-align-top{vertical-align:top;}

 cite{
    font-family:DejaVu,serif;
    display:block;
    margin:1rem;
 }
 blockquote{
    display:block;
    border:1px solid grey;
    padding:5px;
    margin:1rem;
    font-family:DejaVu,serif;
    background:#fee;
 }

 /* ================ Site layout ================ */
 .flex-wrap{
    display:flex;
    flex-wrap:wrap;
 }
 aside ul{padding:0;}
 aside li{list-style:none;}

 /* ================ Headings ================ */
 h1{
    width:100%;
    margin:auto;
    text-align:center;
    font-size:2.5rem;
    font-weight:bold;
    padding:0.3rem;
    margin-bottom:1rem;
 }
 h2{font-size:2rem;}
 h1 .subtitle{font-size:0.8em;}
 h3{font-size:1.5rem;}


 /* ================ Navigation ================ */
 .prevnext{
    font-family:DejaVu,serif;
    position:fixed; top:0px; right:0px;
    margin:1rem;
    width:75px; height:40px
 }
 .prevnext a{
    display:inline-block;
    position:fixed;
    width:40px; height:40px;
    text-decoration:none;
    font-weight:bolder;
    font-size:2rem;
 }
 .prevnext a.index{top:0px; right:10px; font-size:0.5rem;}
 .prevnext a.top{top:0px; right:40px;}
 .prevnext a.prev{top:25px; right:75px;}
 .prevnext a.next{top:25px; right:5px;}

 /* table of content */
 .toc{font-family:Arial,Helvetica,sans-serif;}
 .toc ul{list-style-type:none;}
 .toc{padding:0;}
 .toc>ul>li>a{font-weight:bold;}


 /* ================ Particular elements ================ */
 .warning{
    width:50%;
    padding:.5rem;
    margin:.5rem;
    background:gold;
    border:1px solid grey;
 }

 .intro{
    font-size:1.4rem;
    margin:1rem 0 1rem 2rem;
 }

 .exo{
    font-size:1rem;
    border:1px solid grey;
    padding:0.6rem 1rem;;
    background:lightyellow;
    margin:1rem;
 }
 .exo ul{margin:0;}

 table.wikitable{
    border-collapse:collapse;
 }
 table.wikitable > tr > th, table.wikitable > * > tr > th {
    /* background-color: #eaecf0; */
    background-color: lightblue;
    text-align: center;
    vertical-align:top;
 }
 table.wikitable > tr > th, table.wikitable > tr > td, table.wikitable > * > tr > th, table.wikitable > * > tr > td {
    border: 1px solid #a2a9b1;
    padding: 0.2rem 0.4rem;
    vertical-align:top;
 }
 table.wikitable tr td code{
    background:none;
 }


 /* ================ Style shortcuts ================ */

 .inline-block{display:inline-block;}
 .block{display:block;}

 .arial{font-family:Arial,Helvetica,sans-serif;}
 .courier{font-family:"Courier New",Courier,monospace;}
 .dejavu{font-family:DejaVu,serif;}

 .bold{font-weight:bold;}

 .center{text-align:center;}

 .background-none{background:none;}
 .red{color:red;}

 .border-none{border:none;}
 .border-radius10{border-radius:10px;}
 .border{border:1px solid grey;}
 .border-left{border-left:1px solid grey;}
 .border-right{border-right:1px solid grey;}
 .border-top{border-top:1px solid grey;}
 .border-bottom{border-bottom:1px solid grey;}

 .margin-auto{margin:auto;}
 .margin{margin:1rem;}
 .margin0{margin:0;}
 .margin05{margin:.5rem;}
 .margin2{margin:2rem;}
 .margin3{margin:3rem;}

 .margin-top{margin-top:1rem;}                            
 .margin-top0{margin-top:0;}
 .margin-top05{margin-top:.5rem;}
 .margin-top2{margin-top:2rem;}
 .margin-top3{margin-top:3rem;}

 .margin-left{margin-left:1rem;}
 .margin-left0{margin-left:0;}
 .margin-left05{margin-left:.5rem;}
 .margin-left2{margin-left:2rem;}
 .margin-left3{margin-left:3rem;}
 .margin-left5{margin-left:5rem;}

 .margin-bottom{margin-bottom:1rem;}                            
 .margin-bottom0{margin-bottom:0;}
 .margin-bottom05{margin-bottom:.5rem;}
 .margin-bottom2{margin-bottom:2rem;}
 .margin-bottom3{margin-bottom:3rem;}

 .margin-right{margin-right:1rem;}
 .margin-right0{margin-right:0;}
 .margin-right05{margin-right:.5rem;}
 .margin-right2{margin-right:2rem;}
 .margin-right3{margin-right:3rem;}

 .padding{padding:1rem;}
 .padding0{padding:0;}
 .padding05{padding:.5rem;}
 .padding2{padding:2rem;}
 .padding3{padding:3rem;}

 .padding-top{padding-top:1rem;}
 .padding-top0{padding-top:0;}
 .padding-top05{padding-top:.5rem;}
 .padding-top2{padding-top:2rem;}
 .padding-top3{padding-top:3rem;}

 .padding-left{padding-left:1rem;}
 .padding-left0{padding-left:0;}                                      
 .padding-left05{padding-left:.5rem;}
 .padding-left2{padding-left:2rem;}
 .padding-left3{padding-left:3rem;}

 .padding-bottom{padding-bottom:1rem;}
 .padding-bottom0{padding-bottom:0;}
 .padding-bottom05{padding-bottom:.5rem;}
 .padding-bottom2{padding-bottom:2rem;}
 .padding-bottom3{padding-bottom:3rem;}

 .padding-right{padding-right:1rem;}
 .padding-right0{padding-right:0;}
 .padding-right05{padding-right:.5rem;}
 .padding-right2{padding-right:2rem;}
 .padding-right3{padding-right:3rem;}

 .big1{font-size:1.1rem;}
 .big2{font-size:1.2rem;}
 .big3{font-size:1.3rem;}
 .big4{font-size:1.4rem;}
 .big5{font-size:1.5rem;}
 .big20{font-size:2rem;}
 .big30{font-size:3rem;}
 .big40{font-size:4rem;}

 .small9{font-size:.9rem;}
 .small8{font-size:.8rem;}
 .small7{font-size:.7rem;}
 .small6{font-size:.6rem;}
--- a/younotes1/1.1-motivation-philosophy.html
+++ b/younotes1/1.1-motivation-philosophy.html
@@ -0,0 +1,67 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>1.1: Motivation and Philosophy | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <!-- <a class="prev" title="Previous" href="">&larr;</a> -->
    <a class="next" title="Next" href="1.2-what-is-a-category.html">&rarr;</a>
 </nav>

 <h1>1.1: Motivation and Philosophy</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=I8LbkfSSR58">this youtube video</a></div>

 <br>Is category theory useful only for functional programming ?
 <br>
 <br>Assembly language is the lowest possible level where you tell the computer exactly precisely what to do, like grab this thing from memory, put it in a register, use it as an address, then jump and so on. A very imperative way of programming, related to <b>Turing machines</b>, very primitive machines which stamps things on a paper tape : read this number, put it back on tape, erase something from the tape and so on. There is no high-level programming. This is one approach of programming.
 <br>
 <br>There is an other approach of programming which comes from <b>lambda calculus</b> ; what is possible to compute, thinking about mathematics in terms of how things can be actually executed.
 <br>
 <br>These approaches of programming are not very practical. Writing programs in assembly language is possible but does not scale, that's why we came up with languages that offer higher levels of abstraction ; the next level of abstraction was procedural programming.
 <br>Procedural programming relies on a very important idea : if you want to deal with a complex problem, you chop it into smaller problems (you divide a big problem into small procedures), solve them separately and combine the solutions - this is <b>composability</b>.
 <br>
 <br>Object oriented programming is even more abstract ; once you program an object, you don't have to look inside, you can forget about the implementation and just look at the surface of the object, its interface.
 <br>
 <br>So far we have two important ideas :
 <ul class="naked spaced">
    <li><b>Composability</b>.</li>
    <li><b>Abstraction</b> : we get rid of details.</li>
 </ul>

 With abstraction and composability comes the idea of <b>reusability</b>.
 <br>
 <br>Object-oriented approach poses problem when we want to write concurrent code. Concurrency does not mix well with object-oriented programming, because objects hide implementation, and hide exactly the wrong thing which make them not very composable. They hide mutation, changing their internal state without saying they do so. And they share data between them.
 <br>Mixing sharing and mutation has a name : <b>data race</b>.
 <br>We can use locks, but locks don't combine either.
 <br>
 <br>The next level of abstraction is functional programing ; you abstract things into functions. In a functional language, you don't have mutations so you don't have this problem of hiding data races. You also have ways of composing data structures into bigger data structures. As everything is immutable, you can safely compose things.
 <br>
 <br>Category theory is this higer-level language above functional languages. Not a language which permits to write code, but it lets us express ideas that can be later expressed in programming languages.
 <br>
 <br>Category theory unifies a lot of things ; if you abstract enough, many different things start to look similar in their structures. This permits to unify different areas of mathematics.
 <br>
 <br>If we try to abstract from low-level operations, we see that programming languages take their roots from <b>lambda calculus</b>.
 <br>And we see that all our data structures form <b>types</b>.
 <br>
 <br>There is also a type theory in mathematics, invented to solve paradoxes, like Russel's paradox, which says that you cannot construct the set of all sets (can a set contain sets that don't contain themselves ?) ; it can be translated in barber's paradox (a barber shaves persons that don't shave themselves, so can a barber shave himself ?). Russel's theory of types says that sets form layers upon layers, and we cannot have all sets and put them in one big set. This evolved to Marin Löf type theory, very formal.
 <br>
 <br>And there was logic ; people realized that these distinct areas of mathematics are exactly the same ; this is called the <b>Curry–Howard-Lambek isomorphism</b>, which says that whatever you do in logic can be directly translated into whatever you do in type theory. They are not similar, they are exactly the same, there is a one to one correspondance. And the Lambek part of this isomorphism says that there are certain types of categories (cartesian complete categories) that totally describe the same thing.
 <br>
 <br>Essentially all our human activity is described by one theory. One may turn philosophical, saying that we are not creating mathematics, but discovering them ; think that mathematicians discovered a deep truth about the universe.
 <br>A simpler explanation could be that categories reflect the way we function. We have a very elaborate visual system : our ability to interpret what we see from the outer world comes from billions of years of evolution. In contrast, the ability of our brain to think abstractly is very recent. Doing maths and science is a very fresh ability. This ability comes from the necessity to organize ourselves for activities like hunting, using coordination and language. Compared with the complexity of our visual cortex, this ability is very fresh and still primitive.
 <br>
 <br>Dividing a large problem in smaller pieces and combine the solutions into larger solutions is a so common process that we don't even notice it. This is how we do science as well. But we cannot assume that this reflects the deep nature of the universe. Physics of particles shows that at a certain level of detail, things are not separable. So maybe separation is only a property of our brains. So maybe category theory is not about maths, but about how our brains work ; about epistemology (how we approach things) and not ontology (how things are).

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/1.2-what-is-a-category.html
+++ b/younotes1/1.2-what-is-a-category.html
@@ -0,0 +1,140 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>1.2: What is a category | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="1.1-motivation-philosophy.html">&larr;</a>
    <a class="next" title="Next" href="2.1-functions-epimorphisms.html">&rarr;</a>
 </nav>


 <h1>1.2: What is a category ?</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=p54Hd7AmVFU">this youtube video</a></div>

 <br>The major tools we have at our disposition are :
 <ul>
    <li><b>Abstraction</b> : forget about unecessary details so that things that appear different may look identical.</li>
    <li><b>Composition</b></li>
    <li><b>Identity</b> : because of abstraction, this notion is not trivial ; some things are strictly identical, and some are identical for certain purposes. In mathematics, homotopy type theory is based on distinguishing between what is identical from what is not. Things that are almost equal are called <b>isomorphic</b>.</li>
 </ul>
 Composition and identity define category theory.
 <br>
 <br>A category is a <i>bunch</i> of objects. We don't use the term <i>set</i> because it has a precise mathematical meaning, and some categories are not a set of objects. Some things are bigger than sets.
 <br>If the objects form a set, then the category is called <i>small</i> ; if they don't form a set then it's a <i>large</i> category.
 <br>The arrows form a set (categories where the arrows don't form a set but are objects of a category are called higher-order categories).
 <br>
 <br>So a category is a bunch of <b>objects</b> and <b>arrows</b> (or <b>morphisms</b>) between objects.
 <br>An object is a primitive in this theory ; it has no properties, no internal structure.
 <br>A morphism is also a primitive, it has no properties, except that an arrow has a beginning and end.
 <br>Objects serve only to identify the ends of arrows.
 <br>Notice how this is related to human perception. Hunters were using arrows ! We are used to localize things in space. Arrows express the notion of movement, they are related to social relations between individuals. This language constrains us.
 <br>
 <br>When we define a category, we specify what the objects are, and for each pair of objects what are the arrows between them.
 <br>There may be from zero to an infinity of arrows between two objects. So it's OK to talk of a category as a graph if we admit that there can be an infinity of nodes and an infinity of edges.
 <img class="margin border" src="img/category.jpg" alt="General aspect of a category">
 There may be arrows going from <code>a</code> to <code>b</code>, and from <code>b</code> to <code>a</code>, and from <code>a</code> to <code>a</code>. 
 <br>There may be many different arrows going from <code>a</code> to <code>a</code>.

 <!-- ********************************************************************************* -->
 <h2>Properties</h2>

 <!-- ************************************* -->
 <h3>Composition</h3>
 A property expresses composition :
 <div class="margin">
 If there is an arrow <code>f</code> from <code>a</code> to <code>b</code>
 <br>and an arrow <code>g</code> from <code>b</code> to <code>c</code>,
 <br>then there must exist an arrow from <code>a</code> to <code>c</code>
 <br>that is identical to the composition of <code>f</code> and <code>g</code>.
 </div>

 This arrow is written <span class="formula">g o f</span>, and called <span class="formula">g after f</span>.
 <br>
 <br>There might be multiple arrows going from <code>a</code> to <code>c</code>, but <code>g o f</code> is the composition of <code>f</code> and <code>g</code>.
 <img class="margin border" src="img/composition.jpg" alt="Category composition">
 <br>
 For evey pair of <i>composable</i> arrows, their composition <b>must</b> exist.
 <br><b>Composable</b> means that the end of one is the beginning of the other.
 <br>Here we see the importance of the objects to identify the end and the beginning of the arrows.
 <br>
 <br>So composition is part of the definition of the category ; it must include the definition of composition for every composable pair of arrows, like a big multiplication table.

 <!-- ************************************* -->
 <h3>Identity</h3>

 An other property expresses identity : for every object <code>a</code>, there <b>must</b> exist an arrow going from <code>a</code> to <code>a</code>, called <code>id<sub>a</sub></code>.
 <img class="margin border" src="img/identity.jpg" alt="Identity in a category">

 It is an identity in the sense of composition : if we have an arrow <code>f</code> from <code>a</code> to <code>b</code> then we <b>must</b> have :

 <div class="flex margin">
    <img class="border" src="img/idb.jpg" alt="Left identity">
    <div class="padding"><span class="formula">id<sub>b</sub> o f = f</span> (left identity)</div>
 </div>
 and
 <div class="flex margin">
    <img class="border" src="img/ida.jpg" alt="Right identity">
    <div class="padding"><span class="formula">g o id<sub>a</sub> = g</span> (right identity)</div>
 </div>

 <!-- ************************************* -->
 <h3>Associativity</h3>

 If we have
 <ul class="naked margin0">
    <li>an arrow <code>f</code> from <code>a</code> to <code>b</code>,</li>
    <li>an arrow <code>g</code> from <code>b</code> to <code>c</code>,</li>
    <li>an arrow <code>h</code> from <code>c</code> to <code>d</code>,</li>
 </ul>
 then we must have :

 <div class="margin05"><span class="formula">h o (g o f) = (h o g) o f</span></div>
 So we can just omit parentheses.

 <img class="margin" src="img/associativity.jpg" alt="Category associativity">

 Some theories were deveoped where associativity is weak (both terms of the associativity equation are not identical but only isomorphic).

 <!-- ********************************************************************************* -->
 <h2>The <code>Set</code> category</h2>

 <div class="big2">Objects are types, and arrows are functions.</div>
 <br>A function is an arrow between two types.
 <br>Any single-argument function takes an argument of type <code>a</code> and returns a result of type <code>b</code>.
 <br>In this sense an function is an arrow between two types.
 <br>
 <br>The simplist model for types is that they are just sets of values.
 <br>So we can model programming as a category of sets ; functions are just mathematical functions, defined  between sets.
 <br>
 <br>A lot of categories come from some model.
 <br>For example you take set theory and represent the sets as objects in a category ; this category is called <code><b>Set</b></code>.
 <br>We have sets that have a structure that we know, they have elements.
 <br>When we build the <code><b>Set</b></code> category, <b>we forget the structure of the sets</b>, they are just objects, without structure.
 <br>We also know the functions between the sets. In the Set category, each function becomes an arrow.
 <br>Arrows in a category are also atomic, without structure. <b>We forget the knowledge we have about these functions</b>.
 <br>
 <br>This defines a category because functions can be composed, this composition is associative, and we can define an identity function for each set : the function which associates each element of a set to itself.
 <br>
 <br>So we forget about the structures of the sets and the functions, we just have these morphisms. And using only this, we can say a lot of things about the objects. For example, we can know that a set is empty, that it has only one element.
 <br>
 <br>This gives a completely new way of looking at things, more abstract.
 <br>
 <br>If you think about what's inside the sets, how the elements are mapped, this is assembly language, plumbery. With categories, you don't look inside, you just look at how they are connected.
 <br>
 <br>This achieves the ultimate in data hiding : you have a data type shrunk to a point, and you only know its interface, how it connects to other objects.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->

 </body>
 </html>
--- a/younotes1/10.1-monads.html
+++ b/younotes1/10.1-monads.html
@@ -0,0 +1,27 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>10.1: Monads | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="9.2-bicategories.html">&larr;</a>
    <a class="next" title="Next" href="10.2-monoid-in-the-category-of-endofunctors.html">&rarr;</a>
 </nav>


 <h1>10.1: Monads</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=gHiyzctYqZ0">this youtube video</a></div>



 </body>
 </html>
--- a/younotes1/10.2-monoid-in-the-category-of-endofunctors.html
+++ b/younotes1/10.2-monoid-in-the-category-of-endofunctors.html
@@ -0,0 +1,26 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>10.2: Monoid in the category of endofunctors | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="10.1-monads.html">&larr;</a>
 </nav>


 <h1>10.2: Monoid in the category of endofunctors</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=GmgoPd7VQ9Q">this youtube video</a></div>



 </body>
 </html>
--- a/younotes1/2.1-functions-epimorphisms.html
+++ b/younotes1/2.1-functions-epimorphisms.html
@@ -0,0 +1,179 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>2.1: Functions, epimorphisms | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="1.2-what-is-a-category.html">&larr;</a>
    <a class="next" title="Next" href="2.2-monomorphisms-simple-types.html">&rarr;</a>
 </nav>


 <h1>2.1: Functions, epimorphisms</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=O2lZkr-aAqk">this youtube video</a></div>

 <br>Every time you design a language, you have to provide semantics : what does it mean ? There are two ways of defining semantics.
 <br>One is <b>operational semantics</b> by telling how this things execute ; how a statement can be transformed in a simpler one.
 <br>And the other is <b>denotational semantics</b> where you map it into an other area that you understand, in particular into mathematics. So you build a mathematical model  and you say : this statement or this construct in the language corresponds to this mathematical thing.
 <br>
 <br>For example for types, it is a set of values ; for functions, it is a function between sets.
 <br>
 <br>A function in programming, especially in imperative languages, is not exactly the same as a function in mathematics.
 <br>A function between sets is what we call a <b>pure function</b> and a <b>total function</b> in programming.
 <br>
 <br>A total function is defined for all its arguments, and its argument are taken from some type ; so a function for integers has to be defined for all integers.
 <br>
 <br>A function is pure if you can <b>memoize</b> it, turn it into a lookup table, because for each value of an argument, it should return a particular value. And you can remember this value. You call this function once, it evaluates its argument, you store the answer in a table and the next time you call it you can do a lookup in the table. For finite sets (like booleans or characters), functions are easy to tabulate (functions like <code>isAlpha()</code>, <code>isPrintable()</code>) ; for infinte sets, like strings or integers, we can't tabulate them only because of finite resources - but we could with infinite resources. Functions like <code>getCharAt()</code> can't be memoized.
 <br>
 <br>In practice, we need side effects, but this can be described on top of pure functions.
 <br>If we get to the bottom, the simplest, we get to pure functions, and we can build more complex things on top of it using composability.

 <!-- ******************************* -->
 <h2>Functions</h2>

 Functions are defined in mathematics as a special kind of <b>relation</b>.
 <br>We place ourselves in set theory, not in <b><code>Set</code></b> category (because in category theory, we don't know about the elements).
 <br>So a relation is a subset of pairs of elements. The set of all pairs form a <b></b>.
 <br>Any substet of this cartesian product is a relation by definition. Without any other requirement.

 <img class="margin" src="img/relation.jpg" alt="Relation">

 A relation doesn't have to be symetric.
 <br>An element of <code>S<sub>1</sub></code> can be mapped to several elements of <code>S<sub>2</sub></code>.
 <br>Several elements of <code>S<sub>1</sub></code> can be mapped to the same element of <code>S<sub>2</sub></code>.
 <br>
 <br>Functions have direction.
 <br>We have a relation <i>between <code>S<sub>1</sub></code> and <code>S<sub>2</sub></code></i>,
 <br>but we have a function <i>from <code>S<sub>1</sub></code> to <code>S<sub>2</sub></code></i>.
 <br>
 <br>One argument of a function cannot be mapped into several elements.
 <br>But it's ok for several arguments of a function to be mapped to the same value.
 <br>If we consider total functions, all the elements of <code>S<sub>1</sub></code> must be mapped to elements of <code>S<sub>2</sub></code>. But not all elements of <code>S<sub>2</sub></code> need to be mapped by the function

 <img class="margin" src="img/function.jpg" alt="Function">

 <code>S<sub>1</sub></code> is called the <b>domain</b> of the function and <code>S<sub>2</sub></code> the <b>codomain</b>
 <br>The <b>image</b> of the function is the subset of <code>S<sub>2</sub></code> that is mapped by the function.
 <br>
 <br>Functions have directionality.
 <br>This is important because we find directionality in other kinds of mapping in category theory : <b>functors</b> (mapping between categories), <b>natural transformations</b> (mappings between functors) have the same kind of directionality.
 <br>The simplest way to understand this directionality is asking : is the function invertible ? If a function <code>f</code> permits to go from <code>a</code> to <code>b</code>, is there a function that permits to go from <code>b</code> to <code>a</code> ? Generally it is not.

 <!-- ************************************* -->
 <h3>Isomorphisms</h3>
 If we use Haskell notation :
 <br>
 <br><span class="formula">f :: a &rarr; b</span> (a type of function which goes from set a to set b)
 <br>
 <br><code>f</code> is invertible if there exists a function <span class="formula">g :: b &rarr; a</span> such as
 <br>
 <br><span class="formula">g o f = Id</span>
 <br>
 <br>It means that if you have an element <code>x</code> in <code>a</code>, you map it to an element <code>y</code> in <code>b</code> : <b>f(x) = y</b>
 <br>And then if you map <code>y</code> to an element of <code>a</code> with <code>g</code>, you necessarily come back to <code>x</code> :  <b>g(y) = x</b>
 <br>You come back to the same element for any <code>x</code> in the domain of <code>f</code>.
 <br>The same applies in the other direction :
 <br>
 <br><span class="formula">f o g = Id</span>
 <br>
 <br>A function that is invertible is symetric ; it is called an <b>isomorphism</b>.
 <br>This property can be translated to categorical language :

 <img class="margin" src="img/isomorphism.jpg" alt="Isomorphism">

 <br><span class="formula">g o f = Id<sub>a</sub></span> <span class="formula">f o g = Id<sub>b</sub></span>
 <br>
 <br>We can now express this property without talking about elements.
 <br>And this property is defined for any category, not only category of sets.
 <br>The property is expressed in terms of composition and identity, nothing else.
 <br>
 <br>Isomorphisms are great, they permit to identify two sets, there is a one to one mapping between two sets.
 <br>The two sets can be considered as identical for certain purposes ; they are not really identical, only isomorphic, but we have an identification between these two sets.
 <br>For finite sets, the identification is straight ; for infinite sets, it's a bit more complicate.
 <br>
 <br>There are two reasons for a function not to be an isomorphism :
 <ul class="spaced">
    <li>
        If a function collapses several elements of <code>a</code> to the same element of <code>b</code>.
        <img class="margin" src="img/function-non-injective.jpg" alt="Non injective function">
        For example function <code>isEven()</code>, which asociates a boolean to an integer.
        <br>This corresponds to the process of abstraction : we loose information about which element generated <code>y</code>, we leave the details to keep only the information that interests us.
    </li>
    <li>
        If the image of the function doesn't fill the whole codomain.
        <img class="margin" src="img/function-non-surjective.jpg" alt="Non surjective function">
        Corresponds to the process of modeling : I'm recognizing the pattern of <code>a</code> inside <code>b</code>.
    </li>
 </ul>

 If we think of a function as something directional, as a process which takes place in time, a function that is not invertible increases entropy. We make a transformation, and can't get back to the initial state.

 <br>
 <br>Mathematicians have names for these properties ; the definitions are converse :
 <ul class="spaced">
    <li>
        If a function does not collapse, then it is called <b>injective</b> ; the function is a <b>injection</b>
        <br>If <code>f(x<sub>1</sub>) = f(x<sub>2</sub>)</code> then <code>x<sub>1</sub> = x<sub>2</sub></code>
    </li>
    <li>
        If the image fills the whole codomain (the image is equal to the codomain), then it is called <b>surjective</b> ; the function is a <b>surjection</b>.
        <br>&forall; y &isin; b, &exist; x &isin; a | y = f(x)
        <br>(for all y in b, there exists an x such as y = f(x))
    </li>
 </ul>

 If a function is both injective and surjective, then it is a <b>bijection</b>, it is invertible.


 <!-- ********************************************************************************* -->
 <h2>Epimorphism, monomorphisms</h2>

 We have defined the notions of injection and surjection in set theory, using the elements of sets.
 <br>But how can we do that in the <b><code>Set</code></b> category ? We can't use the elements of sets anymore, sets are seen as objects without structure.
 <br>We must use a general way to work in category theory : define the property of an object using the relations of this object with the other objects of the category.
 <br>
 <br>In the Set category, a surjection is called an <b>epimorphism</b> (surjective is called <b>epic</b>), and an injection is called a <b>monomorphism</b> (injective is called <b>monic</b>).
 <br>
 <br>But these are defined for any category, not only sets, so they are more general notions.

 <!-- ******************************* -->
 <h3>Epimorphism</h3>

 So how to define an epimorphism without talking about elements ? We use other functions and composition.

 <img class="margin" src="img/epimorphism.jpg" alt="Categorical definition of an epimorphism">

 If we have a function <code>f</code> from <code>a</code> to <code>b</code> which is not surjective, it means that there are elements of <code>b</code> that are not in the image of <code>f</code>.
 <br>If we take a function <code>g :: b &rarr; c</code> whose domain is <code>b</code>, it will map elements of <code>b</code> that are inside and outside the image of <code>f</code>.
 <br>But if we compose <code>g</code> with <code>f</code>, <code>g o f</code> will only act on the image of <code>f</code>, and do not deal with the elements outside the image of <code>f</code>.
 <br>If we take two such functions <code>g<sub>1</sub></code> and <code>g<sub>2</sub></code> that differ only outside the image of <code>f</code>, the compositions <code>g<sub>1</sub> o f</code> and <code>g<sub>2</sub> o f</code> will be the same.
 <br>So we can have <code>g<sub>1</sub> o f = g<sub>2</sub> o f</code> with <code>g<sub>1</sub></code> different from <code>g<sub>2</sub></code>.
 <br>

 <br>The converse of this logic permits to define an epimorphism :
 <br>
 <div class="formula margin inline-block">
 f is an epimorphism if for all set c, for all functions g<sub>1</sub> and g<sub>2</sub>,
 <br>g<sub>1</sub> o f = g<sub>2</sub> o f implies that g<sub>1</sub> = g<sub>2</sub>
 </div>

 <br>In the <code>Set</code> category, this corresponds to surjection.
 <br>But this is defined without any references to elements of the sets, and applies to any category.
 <br>
 <br>Notice that we use "for all" quantifiers : we must look at all sets <code>c</code>, and all functions <code>g</code> from <code>b</code> to <code>c</code> to define the property of <code>f</code>.
 <br>
 <br>A way to look at this is that we can cancel <code>f</code> : <code>g<sub>1</sub> <strike>o f</strike> = g<sub>2</sub> <strike>o f</strike></code>

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/2.2-monomorphisms-simple-types.html
+++ b/younotes1/2.2-monomorphisms-simple-types.html
@@ -0,0 +1,95 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>2.2: Monomorphisms, simple types | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="2.1-functions-epimorphisms.html">&larr;</a>
    <a class="next" title="Next" href="3.1-examples-orders-monoids.html">&rarr;</a>
 </nav>


 <h1>2.2: Monomorphisms, simple types</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=NcT7CGPICzo">this youtube video</a></div>

 <!-- ********************************************************************************* -->
 <h2>Monorphisms</h2>

 A non-injective function will map two elements <code>x<sub>1</sub></code> and <code>x<sub>2</sub></code> of set <code>a</code> to the same element <code>y</code> of set <code>b</code>.

 <img class="margin" src="img/monomorphism.jpg" alt="Monomorphism">

 <br>If we consider functions <code>g<sub>1</sub></code> and <code>g<sub>2</sub></code> from <code>c</code> to <code>a</code>, equal except in <code>z</code> : <code>g<sub>1</sub>(z) = x<sub>1</sub></code> and <code>g<sub>2</sub>(z) = x<sub>2</sub></code>.
 <br>Here we have <code>g<sub>1</sub></code> different from <code>g<sub>2</sub></code> but <code>f o g<sub>1</sub> = f o g<sub>2</sub></code>

 <br>
 <br>Taking the converse permits to define a monomorphism :
 <br>
 <div class="formula inline-block margin">
 <code>f</code> is a monomorphism if for all object <code>c</code>, for all morphism <code>g<sub>1</sub></code> and <code>g<sub>2</sub> :: c &rarr; a</code>
 <br>f o g<sub>1</sub> = f o g<sub>2</sub> implies that g<sub>1</sub> = g<sub>2</sub>.
 </div>

 <br>Again, we define a property of one morphism using the whole universe.
 <br>
 <br>In set theory a function that is both injective and surjective is a bijection ; so we can ask if in category theroy a morphism which is both an automorphism and an epimorphism is encessarily an isomorphism. The answer is no, there are counter-examples.

 <!-- ********************************************************************************* -->
 <h2>Single types</h2>

 Here we define some simple types in terms of elements, and we'll see later how this can be expressed in category theory.

 <!-- ************************************* -->
 <h3>Zero elements - Empty set</h3>

 Does not correspond to a type in imperative languages.
 <br>In Haskell, types are funny because they contain this bottom element. So an empty set is not really empty because it contains this bottom element. But if we forget for a moment about functions that never terminate, then we can say that the empty set corresponds to the type <b>Void</b>. It has no constructor.
 <br>Can we find function that takes an argument of type Void ?
 <br>If we define a function in terms of elements, mathematically speaking, the answer is yes. We could call this function a bluff. If I declare "I have a function that takes a Void and return an integer, I challenge you to call it. Prove me wrong.", you can't because there is no way to produce an element of type Void. The ability to construct a function taking a Void as argument (even if we can't call it) is important because it permits to define Void identity.
 <br>
 <div class="formula inline-block">Id<sub>Void</sub> :: Void &rarr; Void</div>
 <br>
 It exists "in vacuum" : you cannot provide an argument for it, you cannot actually test what it does. But it exists.
 <br>In Haskell, it is called an <i>absurd</i> function.
 <br>This name makes sense if you start translating programming or type theory into logic.
 <br>In logic, Void corresponds to false. We can't construct falsity from something (we can't prove that something is false, if something is false, it's false, it has no proof). In this correspondance between types and logic (propositions as types), the existence of a function corresponds to a proof of a proposition.
 <br>Since we can't create a Void, there is no proof af falsity.
 <br>But if we assume false, then from false follows anything.
 <br>
 <div class="formula inline-block">absurd :: Void &rarr; a</div> (a is any type).


 <!-- ************************************* -->
 <h3>One element - Singleton</h3>

 In Haskell, this type is called unit and noted <code>()</code>. It has only one element, and it can be constructed from nothing.
 <br>The notation for the element of the singleton type is also noted <code>()</code> ; we have the type definition <code>() :: ()</code>.
 <br>In the point of view of logic, it correponds to <code>true</code>. We can always prove that it's true (it's a tautology).
 <br>We can write a function <code>unit</code> that returns a unit from any type : <code>unit :: a &rarr; ()</code>. As unit can be created from thin air, we just disregard the argument, create and return a unit.
 <br>
 <br>The function <code>() &rarr; Int</code> is the creation of a constant (a pure function always returns the same value) ; there are many functions like this, for any type.
 <br>For boolean, there are two functions like this : <code>() &rarr; true</code> and <code>() &rarr; false</code>.
 <br>We have as many functions as there are elements in the set.
 <br>We have a way to define the value of an element of a set without talking about elements.
 <br>A family of functions from unit corresponds to picking elements of a set.
 <br>In category theory we'll generalize the notion of singleton set. These functions permit to associate a singleton to any object, they are called <i>generalized elements</i>. It's a kind of backdoor way to talk about elements in category. But the singleton does not exist in all categories.

 <h3>Two elements - Booleans</h3>

 A two element set is equivalent to type <code>Bool</code>. We'll see later that bool is not an atomic construction in Set category, it can be defined as a sum of two units.
 <br>But the two types <code>Void</code> and <code>Unit</code> form the basis for the rest, we can build on top of them to build more complex types.
 <br>A function that returns a boolean is called a <b>predicate</b>, for example <code>isDigit()</code>.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/3.1-examples-orders-monoids.html
+++ b/younotes1/3.1-examples-orders-monoids.html
@@ -0,0 +1,159 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>3.1: Examples of categories, orders, monoids | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="2.2-monomorphisms-simple-types.html">&larr;</a>
    <a class="next" title="Next" href="3.2-kleisli-category.html">&rarr;</a>
 </nav>


 <h1>3.1: Examples of categories, orders, monoids</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=aZjhqkD6k6w">this youtube video</a></div>

 <h2>Empty category</h2>
 A category with no object and no arrow. The axioms af a category are satisfied :
 <ul>
    <li>For any pair of composable arrows, there is an arrow going straight from <code>A</code> to <code>C</code>. If there are no pair, this is automatically satisfied.</li>
    <li>For any object, there has to be an identity. If there is no object, it's automatically satisfied.</li>
 </ul>
 This category is noted <span class="formula">&empty;</span>.
 <br>By itself this category is useless. The value of this category is in context. In the category of all categories, or in the category of small categories, this is important (it's a terminal object).

 <h2>One object category</h2>
 It has at least one arrow, the identity. Also useless by itself, but useful in the context of all categories (it's also a terminal object).

 <h2>Free construction from a graph</h2>
 If we have a graph and want to build a category from it, we can do it by adding arrows.

 <img src="img/graph2category.jpg" alt="Free construction of a category from a graph">

 <br>- Add identity arrows for all nodes of the graph.
 <br>- Add arrows that permit composability.
 <br>And we must check that associativity is satisfied.
 <br>
 <br>For finite graphs, we get a category by adding a finite number of arrows.
 <br>
 <br>This construction in which we just keep adding stuff in order to satisfy the axioms is a very common construction in category theory.
 <br>It's called <b>free construction</b> ; free because we have no constraint other than the constraints required by the definition of a category.
 <br>Free construction can be applied to get a free group, a free monoid and so on.
 <br>
 <br>We'll see applications of free construction for our programming tasks.

 <h2>Orders</h2>
 Orders are categories in which arrows are not functions ; in zero and one object categories, arrows were not functions, but they are abstract arrows which do not have intuitive meaning.
 <br>In orders, arrows represent a relation. In particular an interesting relation is less or equal (<span class="formula">&le;</span>).
 <br>If we have two objets <code>a</code> and <code>b</code>, we draw an arrow from <code>a</code> to <code>b</code> if <code>a &le; b</code> (we also say "<code>a</code> comes before <code>b</code>").
 <br>
 <br>There are certain conditions an order has to fullfill in order to be an order.
 <br>And there are different types of orders : <b>preorders</b>, <b>partial orders</b>, <b>total orders</b>. We are mostly familiar with total order, because when we are sorting, we require that the elements satisfy a total order.

 <h3>Preorders</h3>

 We only require composition : if <code>a &le; b</code> and <code>b &le; c</code>, then we want <code>a &le; c</code>

 <img src="img/preorder.jpg" alt="Preorder">

 In a preorder, there is either one arrow or no arrow between two objects. There cannot be multiple arrows between two objects.
 <br>Between two osbjects means starting from one object and ending to an other object. In principle we can have an arrow going backwards too.
 <br>
 <br>Associativity is obvious.
 <br>
 <br>And there must be identity (the relation must be reflexive) ; that's why there is the "or equal".
 <br>
 <br>A category like this is called a <b>thin category</b>. Every thin category corresponds to a preorder, and every preorder corresponds to a thin category ; there is a one to one correspondance.
 <br>
 <br>If we consider all the different kinds of orders, category theory tells us that preorders are the most basic.
 <br>
 <br>The set of arrows between two objects in a category is called the <b>hom-set</b>.
 <br>The hom-set in a category C between objects a and b is noted <span class="formula">C(a,b)</span>
 <br>We can have <span class="formula">C(a,a)</span>
 <br>A hom-set is a set in the sense of set theory.
 <br>
 <br>A thin category is a category in which every hom-set has either zero or one element.

 <h3>Partial orders</h3>

 We impose additional conditions on preorder to get a partial order.
 <br>Partial order is something that has no loops : if you have an arrow from a to b, you cannot have an arrrow from b to a.
 <br>If wee look at it as a graph, it corresponds to a <b>Directed Acyclic Graph (DAG)</b>.

 <h3>Total Orders</h3>

 The additional condition is that there is one arrow between <i>every</i> object of the category.

 <h2>Epic and monic but not isomorphic</h2>

 <img src="img/epi-mono-thin-category.jpg" alt="Epimorphism and monomorphism in a thin category">

 Going back to the definition of epiomrphism and monomorphism in terms of equality of arrows that go from or to beginning or end of morphism, we see that this is automatically satisfied in a thin category as there is only one arrow between two objects.
 <br>So every arrow in a preorder is an epimorphism and a monomorphism at the same time. But it is not necessarily invertible. In a partial order, this is never invertible because there is no loops.
 <br>
 <br>This is a counter example : an arrow can be both an epimorphism and a monomorphism without being invertible.
 <br>This is different from functions defined with sets, were a injective and surjective function is a bijection (then invertible).

 <h2>Thick categories</h2>
 Categories where hom-sets have multiple arrows.
 In a thin catgory, there may be one or zero arrow ; there is or there is no relation ; a black and white world.
 <br>In a thick category, there may be multiple arrows between objects. If there are no arrows, the objects are not in relation. If there are multiple arrows, they can be seen as different proofs of the relation ; a category can be seen as a proof-relevant order.
 <br>This kind of proof-relevant stuff is becoming more and more important in homotopy type theory, which is built on the asumption that it's not only enough to show that something is related to something else, tehre are different ways to show they are related, and they are not equivalent.

 <h2><a name="monoids">Monoids</a></h2>
 A one-object category can have many loops. One of them is the identity

 <img src="img/one-object-category.jpg" alt="One object category">
 All the arrows are composable because the beginnings and ends of all arrows are the unique object.
 <br>
 <br>A category with a single object is called a <b>monoid</b>.
 <br>
 <br>Monoids are known from algebra as a set of elements and a binary operation (let's call it multiplication) with two conditions imposed :
 <ul>
    <li>
        There is a special element called unit (noted <code>e</code>)such as when you multiply (left or right multiplication) an element by unit, you get the same element :
        <br><code>&exist; e | &forall; a, a * e = e * a = a</code>
        <br>(there exists <code>e</code> such as for all <code>a</code>, <code>a * e = e * a = a)</code>)
    </li>
    <li>The operation is associative : <code>(a *b) * c = a * (b * c)</code></li>
 </ul>
 Examples :
 <ul>
    <li>Natural numbers with multiplication (e = 1)</li>
    <li>Natural numbers with addition (e = 0)</li>
    <li>String concatenation (e = empty string) - interesting example because the operation is not symetric, like addition or multiplication</li>
    <li>List concatenation with appending operation (e = empty list).</li>
 </ul>

 Monoids defined in terms of sets and monoids defined in category theory are equivalent.
 <br>If we call <code>M</code> the monoid defined as a catgory, <code>M</code> has only one hom-set ; <code>M(m, m)</code> is the set of arrrows that start and end at <code>m</code>.
 <br>This hom-set is a set.
 <ul>
    <li>
        So we can go from our category <code>M</code> to a monoid defined in terms of set theory : the category defines a set <code>M(m, m)</code> ; taking two elements from this set (which correspond to two arrows), there is a third element which corresponds to the composition of theses arrows ; the composition corresponds to the multiplication. And one of the elements of the set corresponds to identity, which is automatically a unit. And it's associative.
    </li>
    <li>
        And vice-versa if we start with a monoïd in set theory, we can create a category and define composition using the multiplication.
    </li>
 </ul>
 So there is a one to one correspondance ; these are the same things seen from two different perspectives.

 <img src="img/monoid-set-category.jpg" alt="Equivalence of monoid defined as a set and a category">

 For example, to express the addition in natural numbers as a category, we would have one a arrow which corresponds to adding 5, one arrow corresponding to adding 2, and their composition corresponds to adding 7.
 <br>
 <br>Back to programming, the category of types corresponds to a system that is strongly typed. You cannot compose any two functions, you can compose only functions that match ; the result of one function must have a type that is the same as the argument to the next functioon.
 <br>A momoid is a very special category in which any two functions are composable ; that corresponds to languages which have weak typing.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/3.2-kleisli-category.html
+++ b/younotes1/3.2-kleisli-category.html
@@ -0,0 +1,180 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>3.2: Kleisli category | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="3.1-examples-orders-monoids.html">&larr;</a>
    <a class="next" title="Next" href="4.1-terminal-and-initial-objects.html">&rarr;</a>
 </nav>


 <h1>3.2: Kleisli category</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=i9CU4CuHADQ">this youtube video</a></div>

 <h2>Inclusion</h2>

 This deals with an interesting case to study.
 <br>Let's define a relation on sets, the relation of <b>inclusion</b>. For a set, being a subset of an other set is a relation that we note <span class="formula">&sube;</span>.
 <br>What kind of relation is it ? An order, a preorder ?
 <br>Every set is a subset of itself, so we have identity (in terms of orders, we say it is reflexive).
 <br>It is transitive : if a is <code>a</code> subset of <code>b</code> and <code>b</code> is a subset of <code>c</code> then a is <code>a</code> subset of <code>c</code>.
 <br>And the associativity is obvious.
 <br>
 <br>So this is a preorder.
 <br>This is a partial order because there may be loops : <span class="formula">if a &sube; b &#8896; b &sube; a &rArr; a = b</span>.
 <br>This is not a total order because there may exist disjoint sets or sets that partially overlap.
 <br>We can have a diamond situation : 
 <div>
    <img src="img/diamond1.jpg" alt="" />
    <img src="img/diamond2.jpg" alt="" />
 </div>

 We have a category based on sets where the arrows are not functions, but relations. Some versions of this category is used in modeling topology ; open sets have this property of inclusion.

 <h2>Kleisli category</h2>

 This is a category based on the category of types and functions.
 <br>We can get to this category by solving a programming problem :
 <br>We maintain a library of functions and a new requirement comes : every function must be auditable : every function has to create a log "I was called".
 <br>The simplest solution that comes to mind of imperative programmers is creating a global log.
 So we have in C++
 <div><pre>string log = "";</pre></div>
 If we have a function 
 <div><pre>
 bool negate(bool x){
    return !x;
 }
 </pre></div>
 To add a trace in the log, we can modify it :
 <div><pre>
 bool negate(bool x){
    log += "not!";
    return !x;
 }
 </pre></div>

 This looks simple, but is it really simple ?
 <br>It introduces a <i>hidden dependency</i> between the bodies of our functions a the global log.
 <br>This can't be seen if we look at the signature of <code>negate</code> : it just takes a <code>bool</code> and returns a <code>bool</code>.
 <br>If we remove the declaration of the global log, all the functions are broken without touching them.
 <br>But let's keep that solution.
 <br>
 <br>It works until a new requirement comes : "Our library must be usable in a multi-threaded environment".
 <br>So let's have a global lock ! But locks don't compose, so we can generate dead-lock situations.
 <br>We are then obliged to deal with the complexity hidden behind this apprently simple solution.
 <br>
 <br>This could not happen in Haskell as all functions are supposed to be pure.
 <br>In C++, this could be implemented as a pure function :

 <div><pre>
 pair&lt;bool,string> negate(bool x, string log){
    return make_pair(!x, log + "not!");
 }
 </pre></div>

 OK, this function is pure, there is no side effects, but it's a bit awkward :
 <ul>
    <li>
        We saw that a function is pure if it can be memoized.
        <br>Memoizing the first version of the function is easy, the argument is a boolean so the lookup table contains two elements.
        <br>For the second version, memoizing the boolean argument is easy, but for the string argument, every time we call it with a diffferent string we have a different result. So to memoize it we should consider all the possible different history of calls.
    </li>
    <li>
        An other problem is the use of <code>+</code> in the code <code>log + "not!"</code>.
        <br>Why should a function like negate should know about appending strings ? It acts locally but it has this element of knowledge that is outside of its scope. The principle of separation of concerns is not respected.
    </li>
 </ul>

 This solution would resolve the preceeding issues :
 <div><pre>
 pair&lt;bool,string> negate(bool x){
    return make_pair(!x, "not!");
 }
 </pre></div>

 But then who does the concatenation of the log ?
 <br>What do we do with these functions ? We compose them.
 <br>
 <br>We can modify the way we compose these functions.
 <br>
 <br>Let's define a new way of composing functions that will take care of composing functions that return these pairs.
 <br>With regular composition, we would write :
 <div><pre>
 function &lt;c(a)> compose(function&lt;b(a)> f, function&lt;c(b)> g){
    return [f, g](a x){
        auto p1 = f(x);
        auto p2 = g(p1);
        return p2;
    }
 }
 </pre></div>

 <ul>
    <li>
        <code>a</code>, <code>b</code> and <code>c</code> are types.
    </li>
    <li>
        The function <code>compose()</code> returns a function which takes an argument of type <code>a</code> and returns an object type <code>c</code>.
    </li>
    <li>
        <code>compose()</code>'s arguments are two functions :
        <br><code>f</code> - takes an argument of type <code>a</code> and returns an object type <code>b</code>
        <br><code>g</code> - takes an argument of type <code>b</code> and returns an object type <code>c</code>
    </li>
    
 </ul>

 That's a higher order function, something new in C++ and java, having functions as arguments and returning function and creating them on the spot.
 <br>
 <br>But we want functions that return pairs (embellished functions)
 <div><pre>
 function &lt;pair&lt;c, string>(a)> compose(function&lt;pair&lt;b, string>(a)> f, function&lt;pair&lt;c, string>(b)> g){
    return [f, g](a x){
        auto p1 = f(x);     // p1 is a pair now
        auto p2 = g(p1.first);
        return make_pair(p2.first, p1.second + p2.second); // log concatenation done here
    }
 }
 </pre></div>

 This new way of composing function takes care of appending the log.
 <br>
 <br>Do we have a category with this composition ?
 <ul>
    <li>
        Is it associative ? In the first parts of the pairs, we are just doing regular composition, which was associative before.
        <br>In the second parts, we do string concatenation, which is associative.
    </li>
    <li>
        Identity is
 <div><pre>
 function pair&lt;a, string> id(a x){
    return make_pair(x, "");
 }
 </pre></div>
        String concatenation is a binary operator that is associative and has a unit. So this works for any monoid.
    </li>
 </ul>

 So we have a category whose objects are types a, b, c... and arrows are not regular functions.
 <br>An arrow from a to b is a function from a to a pair (b, string), an embellished function.
 <br>This is the Kleisli category ; its arrows (the embellished functions) are called the Kleisli arrows. Kleisli arrows can be defined for a lot of embellishements.
 <br>
 <br>This is a view of a <b>monad</b>. These arrows are composable because this embellishement is a monad.
 <br>A monad is just a way of composing special types of functions.
 <br>When we redefine composition, we have this one additional degree of freedom. If we use this additional degree or freedom, we use a monad.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/4.1-terminal-and-initial-objects.html
+++ b/younotes1/4.1-terminal-and-initial-objects.html
@@ -0,0 +1,189 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>4.1: Terminal and initial objects | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="3.2-kleisli-category.html">&larr;</a>
    <a class="next" title="Next" href="4.2-products.html">&rarr;</a>
 </nav>


 <h1>4.1: Terminal and initial objects</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=zer1aFgj4aU">this youtube video</a></div>

 <h2>Recapitulation on Kleisli category</h2>
 We start with a category <code>C</code> and based on this category we build an other category, the Kleisli category <code>K</code>.
 <br>In <code>K</code>, the objects are the same as in <code>C</code>. However, the arrows in <code>K</code> are not the same as the arrows in <code>C</code>. 
 <br>In <code>C</code>, we have a mapping which, for every object, gives an other object.
 <br>We saw a particular case in which for every type <code>a</code>, we assign to it a pair composed by <code>a</code> and a string. <code>a &rarr; (a, string)</code>.
 <br>We make a mapping of types - from type a to type <code>(a, string)</code> - let's call it <code>ma</code> ; we'll see later that this kind of mapping is a <code>functor</code>.
 <br>
 <br>In <code>C</code>, the arrow from <code>a</code> to <code>mb</code> (the embellished arrow) becomes the arrow from <code>a</code> to <code>b</code> in <code>K</code>.
 <br>In a way, we implement an arrow in <code>K</code> in terms of an arrow in <code>C</code>.

 <img src="img/kleisli.jpg" alt="Kleisli category">

 For <code>K</code> to be a category, we need :
 <ul>
    <li>
        Composition ; this is not obvious.
        <br>In <code>C</code>, the arrow from <code>a</code> to <code>mb</code> and the arrow from <code>b</code> to <code>mc</code> do not compose (the end of the first is different from the begining of the second).
        <br>We saw that in this particular case, they compose : first we use the arrow from <code>a</code> to <code>mb</code>, and we get the pair <code>(b, string)</code> ; from this pair we take <code>b</code> and use the arrow from <code>b</code> to <code>mc</code>, and we get the pair <code>(c, string)</code> ; and we combine this by concatenating the two strings to return a pair <code>(c, string1 + string2)</code>.
        <br>This was possible because concatenation composes, but this is not generally true.
        <br>To have composition in <code>K</code>, we must be able to find a way to define composition in the implementation.
    </li>
    <li>
        Identity : we built that defining an arrow from <code>a</code> to <code>ma</code>, which has to be a unit in the new composition we build.
        <br>This was achieved using an empty string.
    </li>
    <li>
        Associativity ; this was possible because string concatenation is associative.
    </li>
 </ul>

 Once all this is established, we can say that <code>K</code> is a category.
 <br>And the mapping <code>m</code> is called a <b>monad</b> ; this is one of the many definition of a <b>monad</b>.

 <h2>Universal construction</h2>

 So we talked about sets, with two views : the category <code>Set</code>, and set theory.
 <br>In set theory, sets are things that have elements ; using the elements, we can define things like functions ; we have empty set, singleton set.
 <br>And then in category Set, we become amnesic, we don't know anymore that sets contain elements. Wa can only talk about arrows. These arrows come from functions in set theory. Every time we have a function between two sets, we have an arrow in the category.
 <br>And we know how to compose functions (the result of a function is the argument of an other function). We use the way functions compose in set theory to determine how arrows compose in our Set category. In the category, we don't know why the arrows compose this way, this knowledge comes from set theory.
 <br>
 <br>But then how can we define things that we know from set theory ? Empty set, singleton set, cartesian product ? All these notions are defined in terms of elements. We have to rediscover all this using only arrows and their composition, nothing else.
 <br>There is a very general method of defining things called <b>universal construction</b>.
 <br>In category theory, we use universal construction to construct a particular kind of object, or a particular kind of arrow, or a particular kind of pattern that we knew in set theory.
 <br>As we can't look inside an object, the only thing we can do is define the properties of an object in terms of relations of this object to every other object of the category. These relations are the arrows incoming to this object or outgoing from this object. We have to think about the whole universe.
 <br>That's what we did when we talked about epimorphisms and automorphisms.
 <br>
 <br>The general method of universal construction is like googling something : you define a pattern, a combination of objects and arrows. It could be a simple pattern, like one object, or an object and an arrow to an other object.
 <br>So you say "here is my pattern, google in this category and show me your hits, everything that matches this pattern". In general we get a lot of results, often an infinity.
 <br>So it's not good enough, we need to rank these results. If we have two hits matching the same pattern, we need to be able to say which one is better than the other. Maybe not all objects are comparable, and this does not guarantee that one object is at the top. But if there is one, then we know that it is the object we were looking for.

 <h2>Terminal object</h2>

 We place ourselves in the <code>Set</code> category and try to find the universal property for the <b>singleton set</b>.
 <br>Singleton set is also called a <b>unit</b> and noted <span class="formula">()</span>.

 <br>How does this set relate to other sets ?

 <br>One interesting property is that it has an incoming arrow coming from every other object in the category. A polymorphic function which ignores its argument and returns a unit. There is even a function from the empty set (<code>void</code>).

 <img src="img/singleton-incoming.jpg" alt="Incoming arrows to a singleton">

 Unfortunately, this property is not limited to empty set. In fact there are arrows from every set to every other set, except for one case : there is no arrow from a non-empty set to empty set.
 <br>For example, there are at least two functions between a set and a two-element set (type <code>bool</code>) : functions that we can call <code>true</code> and <code>false</code>, which ignore the arguments and return <code>true</code> or <code>false</code>.
 <br>
 <br>The difference is that for singleton set, there is only one incoming arrow, a unique arrow from any other set to unit.
 <br>
 <br>Here is an universal property that defines the singleton set.
 <br>
 <br>But this construction involves only arrows, we can forget about sets and apply it to any other category.
 <br>We call the object defined this way a <b>terminal object</b>.
 <br>In every category, we can try to define a terminal object : this is an object that has a unique arrow coming from any other object.
 <br>We'll see that not every category has a terminal object.
 <br>There are two separate conditions :
 <ul>
    <li>
        For all object <code>a</code>, there exists an <code>f</code> that goes from a to the terminal object.
        <div class="formula">&forall; a &exist; f :: a &rarr; ()</div>
    </li>
    <li>
        For every two functions <code>f</code> and <code>g</code> from a to the terminal object, <code>f</code> and <code>g</code> must be equal.
        <div class="formula">&forall; f :: a &rarr; (), g :: a &rarr; () &rArr; f = g</div>
        That's the way to define uniqueness in mathematics : what if I have two things that satisfy a condition ? They have to be equal, so I only have one of them. 
    </li>
 </ul>

 <h4>Example in an order</h4>
 What does a teminal object mean ? Having an arrow from any other object means that the object is <i>less than or equal</i> any other object. So the terminal object must be the largest object.
 <br>Obviously we see that some categories don't have a largest object, for example there is no largest natural number.

 <h2>Initial object</h2>

 We can try to define an empty set, or see what it happens if we invert the arrows of the terminal object. In fact, this is the same question.
 <br>An empty set can be defined by outgoing arrows.
 <br>We call <b>void</b> empty set.
 <br>There is a function going from void to any other type, a tricky function called <b>absurd()</b> : I say that I have this function, try calling it ; give me an element of void and I'll give you an element of a. Since you can't give me an element of void, you can't prove that this function does not exist.

 <img src="img/absurd.jpg" alt="Outgoing arrows from empty set">

 Here we have reversed the definition used for the terminal object.
 <br>The <b>initial object</b> is an object that has a unique outgoing arrow to every other object.
 <br>In the set category, it corresponds to an empty set.
 <br>The definition is similar to terminal object's definition :
 <ul>
    <li>
        For all object <code>a</code>, there exists an <code>f</code> that goes from the initial object to <code>a</code>.
        <div class="formula">&forall; a &exist; f :: void &rarr; a</div>
    </li>
    <li>
        For every two functions <code>f</code> and <code>g</code> from the initial object to <code>a</code>, <code>f</code> and <code>g</code> must be equal
        <div class="formula">&forall; f :: void &rarr; a, g :: void &rarr; a &rArr; f = g</div>
    </li>
 </ul>

 <h3>Unique path</h3>

 In any category that has a terminal object, any path that goes from an object to the terminal object can be replaced by a single arrow. 

 <img src="img/path-to-terminal.jpg" alt="Outgoing arrows from empty set">

 And it's always the same arrow, that's where uniqueness come from : any path can be shrunk to the same unique arrow.
 <br>
 <br>If instead of having void we had the boolean set (two-element set), we would have at least two paths from any object,the true path and the false path.
 <br>
 <br>And the same is true with initial object if we reverse.

 <h3>Uniqueness</h3>

 The next question we might ask is "how many of these objects are there ?"
 <br>Intuitively we can say that there is only one empty set, but for the singleton set, this is not obvious : is the set containg one orange equal to the set containing one apple ? It raises the question of the meaning of equality of two objects. We don't know. It is not part of our thinking about categories. There is no equality of objects. There is equality of arrows. If we have two arrows with the same end and beginning, we can ask the question of their equality. But for objects, equality is not defined.
 <br>Instead we can aks the question "Are they isomorphic ?". Isomorphism is weel defined in every category (if you have two arrows between the objects, one being the invert of the other).
 <br>
 <br>Terminal and initial objects are unique up to an isomorphism. The proofs are almost the same, except inverting the arrows.
 <br>A stronger condition is may be that there is a unique isomorphism between two terminal or two initial objects.
 <br>For example, if we have a set containing true and false, and a set containing black and white, there are two isomorphisms :
 <br>One associates black to true and white to false ; one associates white to true and black to false.

 <h4>Proof for terminal object</h4>

 Suppose we have two terminal objects a and b. Just apply the definition : 
 <br><code>a</code> is a terminal object so there is a unique arrow from any object to <code>a</code>.
 <br>In particular, there will be an arrow from <code>b</code> to <code>a</code> (let's call it <code>g</code>).
 <br>But <code>b</code> is also a terminal object, so there is a unique arrow from <code>a</code> to <code>b</code> (let's call it <code>f</code>).
 <br>Let's call <span class="formula">h = g o f</span> ; it goes from <code>a</code> to <code>b</code> and back to <code>a</code>, so it's a loop from <code>a</code> to <code>a</code>.
 <br>But <code>a</code> is a terminal object, so there is a unique arrow from <code>a</code> to <code>a</code>.
 <br>And we know that there is always an identity for any object, so <code>h = Id</code>.
 <br>So whe have <span class="formula">g o f = Id<sub>a</sub></span>, so f and g are isomorphic.
 <br>Similarily <span class="formula">f o g = Id<sub>b</sub></span>
 <br>And it's a unique isomorphism because <code>f</code> and <code>g</code> are unique (by definition of terminal object).

 <h2>Back to universal constructions</h2>

 This illustrates universal construction. Here the pattern to pick is the simplest possible pattern, an object.
 <br>Show me all the examples of this pattern in your category ; these are all the objects of the category.
 <br>The query is very imprecise, but we have the ranking. We say that a is better than b if there is a unique arrow from b to a.
 <br>Many objects have multiple arrows incomping to them, so they don't compare, the ranking is not a total order.

 <img src="img/terminal-object-selection.jpg" alt="Terminal object selection">

 So the terminal object is better than any other object.
 <br>
 <br>The difference between terminal and initial objects lies only in ranking. The query is the same ("an object"). To rank the initial object we would say that <code>a</code> is better than <code>b</code> if there is an arrow from <code>a</code> to <code>b</code>.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/4.2-products.html
+++ b/younotes1/4.2-products.html
@@ -0,0 +1,143 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>4.2: Products | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="4.1-terminal-and-initial-objects.html">&larr;</a>
    <a class="next" title="Next" href="5.1-coproducts-sum-types.html">&rarr;</a>
 </nav>


 <h1>4.2: Products</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=Bsdl_NKbNnU">this youtube video</a></div>

 <h2>Complement on terminal objects</h2>

 We said that there is a unique incoming arrow from every object to a terminal object, but said nothing about outgoing arrows. There are usually outgoing arrows, and these arrows help us to defined the <b>generalized elements</b> in other objects.
 <br>Every arrow from the terminal object to an other object is a definition of a generalized element in this other object.
 <br>This happens in the Set category : when you map a singleton set to an other set, that's equivalent of picking one element in this set : the element of the singleton set is mapped to a particular element of the other set. There are many morphisms and each of them picks a different element.
 <br>So we can generalize this to other categories saying that if I have a terminal object in a category and morphisms from terminal to other objects, it's like picking an element in the other object, without knowing what an element is.
 <br>It's important because there are many categories similar to the category of sets, and if they have a terminal object, it provides a way of picking elements.

 <h2>Opposite category</h2>

 When we saw universal constructions of terminal and initial objects, we studied in detail terminal objects, and skipped initial objects saysing that it's the same if we invert the arrows.
 <br>This trick of inversing arrows has a deep meaning. Every construction in category theory has its opposite construction that is done by reversing arrows. For example, defining a terminal object gives for free the definition of the initial object by repeating the same thing with inverted arrows..
 <br>This property is related to the fact that for any category wa can always create a new category identical to the first, but with arrows reversed.
 <br>This new category is called the <b>opposite category</b> and is noted <span class="formula">C<sup>op</sub></span>
 <br>The inverse of a function <code>f</code> is noted <span class="formula">f<sup>op</span>
 <br>from every arrow <code>f</code> going from <code>a</code> to <code>b</code> there is an arrow <code>f<sup>op</sup></code> going from <code>b</code> to <code>a</code>.

 <img src="img/opposite-category.jpg" alt="Opposite category">

 But how do we know that C<sup>op</sup> is a category ?
 <ul>
    <li>
        <b>Composition</b> : if we have two arrows <code>f :: a &rarr; b</code> and <code>g :: b &rarr; c</code>, we have their composition <code>g o f :: a &rarr; c</code>.
        <br>We can associate to <code>g o f</code> in the new category <code>(g o f)<sup>op</sup> :: c &rarr; a</code>.
        <div class="formula">(g o f)<sup>op</sup> = f<sup>op</sup> o g<sup>op</sup></div>
    </li>
    <li>
        <b>Identity</b> : when we invert identity, we have identity again.
    </li>
    <li>
        <b>Associativity</b> comes automatically
    </li>
 </ul>

 So instead of defining the initial object in category <code>C</code> we could say that the initial object is the terminal object in the opposite category.

 <h2>Product</h2>
 In the ancient world of set, there is something called the <b>cartesian product</b>.

 <img src="img/product1.jpg" alt="Cartesian product 1">
 The cartesian product of two sets <code>a</code> and <code>b</code> is the set of pairs composed by an element of <code>a</code> and an element of <code>b</code>.
 <br>For example a plane is the cartesian product of x and y axis.

 <img src="img/product2.jpg" alt="Cartesian product 2">

 To express cartesian product in terms of categories, what are the properties ?
 <br>For every cartesian product of two sets, there are these two special functions called <b>projections</b>.
 <br>In Haskell, they are called first (<code>fst</code>) an second (<code>snd</code>).

 <img src="img/product3.jpg" alt="Cartesian product 3">

 So here we have a pattern : <code>a</code> and <code>b</code> are fixed ; the pattern is : pick an object <code>c</code> which has two arrows, one going to <code>a</code> and one going to <code>b</code>. <code>c</code> might be a cartesian product, but we don't know. There may be many other such <code>c</code>. One of them is the cartesian product, which one is the correct one ?
 <br>Universal construction to the rescue, we need to be able to rank them.

 <img src="img/product4.jpg" alt="Cartesian product 4">

 We say that <code>c</code> is better than <code>c'</code> if there is a unique morphism <code>m</code> from <code>c'</code> to <code>c</code> such as
 <br><span class="formula">p o m = p'</span> and <span class="formula">q o m = q'</span>
 <br>With multiplication we would say that <code>p'</code> factorizes <code>p</code> into <code>p</code> times <code>m</code> and <code>q'</code> factorizes <code>q</code> into <code>q</code> times <code>m</code>.
 <br><code>p'</code> and <code>q'</code> have a common factor, <code>m</code>.
 <br><code>m</code> takes the worst of these two projections, condenses them ; <code>m</code> can shrink stuff or not cover. All the non-injectivity or non-surjectivity is concentrated into <code>m</code>.
 <br>
 <br>Back to programming : the real product of <code>a</code> and <code>b</code> is a pair of type <code>(a, b)</code> in Haskell ; expressed as <code>&lt;a,b></code> in C++
 <br>With these two projections 
 <br><code>fst(a, _) = a</code>
 <br><code>snd(_, b) = b</code>
 <br><code>a = Int</code> ; <code>b = Bool</code> ; the product is a pair <code>(Int, Bool)</code>
 <br>
 <br>Examples of bad product : 
 <br>
 <br>Type <code>Int</code> is a bad candidate for product, but it has projections :
 <br><code>p' :: Int &rarr; Int</code>, for example <code>p' = Id</code>
 <br><code>q' :: Int &rarr; Bool</code>, for example <code>q' = True</code>
 <br>So what is the projection <code>m</code> ?
 <br><code>m :: Int &rarr; (Int, Bool)</code>
 <br><code>m x = (x, True)</code>
 <br><code>m</code> is bad because non surjective, it misses the pairs <code>(Int, False)</code>
 <br>
 <br>An other bad candidate is a triple <code>(Int, Int, Bool)</code>
 <br>We can define projections too :
 <br><code>p' :: (Int, Int, Bool) &rarr; Int</code> ; for example <code>p'(x, _, _) = x</code>
 <br><code>q' :: (Int, Int, Bool) &rarr; Bool</code> ; for example <code>q'(_, _, b) = b</code>
 <br>So what is the projection <code>m</code> ?
 <br><code>m :: (Int, Int, Bool) &rarr; Bool</code>
 <br><code>m(x, y, b) = (x, b)</code>
 <br><code>m</code> is bad because non injective
 <br>Each candidate has a flaw, and we can distill these flaws in <code>m</code>.
 <br>
 <br>The definition of product is :
 <br>
 <div style="display:inline-block; border:1px solid black; margin:1em 0 1em 2em;">
    <div style="float:left; padding:1em 0 1em 0;">
        <img src="img/product4.jpg" alt="Cartesian product 4" />
    </div>
    <div style="float:left; padding:1em;">
        A categorical product of two objects <code>a</code> and <code>b</code> is a third object <code>c</code> with two projections
        <br><code>p :: c &rarr; a</code>
        <br><code>q :: c &rarr; b</code>
        <br>Which has the universal property :
        <br>For any object <code>c'</code> with projections
        <br><code>p' :: c' &rarr; a</code>
        <br><code>q' :: c' &rarr; b</code>
        <br>There is a unique morphism <code>m :: c' &rarr; c</code> such as 
        <br><code>p' = p o m</code>
        <br><code>q' = q o m</code>
    </div>
 </div>


 <br>Saying that <code>p' = p o m</code> and <code>q' = q o m</code> is equivalent to say that the diagram <b>commutes</b>.
 <br>We say that a diagram commutes if two paths give the same results.
 <br>
 <br>Not every category has product, and if it has, maybe it doesn't have it for any pair of objects.
 <br>In the category of sets, every two sets have a product.
 <br>If we want to imitate Set category, we will want to have categories which have initial objects, terminal objects, product and coproduct.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/5.1-coproducts-sum-types.html
+++ b/younotes1/5.1-coproducts-sum-types.html
@@ -0,0 +1,103 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>5.1: Coproducts, sum types | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="4.2-products.html">&larr;</a>
    <a class="next" title="Next" href="5.2-algebraic-data-types.html">&rarr;</a>
 </nav>


 <h1>5.1: Coproducts, sum types</h1>

 <div>Notes from <a href="https://www.youtube.com/watch?v=LkIRsNj9T-8">this youtube video</a></div>

 <h2>Coproduct</h2>

 The coproduct is the <b>dual</b> of the product. The dual is the same thing but in the opposite category.
 <br>So we build the product diagram reverting the arrows :

 <img src="img/product4.jpg" alt="Cartesian product 4">

 Instead of having projections <code>p</code> and <code>q</code>, we have <b>injections</b> <code>i</code> and <code>j</code>.
 <br>So this is the pattern : we fix two objects <code>a</code> and <code>b</code>. An object <code>c</code> will match this pattern if it has two arrows coming to it from <code>a</code> and <code>b</code>.
 <br>And to match which candidate is the best, we map the best match <code>c</code> to fake candidates <code>c'</code>.
 <br>The existence of a unique morphism such as the diagram commutes permits to determine the best match.
 <br>Commuting condition is expressed by 
 <div class="formula">
 i' = m o i
 <br>j' = m o j
 </div>

 <h3>In terms of functions</h3>

 What does coproduct mean in set theory ?
 <br>The fact that we have thes injection means that we are embedding the sets <code>a</code> and <code>b</code> into <code>c</code>.
 <br>Functions can shrink things, or not cover their whole codomain, they can be non injective or non surjective ; but we want <code>i</code> and <code>j</code> to be the best fit. We want to embed exactly <code>a</code> and <code>b</code> into <code>c</code>, no more and no less. This is just like the <b>union</b> of <code>a</code> and <code>b</code>.

 <img src="img/union.jpg" alt="Union">

 Every universal construction permits to build the best possible fit, it picks an ideal match.

 But what happens when they overlap ? Or when <code>a</code> = <code>b</code> ?
 <br>The union of a set with itself is the set itself. But there is an other possibility : the <b>discrimated union</b> ; we tag the elements in the discrimated union : this element comes from the left one, this element comes from the right one ; the set is duplicated.
 <br><code>c</code> is in fact a discrimated union because we can easily build a morphism <code>m</code> from discriminated union to union ; <code>m</code> is unique and non-injective.

 <img src="img/discriminated-union1.jpg" alt="Discriminated Union">

 And we could not go the other way round.

 <img src="img/discriminated-union2.jpg" alt="Discriminated Union 2">

 Each element <code>x</code> should be mapped twice, a function can't do that.

 <h3>In terms of types</h3>

 Called a <b>tagged union</b> or <b>variant</b>.
 <br>In many programming languages you have a union ; if you take the union of Integer and boolean, you will have either an integer or a boolean, not both.
 <br>The simplest example is an enumeration, which is a union of things.
 <br>
 <br>So the canonical way to build a product is a pair, built into the language.
 <br>A union, also called a <b>sum type</b>, is not usually built into the language but is easy to define.
 <br>The canonical definition of a sum type of two types is called <code>Either</code>, taking in parameters two types <code>a</code> and <code>b</code>.
 <br>In Haskell, <code>data Either = Left a | Right b</code> (Left a or Right b) ; <code>Left</code> and <code>Right</code> corresponds to injections <code>p</code> and <code>q</code>.
 <br>In C++ we would define a class with two constructors.
 <br>
 <br>This is a dual picture ; in product we have the functions <code>fst</code> and <code>snd</code> which can destroy the pair, extract and see what's inside a pair.
 In coproduct we have functions which construct an <code>Either</code>. But can we extract stuff from an <code>Either</code> ?
 <br>If we have an <code>x :: Either Int Bool</code>, to extract an Int, we need to write code that takes into account both possibilities, that will match either Right or Left ; this is called <b>pattern matching</b> ; Left and right are patterns.

 <h2>The type system</h2>

 Now that we have product type, sum type, unit type, void, we have pretty much of the foundations of the type system.
 <br>
 <br>Product types are the most visible ones, they may be built-in in Haskell or defined with generics in C++.
 <br>All these constructs in Haskell are equivalent to a product : they store two floats, no more and no less.

 <div><pre>
 data Point = (Float, FLoat)
 data Point = P Float Float
 data Point{
    x :: Float,
    y :: Float
 }
 </pre></div>

 <br>Why are these called products and sums ?
 <br>A product comes from cartesian product, so it's undersandable.
 <br>Coproduct is a union, which is a kind of sum of two sets.
 <br>This will be precised in the next course.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/5.2-algebraic-data-types.html
+++ b/younotes1/5.2-algebraic-data-types.html
@@ -0,0 +1,145 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>5.2: Algebraic data types | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>

 <body>

 <nav class="prevnext">
    <a class="top" title="Index" href="../index.html">&uarr;</a>
    <a class="prev" title="Previous" href="5.1-coproducts-sum-types.html">&larr;</a>
    <a class="next" title="Next" href="6.1-functors.html">&rarr;</a>
 </nav>


 <h1>5.2: Algebraic data types</h1>

 <div>Notes from <a href="">this youtube video</a></div>


 <h2>Product</h2>

 Why is it an algebra ?
 <br>We have products and sums just like in algebra.
 <br>Product is sort of multiplication. It means that we have at least a <b>monoid</b>.
 <br>A monoid has an operation (here multiplication) that is associative and has a unit.
 <br>But does the product in types behave like multiplication ?

 <ul class="spaced">
    <li><b>Symetry</b> (this is not needed for a monoid)
        <br>The product of numbers is symetric, but this is not true for the product of two types :
        <br>If we have types <code>a</code> and <code>b</code>, the pair <code>(a, b)</code> is different from <code>(b,a)</code>. However they contain the same information, which means that they are isomorphic ; the isomorphism is called <code>swap</code>.
 <div><pre>
 swap :: (a, b) &rarr; (b, a)
 swap p  = (snd p, fst p)
 </pre></div>
        The inverse of <code>swap</code> is <code>swap</code>.
        <br>So multiplication is symetric up to isomorphism.
    </li>

    <li>
        <b>Associativity</b>
        <br>Are <code>((a, b), c)</code> and <code>(a, (b, c))</code> equivalent ? No.
        <br>No but these two types contain the same information, but re-arranged ; they are isomorphic.
        <div><pre>assoc :: ((a, b), c) = (a, (b, c))</pre></div>
        This function is an isomorphism, it has an inverse.
        <br>Associativity means that we can omit parentheses and simply write <code>(a, b, c)</code>.
        <br>So we just have tuples ; structs or records with multiple fields are just examples of this.
        <br>In classical algebra, this corresponds to <code>(a * b) * c = a * (b * c)</code>
    </li>
    
    <li>
        <b>Unit</b>
        <br>What would be the type, which paired with any other type would give the same type ? This type should have only one element.
        <br><code>(a, ())</code> is isomorphic to <code>a</code>.
 <div><pre>
 munit(x, ()) = x
 munit_inv(x) = (x, ())
 </pre></div>
        It's like taking the cartesian product of a line and a point, it gives a line (not exactly the same line).
        <br>What we did for right unit can be done for left unit.
        <br>In classical algebra, this corresponds to <code>a * 1 = a</code>
    </li>
 </ul>

 So we have a monoid with respect to product.

 <h2>Sum</h2>

 <ul class="spaced">
    <li>
        <b>Symetry</b>
        <br><code>Either a b ~ Either b a</code> ; isomorphic
    </li>
    
    <li>
        <b>Associativity</b>
        <br>Similarily it is also associative up to isomorphism.
        <br>If we want to associate Eithers we can write data structures like
        <div><pre>data Triple = Left a | Middle b | Right c</pre></div>
    </li>
    
    <li>
        <b>Unit</b>
        <br>The unit of sum is <code>Void</code>.
        <br><code>Either a Void</code> is isomorphic to a.
        <br>In classical algebra, corresponds to <code>a + 0 = a</code>.
    </li>
 </ul>

 <h2>Algebra</h2>

 So we have a second monoid. That's not all, we would like to combine these two monoids into something bigger.
 <br>
 <br>From algebra we have <code>a * 0 = 0</code>
 <br>Is it true with types ? Is <code>(a, Void)</code> isomorphic to <code>Void</code> ?
 <br>Constructing a pair (a, Void) is impossible because we can't give an element of type <code>Void</code> ; this pair is inhabited, which is the same as <code>Void</code>.
 <br>
 <br>From algebra we also have distributivity : <code>a * (b + c) = a * b + a * c</code>.
 <br>This is true, up to an isomorphism : <code>(a, Either b c) ~ Either (a, b) (a, c)</code>.
 <br>
 <br>A structure lke this in algebra is called a <b>ring</b>, except that in a true ring, addition and multiplication have an inverse. Here we don't know how to substract something or divide by something.
 <br>A structure like that is called a <b>rig</b> or <b>semi-ring</b>.
 <br>
 <br>What is the correspondance of <code>2 = 1 + 1</code> ?
 <br>1 is the unit type. There are two possible values : left unit or right unit. We can call left unit <code>true</code>, and right unit <code>false</code>. 2 is isomorphic to a boolean.
 <br>
 <br>What is the correspondance of <code>2 = 1 + a</code> ?
 <br>This is <code>Maybe</code> :
 <br><code>data Maybe a = Nothing | Just a</code>.
 <br>This has two constructors ; <code>Nothing</code> takes no argument, so it's equivalent to Unit.
 <br>So <code>Maybe a</code> is equivalent to <code>Either () a</code>.
 <br>
 <br>Let's see an equation :
 <br><code>l(a) = 1 + a * l(a)</code>
 <br>Which can be solved as follows :
 <br><code>l(a) - a * l(a) = 1</code>
 <br><code>l(a) * (1 - a) = 1</code>
 <br><code>l(a) = 1 / (1 - a)</code>
 <br>
 <br>Expressed as type, this gives :
 <br><code>data List a = Nil | Cons a (List a)</code>
 <br>A list of <code>a</code> is either empty or it's a Cons of head and tail.
 <br><code>List</code> a is a sum constructor (|)
 <br><code>Nil</code> is a constructor that takes no argument, which corresponds to Unit type.
 <br><code>Cons</code> is a product constructor, it takes two types as arguments.
 <br>
 <br>To solve this equation with types, we cannot do division or substraction.
 <br>But <code>l(a) = 1 / (1 - a)</code> happens to be the sum of a geometric sequence : <code>1 + a + a*a + a*a*a + ...</code>
 <br><code>1</code> corresponds to empty list ; <code>a</code> is a singleton list ; <code>a*a</code> is a list of 2 elements ; <code>a*a*a</code> is a list of 3 elements...
 <br>With this equation we have defined all possible lists.
 <br>
 <br>The equation : <code>l(a) = 1 + a * l(a)</code> can be solved by substitution :
 <br>Using classical algebraic notation :
 <br><code>l(a) = 1 + a * (1 + a * l(a)) = 1 + a + a * a * (1 + a * l(a))</code> ...
 <br>This is a way of doing the same thing without doing the power series.

 <!-- ********************************************************************************* -->
 <!-- ************************************* -->
 </body>
 </html>
--- a/younotes1/6.1-functors.html
+++ b/younotes1/6.1-functors.html
@@ -0,0 +1,171 @@
 <!DOCTYPE html>
 <html lang="en">
 <head>
    <meta charset="utf-8" />
    <title>6.1: Functors | Categories Bartosz Milewski Youtube notes</title>
    <link rel="shortcut icon" href="favicon.png" type="image/x-icon">
    <link rel="copyright" href="http://www.gnu.org/copyleft/gpl.html"/>
    <link href="../static/style.css" rel="stylesheet" type="text/css">
 </head>