X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;f=topics%2Fweek7_introducing_monads.mdwn;h=1dbd5101872f6245b30b145ae4718680900d75a6;hb=f283b53c6b5bf64e0c5cf06799951f85b981f862;hp=244793ff2b49620057e69bc0951be07c6a0a5082;hpb=7cdd4e2e306a7ceeb5cb2ebe423a2e8395283274;p=lambda.git

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 244793ff..1dbd5101 100644
--- a/topics/week7_introducing_monads.mdwn
+++ b/topics/week7_introducing_monads.mdwn
@@ -161,24 +161,24 @@ definitions:
 
 Identity is a monad.  Here is a demonstration that the laws hold:
 
-    mcomp mid k == (\fgx.f(gx)) (\p.p) k
-                ~~> \x.(\p.p)(kx)
-                ~~> \x.kx
-                ~~> k
-    mcomp k mid == (\fgx.f(gx)) k (\p.p)
-                ~~> \x.k((\p.p)x)
-                ~~> \x.kx
-                ~~> k
-    mcomp (mcomp j k) l == mcomp ((\fgx.f(gx)) j k) l
-                       ~~> mcomp (\x.j(kx)) l
-                        == (\fgx.f(gx)) (\x.j(kx)) l
-                       ~~> \x.(\x.j(kx))(lx)
-                       ~~> \x.j(k(lx))
-    mcomp j (mcomp k l) == mcomp j ((\fgx.f(gx)) k l)
-                       ~~> mcomp j (\x.k(lx))
-                        == (\fgx.f(gx)) j (\x.k(lx))
-                       ~~> \x.j((\x.k(lx)) x)
-                       ~~> \x.j(k(lx))
+    mcomp mid k ≡ (\fgx.f(gx)) (\p.p) k
+              ~~> \x.(\p.p)(kx)
+              ~~> \x.kx
+              ~~> k
+    mcomp k mid ≡ (\fgx.f(gx)) k (\p.p)
+              ~~> \x.k((\p.p)x)
+              ~~> \x.kx
+              ~~> k
+    mcomp (mcomp j k) l ≡ mcomp ((\fgx.f(gx)) j k) l
+                      ~~> mcomp (\x.j(kx)) l
+                        ≡ (\fgx.f(gx)) (\x.j(kx)) l
+                      ~~> \x.(\x.j(kx))(lx)
+                      ~~> \x.j(k(lx))
+    mcomp j (mcomp k l) ≡ mcomp j ((\fgx.f(gx)) k l)
+                      ~~> mcomp j (\x.k(lx))
+                        ≡ (\fgx.f(gx)) j (\x.k(lx))
+                      ~~> \x.j((\x.k(lx)) x)
+                      ~~> \x.j(k(lx))
 
 The Identity Monad is favored by mimes.
 
@@ -393,5 +393,5 @@ theory of accommodation, and a theory of the situations in which
 material within the sentence can satisfy presuppositions for other
 material that otherwise would trigger a presupposition violation; but,
 not surprisingly, these refinements will require some more
-sophisticated techniques than the super-simple Option monad.)
+sophisticated techniques than the super-simple Option/Maybe monad.)