X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=0dcb0957803ffa0855c51e792a0c0979a4590683;hp=4bde11e08fbdec51ebd083d13cc5fdd2c9089a48;hb=4d9fe4645917a4966694c7c4bf8edde8b243745f;hpb=447c097435042d6895c2cf7e861ec119a2f20b63

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 4bde11e0..0dcb0957 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*.