remove spaces after applications of mid

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index b7e962a..49993ff 100644 (file)
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -171,27 +171,27 @@ has to obey the following Map Laws:
        Moreover, with `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.) These
        have to obey the following MapN Laws:
 
        Moreover, with `map2` in hand, `map3`, `map4`, ... `mapN` are easily definable.) These
        have to obey the following MapN Laws:
 

-    1. <code>⇧ (id : P->P) : <u>P</u> -> <u>P</u></code> is a left identity for `¢`, that is: `(⇧ id) ¢ xs = xs`
-    2. `⇧ (f a) = (⇧ f) ¢ (⇧ a)`
-    3. The `map2`ing of composition onto boxes `fs` and `gs` of functions, when `¢`'d to a box `xs` of arguments == the `¢`ing of `fs` to the `¢`ing of `gs` to xs: `(⇧ (○) ¢ fs ¢ gs) ¢ xs = fs ¢ (gs ¢ xs)`.
-    4. When the arguments (the right-hand operand of `¢`) are an `⇧`'d value, the order of `¢`ing doesn't matter: `fs ¢ (⇧ x) = ⇧ ($x) ¢ fs`. (Though note that it's `⇧ ($x)`, or `⇧ (\f. f x)` that gets `¢`d onto `fs`, not the original `⇧ x`.) Here's an example where the order *does* matter: `[succ,pred] ¢ [1,2] == [2,3,0,1]`, but `[($1),($2)] ¢ [succ,pred] == [2,0,3,1]`. This Law states a class of cases where the order is guaranteed not to matter.
-    5. A consequence of the laws already stated is that when the _left_-hand operand of `¢` is a `⇧`'d value, the order of `¢`ing doesn't matter either: `⇧ f ¢ xs == map (flip ($)) xs ¢ ⇧ f`.
+    1. <code>⇧(id : P->P) : <u>P</u> -> <u>P</u></code> is a left identity for `¢`, that is: `(⇧id) ¢ xs = xs`
+    2. `⇧(f a) = (⇧f) ¢ (⇧a)`
+    3. The `map2`ing of composition onto boxes `fs` and `gs` of functions, when `¢`'d to a box `xs` of arguments == the `¢`ing of `fs` to the `¢`ing of `gs` to xs: `(⇧(○) ¢ fs ¢ gs) ¢ xs = fs ¢ (gs ¢ xs)`.
+    4. When the arguments (the right-hand operand of `¢`) are an `⇧`'d value, the order of `¢`ing doesn't matter: `fs ¢ (⇧x) = ⇧($x) ¢ fs`. (Though note that it's `⇧($x)`, or `⇧(\f. f x)` that gets `¢`d onto `fs`, not the original `⇧x`.) Here's an example where the order *does* matter: `[succ,pred] ¢ [1,2] == [2,3,0,1]`, but `[($1),($2)] ¢ [succ,pred] == [2,0,3,1]`. This Law states a class of cases where the order is guaranteed not to matter.
+    5. A consequence of the laws already stated is that when the _left_-hand operand of `¢` is a `⇧`'d value, the order of `¢`ing doesn't matter either: `⇧f ¢ xs == map (flip ($)) xs ¢ ⇧f`.

 
 <!-- Probably there's a shorter proof, but:
 
 <!-- Probably there's a shorter proof, but:

-   ⇧ T ¢ xs ¢ ⇧ f
-== ⇧ T ¢ ((⇧ id) ¢ xs) ¢ ⇧ f, by 1
-== ⇧ (○) ¢ ⇧ T ¢ ⇧ id ¢ xs ¢ ⇧ f, by 3
-== ⇧ ($id) ¢ (⇧ (○) ¢ ⇧ T) ¢ xs ¢ ⇧ f, by 4
-== ⇧ (○) ¢ ⇧ ($id) ¢ ⇧ (○) ¢ ⇧ T ¢ xs ¢ ⇧ f, by 3
-== ⇧ ((○) ($id)) ¢ ⇧ (○) ¢ ⇧ T ¢ xs ¢ ⇧ f, by 2
-== ⇧ ((○) ($id) (○)) ¢ ⇧ T ¢ xs ¢ ⇧ f, by 2
-== ⇧ id ¢ ⇧ T ¢ xs ¢ ⇧ f, by definitions of ○ and $
-== ⇧ T ¢ xs ¢ ⇧ f, by 1
-== ⇧ ($f) ¢ (⇧ T ¢ xs), by 4
-== ⇧ (○) ¢ ⇧ ($f) ¢ ⇧ T ¢ xs, by 3
-== ⇧ ((○) ($f)) ¢ ⇧ T ¢ xs, by 2
-== ⇧ ((○) ($f) T) ¢ xs, by 2
-== ⇧ f ¢ xs, by definitions of ○ and $ and T == flip ($)
+   ⇧T ¢ xs ¢ ⇧f
+== ⇧T ¢ ((⇧id) ¢ xs) ¢ ⇧f, by 1
+== ⇧(○) ¢ ⇧T ¢ ⇧id ¢ xs ¢ ⇧f, by 3
+== ⇧($id) ¢ (⇧(○) ¢ ⇧T) ¢ xs ¢ ⇧f, by 4
+== ⇧(○) ¢ ⇧($id) ¢ ⇧(○) ¢ ⇧T ¢ xs ¢ ⇧f, by 3
+== ⇧((○) ($id)) ¢ ⇧(○) ¢ ⇧T ¢ xs ¢ ⇧f, by 2
+== ⇧((○) ($id) (○)) ¢ ⇧T ¢ xs ¢ ⇧f, by 2
+== ⇧id ¢ ⇧T ¢ xs ¢ ⇧f, by definitions of ○ and $
+== ⇧T ¢ xs ¢ ⇧f, by 1
+== ⇧($f) ¢ (⇧T ¢ xs), by 4
+== ⇧(○) ¢ ⇧($f) ¢ ⇧T ¢ xs, by 3
+== ⇧((○) ($f)) ¢ ⇧T ¢ xs, by 2
+== ⇧((○) ($f) T) ¢ xs, by 2
+== ⇧f ¢ xs, by definitions of ○ and $ and T == flip ($)

 -->
 
 *   ***Monad*** (or "Composables") A MapNable box type is a *Monad* if there
 -->
 
 *   ***Monad*** (or "Composables") A MapNable box type is a *Monad* if there


@@ -214,7 +214,7 @@ has to obey the following Map Laws:
 
         u >>= (\a -> k a >>= j) == (u >>= k) >>= j
         u >>= ⇧ == u
 
         u >>= (\a -> k a >>= j) == (u >>= k) >>= j
         u >>= ⇧ == u

-        ⇧ a >>= k == k a
+        ⇧a >>= k == k a

 
     (Also, Haskell calls `⇧` `return` or `pure`, but we've stuck to our terminology in this context.) Some authors try to make the first of those Laws look more symmetrical by writing it as:
 
 
     (Also, Haskell calls `⇧` `return` or `pure`, but we've stuck to our terminology in this context.) Some authors try to make the first of those Laws look more symmetrical by writing it as:
 


@@ -271,11 +271,11 @@ j >=> k ≡= \a. (j a >>= k)
 u >>= k == (id >=> k) u; or ((\(). u) >=> k) ()
 u >>= k == join (map k u)
 join w == w >>= id
 u >>= k == (id >=> k) u; or ((\(). u) >=> k) ()
 u >>= k == join (map k u)
 join w == w >>= id

-map2 f xs ys == xs >>= (\x. ys >>= (\y. ⇧ (f x y)))
+map2 f xs ys == xs >>= (\x. ys >>= (\y. ⇧(f x y)))

 map2 f xs ys == (map f xs) ¢ ys, using ¢ as an infix operator
 fs ¢ xs == fs >>= (\f. map f xs)
 ¢ == map2 id
 map2 f xs ys == (map f xs) ¢ ys, using ¢ as an infix operator
 fs ¢ xs == fs >>= (\f. map f xs)
 ¢ == map2 id

-map f xs == ⇧ f ¢ xs
+map f xs == ⇧f ¢ xs

 map f u == u >>= ⇧ ○ f
 </pre>
 
 map f u == u >>= ⇧ ○ f
 </pre>
 


@@ -414,7 +414,7 @@ For the first failure, we noted that it's easy to define a `map` operation for t
 
 But if on the other hand, your box type is `α -> R`, you'll find that there is no way to define a `map` operation that takes arbitrary functions of type `P -> Q` and values of the boxed type <code><u>P</u></code>, that is `P -> R`, and returns values of the boxed type <code><u>Q</u></code>.
 
 
 But if on the other hand, your box type is `α -> R`, you'll find that there is no way to define a `map` operation that takes arbitrary functions of type `P -> Q` and values of the boxed type <code><u>P</u></code>, that is `P -> R`, and returns values of the boxed type <code><u>Q</u></code>.
 

-For the second failure, that is cases of Mappables that are not MapNables, we cited box types like `(R, α)`, for arbitrary fixed types `R`. The `map` operation for these is defined by `map f (r,a) = (r, f a)`. For certain choices of `R` these can be MapNables too. The easiest case is when `R` is the type of `()`. But when we look at the MapNable Laws, we'll see that they impose constraints we cannot satisfy for *every* choice of the fixed type `R`. Here's why. We'll need to define `⇧ a = (r0, a)` for some specific `r0` of type `R`. The choice can't depend on the value of `a`, because `⇧` needs to work for `a`s of _any_ type. Then the MapNable Laws will entail:
+For the second failure, that is cases of Mappables that are not MapNables, we cited box types like `(R, α)`, for arbitrary fixed types `R`. The `map` operation for these is defined by `map f (r,a) = (r, f a)`. For certain choices of `R` these can be MapNables too. The easiest case is when `R` is the type of `()`. But when we look at the MapNable Laws, we'll see that they impose constraints we cannot satisfy for *every* choice of the fixed type `R`. Here's why. We'll need to define `⇧a = (r0, a)` for some specific `r0` of type `R`. The choice can't depend on the value of `a`, because `⇧` needs to work for `a`s of _any_ type. Then the MapNable Laws will entail:

 
     1. (r0,id) ¢ (r,x) == (r,x)
     2. (r0,f x) == (r0,f) ¢ (r0,x)
 
     1. (r0,id) ¢ (r,x) == (r,x)
     2. (r0,f x) == (r0,f) ¢ (r0,x)