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.
 
 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*.
 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*.