(no commit message)

diff --git a/topics/week5_system_F.mdwn b/topics/week5_system_F.mdwn
index 36c071c..c20b61c 100644 (file)
--- 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`
 
 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
 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