--- a/slide.md	Tue May 20 16:08:38 2014 +0900
+++ b/slide.md	Tue May 20 16:16:30 2014 +0900
@@ -14,10 +14,10 @@
 # セミナーについて必要する事前知識
 * なお、このセミナーについては
   * C や Java によるプログラミング言語を書いたことがある
-    * 関数や引数、型といった単語への詳細は省略することがあります
+    * 関数や引数、型といった単語の詳細は省略することがあります
   * 数学における述語論理
     * P ならば Q といった論理
-* ことを前提条件としています
+* といったことを前提条件としています
 
 
 # Agda とはどういう言語なのか
@@ -37,7 +37,7 @@
 * 関数と命題の対応を Curry-Howard Isomorphism と言います
 
 
-# A ならば B と A が成り立つのなら B が成りたつ
+# 'A ならば B' と 'A' が成り立つなら 'B'
 
 * Agda において
   * apply : A -> (A -> B) -> B
@@ -74,19 +74,19 @@
 # 関数の定義を C の Syntax 書くと
 * apply : A -> (A -> B) -> B
 
-* B apply(A a, B ( * apply )(A))
-* これを満たす B を関数の定義で書けば良い
-* 証明 == 返り値を返す なので
+* B apply(A a, B ( * f )(A))
+* これを満たす定義を関数applyの実装として書けば良い
+* 証明 == 正しい返り値を返す なので
 * つまりコンパイルを通してしまえば良い
 
 
 # Agda で書いてみると
 
 * emacs から使うと良いです
-* module <filename> where
+* module < filename > where
 * を先頭に書く必要があります
-* 下に証明を定義していく
-* C-c C-l で型チェック
+* 証明を定義していく
+* C-c C-l で型チェック(証明チェック)ができます
 
 
 # Agda による apply
@@ -96,17 +96,18 @@
 * とは
 * A を Int, B を String とすると
 * Int と、 Int から String を返す関数があれば String を作れる
-* と読める
+* と読める。つまり関数適用です
 
 
 # 命題に 'ならば' を含む場合
 * 関数を返せば良いです
 * Agda には lambda があるので
 
-* id : A -> A
+* id : (A -> A)
 * id = \a -> a
 
-* いったように書けます
+* といったように書けます。
+* lambda の syntax は \arg -> body です
 
 
 # 'ならば' を含む証明
@@ -126,4 +127,6 @@
 
 # 自然数の加算の交換法則の証明
 
+* TODO: いまから
+
 <!-- vim: set filetype=markdown.slide: -->