From: jim <jim@web>
Date: Thu, 19 Mar 2015 16:07:30 +0000 (-0400)
Subject: replace some == with &equiv;
X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=commitdiff_plain;h=dc3c0aad5b47d74089d6097bb062f6bfe3fea7dd;hp=7cdd4e2e306a7ceeb5cb2ebe423a2e8395283274

replace some == with &equiv;
---

diff --git a/topics/week7_introducing_monads.mdwn b/topics/week7_introducing_monads.mdwn
index 244793ff..b74ccff0 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.