X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=539017ea0d35488b5810cdb19d4fa667cecedd5a;hp=4517509b28236e8cab4d3c4123b4e03c5be348c5;hb=ff8ade136061e84890099464dc05206a8ecaeb98;hpb=293b63f453994f8c3c458ca264ef0fb04b79e1fb

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 4517509b..539017ea 100644
--- 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*.