--- /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 )
+
+