X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2Fweek5_system_F.mdwn;fp=topics%2Fweek5_system_F.mdwn;h=c20b61c546b64b2c2e30bf6a80d98d0fc66113d9;hp=36c071cd9e305f2f9ac1e0edc2e2a7daf8c2e1d1;hb=34942572995dfda43937082cbb6d7addc323e8e6;hpb=ef351afc1578508e294f73be1c2f2445463d6383

diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index 36c071cd..c20b61c5 100644
--- a/topics/week5_system_F.mdwn
+++ b/topics/week5_system_F.mdwn
@@ -122,7 +122,7 @@ Exercise: convince yourself that `zero` has type `N`.
 
 The key to the extra expressive power provided by System F is evident
 in the typing imposed by the definition of `pred`.  The variable `n`
-is typed as a Church number, i.e., as `N ≡ ∀α.(α->α)->α->α`.
+is typed as a Church number, i.e., as <code>N &equiv; ∀α.(α->α)->α->α</code>.
 The type application `n [Pair]` instantiates `n` in a way that allows
 it to manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`.
 In other words, the instantiation turns a Church number into a certain