week2: ~~>_eta

Signed-off-by: Jim Pryor <profjim@jimpryor.net>

diff --git a/week2.mdwn b/week2.mdwn
index 1e3aa2b..eedc6de 100644 (file)
--- a/week2.mdwn
+++ b/week2.mdwn
@@ -318,6 +318,8 @@ will eta-reduce by n steps to:
 
        \x. M
 
 
        \x. M
 

+When we add eta-reduction to our proof system, we end up reconstruing the meaning of `~~>` and `<~~>` and "normal form", all in terms that permit eta-reduction as well. Sometimes these expressions will be annotated to indicate whether only beta-reduction is allowed (<code>~~><sub>&beta;</sub></code>) or whether both beta- and eta-reduction is allowed (<code>~~><sub>&beta;&eta;</sub></code>).
+

 The logical system you get when eta-reduction is added to the proof system has the following property:
 
 >      if `M`, `N` are normal forms with no free variables, then <code>M &equiv; N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.
 The logical system you get when eta-reduction is added to the proof system has the following property:
 
 >      if `M`, `N` are normal forms with no free variables, then <code>M &equiv; N</code> iff `M` and `N` behave the same with respect to every possible sequence of arguments.