--- a/a02/agda/practice-logic.agda	Wed Oct 02 13:19:44 2019 +0900
+++ b/a02/agda/practice-logic.agda	Tue Oct 15 16:05:34 2019 +0900
@@ -4,6 +4,21 @@
 postulate A : Set
 postulate B : Set
 
+postulate b : B
+
+lemma0 : A -> B
+lemma0 = {!!}
+
+id : { A : Set } → ( A → A )
+id = {!!}
+
+id' : { A : Set } → ( A → A )
+id' x  = {!!}
+
+_・_ : {A B C : Set } → {!!}
+f ・ g = λ x → f ( g x )    
+
+
 Lemma1 : Set
 Lemma1 = A -> ( A -> B ) -> B
 
@@ -52,6 +67,30 @@
 lemma6 : Lemma6
 lemma6 = \b ->  {!!}
 
+ex1 : {A B : Set} → ( A ∧ B ) → A 
+ex1 a∧b = {!!}
+
+ex2 : {A B : Set} → ( A ∧ B ) → B 
+ex2 a∧b = {!!}
+
+ex3 : {A B : Set} → A → B → ( A ∧ B ) 
+ex3 a b = {!!}
+
+ex4 : {A B : Set} → A → ( A ∧ A ) 
+ex4 a  = record { and1 = {!!} ;  and2 = {!!} }
+
+ex5 : {A B C : Set} → ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 
+ex5 a∧b∧c = record { and1 = {!!} ; and2 = {!!} }
+
+ex6 : {A B C : Set} → ( (A → B ) ∧ ( B →  C) )  → A → C
+ex6  =  {!!}
+
+ex7 : {A : Set} → ( A ∨ A ) → A
+ex7 =  ?
+
+ex8 : {A B : Set} → B → ( A ∨ ( B → A ) ) → A
+ex8 = ?
+
 open import Relation.Nullary
 open import Relation.Binary
 open import Data.Empty

--- a/a02/lecture.ind	Wed Oct 02 13:19:44 2019 +0900
+++ b/a02/lecture.ind	Tue Oct 15 16:05:34 2019 +0900
@@ -98,16 +98,13 @@
 
 と定義する。
 
----問題2.1 Agdaによる関数と証明
-
-
-以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
-
-<a href="agda/lambda.agda"> lambda </a> <!---  Exercise 2.1 --->
 
 
 ---Agdaの構文
 
+<a href="agda-install.html"> Agda のinstallの方法 </a>
+<br>
+
 型と値
 
 名前の作り方
@@ -120,6 +117,15 @@
 
 <a href="agda.html"> agda の細かい構文の話 </a> 
 
+
+---問題2.1 Agdaによる関数と証明
+
+
+以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
+
+<a href="agda/lambda.agda"> lambda </a> <!---  Exercise 2.1 --->
+
+
 --record または ∧
 
 導入                          除去
@@ -255,11 +261,13 @@
 
 前の証明図と、Agdaで証明とどこがどう対応しているのかを考えてみよう。
 
----問題2.2 Agdaのrecord
+---問題2.2 Agdaによる関数と証明
+
 
 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
 
-<a href="agda/record1.agda"> record </a> <!---  Exercise 2.2 --->
+<a href="agda/practice-logic.agda"> practice-logic</a> <!---  Exercise 2.2 --->
+
 
 
 --data または 排他的論理和(Sum)
@@ -399,6 +407,8 @@
 
 <a href="agda/equality.agda"> equality </a> <!---  Exercise 2.4 --->
 
+<a href="agda/practice-nat.agda"> equality </a> <!---  Exercise 2.5 --->
+
 --集合のLevel 
 
 論理式は型であり、それは基本的はSetになっている。例えば、A → B は Set である。

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/chap0.agda	Tue Oct 15 16:05:34 2019 +0900
@@ -0,0 +1,105 @@
+module chap0 where
+
+open import Data.List
+open import Data.Nat hiding (_⊔_)
+open import Data.Integer hiding (_⊔_)
+open import Data.Product
+
+A : List ℕ
+A = 1 ∷ 2 ∷ []
+
+data Literal : Set where
+    x : Literal
+    y : Literal
+    z : Literal
+
+B : List Literal
+B = x ∷ y ∷ z ∷ []
+
+
+ListProduct : {A B : Set } → List A → List B → List ( A × B )
+ListProduct = {!!}
+
+ex05 : List ( ℕ × Literal )
+ex05 = ListProduct A B   -- (1 , x) ∷ (1 , y) ∷ (1 , z) ∷ (2 , x) ∷ (2 , y) ∷ (2 , z) ∷ [] 
+
+ex06 : List ( ℕ × Literal × ℕ )
+ex06 = ListProduct A (ListProduct B A)
+
+ex07 : Set
+ex07 =  ℕ × ℕ
+
+data ex08-f : ℕ → ℕ → Set where
+    ex08f0 : ex08-f 0 1
+    ex08f1 : ex08-f 1 2
+    ex08f2 : ex08-f 2 3
+    ex08f3 : ex08-f 3 4
+    ex08f4 : ex08-f 4 0
+
+data ex09-g : ℕ → ℕ → ℕ → ℕ → Set where
+    ex09g0 : ex09-g 0 1 2 3
+    ex09g1 : ex09-g 1 2 3 0
+    ex09g2 : ex09-g 2 3 0 1
+    ex09g3 : ex09-g 3 0 1 2
+
+open import Data.Nat.DivMod
+open import Relation.Binary.PropositionalEquality
+
+_≡7_ : ℕ → ℕ → Set
+n ≡7 m = (n % 7) ≡ (m % 7 )
+
+refl7 :  { n : ℕ} → n ≡7 n
+refl7 = {!!}
+
+sym7  : { n m : ℕ} → n ≡7 m → m ≡7 n
+sym7  = {!!}
+
+trans7 : { n m o : ℕ} → n ≡7 m → m ≡7 o → n ≡7 o
+trans7 = {!!}
+
+open import Level renaming ( zero to Zero ; suc to Suc )
+
+record Graph  { v v' : Level } : Set (Suc v ⊔ Suc v' ) where
+  field
+    vertex : Set v
+    edge : vertex  → vertex → Set v'
+
+data edge012a :  ℕ → ℕ →  Set where
+    e012a-1 : edge012a 1 2
+    e012a-2 : edge012a 2 3
+    e012a-3 : edge012a 3 4
+    e012a-4 : edge012a 4 5
+    e012a-5 : edge012a 5 1
+
+graph012a : Graph {Zero} {Zero}
+graph012a = record { vertex = ℕ  ; edge = edge012a }
+
+data edge012b :  ℕ → ℕ →  Set where
+    e012b-1 : edge012b 1 2
+    e012b-2 : edge012b 1 3
+    e012b-3 : edge012b 1 4
+    e012b-4 : edge012b 2 3
+    e012b-5 : edge012b 2 4
+    e012b-6 : edge012b 3 4
+
+graph012b : Graph {Zero} {Zero}
+graph012b = record { vertex = ℕ  ; edge = edge012b }
+
+data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set  where
+    direct :   E x y -> connected E x y 
+    indirect :  { z : V  } -> E x z  ->  connected {V} E z y -> connected E x y
+
+open import Data.Empty
+open import Relation.Nullary
+
+-- data Dec (P : Set) : Set where
+--    yes :   P → Dec P
+--    no  : ¬ P → Dec P
+
+reachable :  { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
+reachable {V} E X Y = Dec ( connected {V} E X Y )
+
+dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
+
+