--- a/a02/agda/data1.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/a02/agda/data1.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -28,20 +28,20 @@
 open _∧_
 
 ex3' : {A B : Set} → ( A ∨ B ) →   A ∧ B   -- this is wrong
-ex3' = ?
+ex3' (case1 x) = ?
+ex3' (case2 x) = ?
 
 ex4' : {A B : Set} → ( A ∧ B ) →   A ∨ B   
-ex4' ab = case1 (proj1 ab )
+ex4' ⟪ a , b ⟫ = ?
 
 --- ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∨  B ) → C ) is wrong
 ex5 :  {A B C : Set} →  (( A → C ) ∨ ( B  → C ) ) → ( ( A ∧  B ) → C )
-ex5 (case1 a→c) ab = a→c (proj1 ab)
-ex5 (case2 b→c) ab = b→c (proj2 ab)
+ex5 = ?
 
 data ⊥ : Set where
 
-⊥-elim : {A : Set } -> ⊥ -> A
-⊥-elim = {!!}
+⊥-elim : {A : Set } →  ⊥ →  A
+⊥-elim ()
 
 ¬_ : Set → Set
 ¬ A = A → ⊥
@@ -76,6 +76,36 @@
     problem2 = {!!}
 
 
+data Nat : Set where
+  zero : Nat
+  suc  : Nat →  Nat
+
+one : Nat
+one = suc zero
+
+five : Nat
+five = suc (suc (suc (suc (suc zero))))
+
+add : ( a b : Nat ) → Nat
+add zero x = x
+add (suc x) y = suc ( add x y )
+
+data _≡_ {A : Set } : ( x y : A ) → Set where
+  refl : {x : A} → x ≡ x
+
+test11 : add one five ≡ suc five
+test11 = refl
+
+mul : ( a b : Nat ) → Nat
+mul zero x = zero
+mul (suc x) y = add y (mul x y)
+
+ex6 : Nat
+ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
+
+ex7 : mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) ≡  suc (suc (suc (suc (suc (suc zero)))))
+ex7 = refl
+
 data Three : Set where
   t1 : Three
   t2 : Three
@@ -95,27 +125,24 @@
    r2 : 3Ring t2 t3
    r3 : 3Ring t3 t1
 
-data Nat : Set where
-  zero : Nat
-  suc  : Nat →  Nat
-
-add : ( a b : Nat ) → Nat
-add zero x = x
-add (suc x) y = suc ( add x y )
-
-mul : ( a b : Nat ) → Nat
-mul zero x = zero
-mul (suc x) y = add y (mul x y)
-
-ex6 : Nat
-ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
-
 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
 
-dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
+dag :  { V : Set } ( E : V -> V -> Set ) →  Set
 dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
 
 lemma : ¬ (dag 3Ring )
-lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 )))
+lemma r = ?
+
+--   t1 → t2 → t3
+--
+data 3Line : (dom cod : Three) → Set where
+   line1 : 3Line t1 t2
+   line2 : 3Line t2 t3
+
+lemma1 : dag 3Line
+lemma1 = ?
+
+
+