From 53f10e967ccbf9405baa35d5247079e8776ea279 Mon Sep 17 00:00:00 2001 From: "Yann Esposito (Yogsototh)" Date: Thu, 6 Dec 2012 19:12:58 +0100 Subject: [PATCH] revert to zsh version(s) back --- categories.html | 33 ++++++++++++------- categories/10_Introduction/020_Plan.html | 1 + .../140_Untyped_Pure_Programming.html | 2 +- .../200_Type_Theory_Categories.html | 18 +++++++--- .../180_Monads_are_just_monoids_1_4.html | 12 +++---- .../30_How/180_Monads_are_just_monoids_1_4.md | 12 +++---- 6 files changed, 48 insertions(+), 30 deletions(-) diff --git a/categories.html b/categories.html index 5bdba5d..3f10073 100644 --- a/categories.html +++ b/categories.html @@ -92,6 +92,7 @@
  • General overview
  • Math & Abstraction
  • Programming & Abstraction
    • +
  • Categories & Abstraction
  • What?
    • @@ -316,7 +317,7 @@ Theory=(Axioms,StringsRules,
  • Y = λf.(λx.f (x x)) (λx.f (x x)) +
  • Y = λf.(λx.f (x x)) (λx.f (x x))
  • Y g = g (Y g)
    • @@ -390,11 +391,19 @@ type Product = Product {getProduct :: a} -- Just a named box
    -

    Type Theory & Categories

    -
    typed λ-calculus cartesian closed categories -
    untyped λ-calculus C-monoids (subclass of categories) -
    Martin-Löf type theories locally cartesian closed categories -
    +

    Type Theory ⇒ Categories

    + +
      +
    • Type theory helped to remove paradoxes in Set Theory.
      • +
    • Prevent relations between different kind of objects.
      • +
    • Used in computer science
      • +
    + +
      +
    • typed λ-calculus ⇒ cartesian closed categories
      • +
    • untyped λ-calculus ⇒ C-monoids (subclass of categories)
      • +
    • Martin-Löf type theories ⇒ locally cartesian closed categories
      • +

    Plan

    @@ -886,16 +895,16 @@ Haskell types is fractal:

    Monads are just monoids (1/4)

    -

    A monoid is a triplet \((M,⊙,e)\) s.t.

    +

    A monoid is a triplet \((E,∙,e)\) s.t.

      -
    • \(M\) a set
      • -
    • \(⊙:E×E→M\)
      • -
    • \(e:1→M\)
      • +
    • \(E\) a set
      • +
    • \(∙:E×E→E\)
      • +
    • \(e:1→E\)

    Satisfying

      -
    • \(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\)
      • -
    • \(e⊙x = x = x⊙e, ∀x∈M\)
      • +
    • \(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\)
      • +
    • \(e∙x = x = x∙e, ∀x∈E\)
    diff --git a/categories/10_Introduction/020_Plan.html b/categories/10_Introduction/020_Plan.html index e2e41cc..2037f71 100644 --- a/categories/10_Introduction/020_Plan.html +++ b/categories/10_Introduction/020_Plan.html @@ -5,6 +5,7 @@
  • General overview
  • Math & Abstraction
  • Programming & Abstraction
    • +
  • Categories & Abstraction
  • What?
    • diff --git a/categories/10_Introduction/140_Untyped_Pure_Programming.html b/categories/10_Introduction/140_Untyped_Pure_Programming.html index 20d6d20..596d638 100644 --- a/categories/10_Introduction/140_Untyped_Pure_Programming.html +++ b/categories/10_Introduction/140_Untyped_Pure_Programming.html @@ -4,7 +4,7 @@
  • Mostly static constructions like pipes.
  • All pipes can be plugged ⇒ all error at runtime
    • (+ 37 "foo") -
    • Y = λf.(λx.f (x x)) (λx.f (x x)) +
    • Y = λf.(λx.f (x x)) (λx.f (x x))
    • Y g = g (Y g)
    • diff --git a/categories/10_Introduction/200_Type_Theory_Categories.html b/categories/10_Introduction/200_Type_Theory_Categories.html index 5ed7049..f21b2ac 100644 --- a/categories/10_Introduction/200_Type_Theory_Categories.html +++ b/categories/10_Introduction/200_Type_Theory_Categories.html @@ -1,5 +1,13 @@ -

    Type Theory & Categories

    -
    typed λ-calculus cartesian closed categories -
    untyped λ-calculus C-monoids (subclass of categories) -
    Martin-Löf type theories locally cartesian closed categories -
    +

    Type Theory ⇒ Categories

    + +
      +
    • Type theory helped to remove paradoxes in Set Theory.
      • +
    • Prevent relations between different kind of objects.
      • +
    • Used in computer science
      • +
    + +
      +
    • typed λ-calculus ⇒ cartesian closed categories
      • +
    • untyped λ-calculus ⇒ C-monoids (subclass of categories)
      • +
    • Martin-Löf type theories ⇒ locally cartesian closed categories
      • +
    diff --git a/categories/30_How/180_Monads_are_just_monoids_1_4.html b/categories/30_How/180_Monads_are_just_monoids_1_4.html index ab0d225..f561e6f 100644 --- a/categories/30_How/180_Monads_are_just_monoids_1_4.html +++ b/categories/30_How/180_Monads_are_just_monoids_1_4.html @@ -1,12 +1,12 @@

    Monads are just monoids (1/4)

    -

    A monoid is a triplet \((M,⊙,e)\) s.t.

    +

    A monoid is a triplet \((E,∙,e)\) s.t.

      -
    • \(M\) a set
      • -
    • \(⊙:E×E→M\)
      • -
    • \(e:1→M\)
      • +
    • \(E\) a set
      • +
    • \(∙:E×E→E\)
      • +
    • \(e:1→E\)

    Satisfying

      -
    • \(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\)
      • -
    • \(e⊙x = x = x⊙e, ∀x∈M\)
      • +
    • \(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\)
      • +
    • \(e∙x = x = x∙e, ∀x∈E\)
    diff --git a/categories/30_How/180_Monads_are_just_monoids_1_4.md b/categories/30_How/180_Monads_are_just_monoids_1_4.md index e456c23..4a4b0b5 100644 --- a/categories/30_How/180_Monads_are_just_monoids_1_4.md +++ b/categories/30_How/180_Monads_are_just_monoids_1_4.md @@ -1,13 +1,13 @@ Monads are just monoids (1/4) ----------------------------- -A monoid is a triplet \\((M,⊙,e)\\) s.t. +A monoid is a triplet \\((E,∙,e)\\) s.t. -- \\(M\\) a set -- \\(⊙:E×E→M\\) -- \\(e:1→M\\) +- \\(E\\) a set +- \\(∙:E×E→E\\) +- \\(e:1→E\\) Satisfying -- \\(x⊙(y⊙z) = (x⊙y)⊙z, ∀x,y,z∈M\\) -- \\(e⊙x = x = x⊙e, ∀x∈M\\) +- \\(x∙(y∙z) = (x∙y)∙z, ∀x,y,z∈E\\) +- \\(e∙x = x = x∙e, ∀x∈E\\)