--- a/a02/lecture.ind	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/lecture.ind	Wed Nov 08 21:35:54 2023 +0900
@@ -22,6 +22,7 @@
 
 論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。
 
+この章の内容は基本的には Girad 先生の Proofs and Typesに書いてある内容です。
 
 --あらすじ
 
@@ -162,7 +163,7 @@
 
 record によって  
 
-   record _∧_ A B : Set
+   record _∧_ A B : Set where
      field
          π1 : A
          π2 : B
@@ -177,7 +178,7 @@
 
 とかける。(Haskell では (∧) を使う)
 
-は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。
+は、型Aと型Bから作るデータ構造である。オブジェクトあるいは構造体だと思って良い。
 
    record { π1 = x ; π2 = y }