edits

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 4bde11e..0dcb095 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -9,23 +9,6 @@ simply-typed lambda calculus as a way of expressing natural language
 meaning.  So we will need to get more sophisticated about types.  The
 next step in that journey will be to consider System F.
 
-In the simply-typed lambda calculus, we write types like <code>&sigma;
--> &tau;</code>.  This looks like logical implication.  We'll take
-that resemblance seriously when we discuss the Curry-Howard
-correspondence.  In the meantime, note that types respect modus
-ponens: 
-
-<pre>
-Expression    Type      Implication
------------------------------------
-fn            &alpha; -> &beta;    &alpha; &sup; &beta;
-arg           &alpha;         &alpha;
-------        ------    --------
-(fn arg)      &beta;         &beta;
-</pre>
-
-The implication in the right-hand column is modus ponens, of course.
-
 System F was discovered by Girard (the same guy who invented Linear
 Logic), but it was independently proposed around the same time by
 Reynolds, who called his version the *polymorphic lambda calculus*.