# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586610362 -32400
# Node ID 93dd4c04196908b6f4e772c82e9d05f6d7a7d4db
# Parent  0173a5dc6a42b93c7349900137f03a708624be3e
...

diff -r 0173a5dc6a42 -r 93dd4c041969 CCCGraph1.agda
--- a/CCCGraph1.agda	Sat Apr 11 20:32:37 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 11 22:06:02 2020 +0900
@@ -234,12 +234,18 @@
               d-eval (○ a) g = refl
               d-eval < f , f₁ > g = cong₂ (λ j k → < j , k > ) (d-eval f g) (d-eval f₁ g)
               d-eval (iv x (id a)) g = iv-d x g
-              d-eval (iv (x *) (○ a)) g = {!!}
+              d-eval (iv (x *) (○ a)) g = refl
               d-eval (iv π < f , f₁ >) g = d-eval f g
               d-eval (iv π' < f , f₁ >) g = d-eval f₁ g
-              d-eval (iv ε < f , f₁ >) g = {!!}
-              d-eval (iv (x *) < f , f₁ >) g = {!!}
-              d-eval (iv x (iv f f₁)) g = {!!}
+              d-eval (iv ε < f , f₁ >) g = cong₂ (λ j k → iv ε k ) (d-eval f g) (
+                  cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g ))
+              d-eval (iv (x *) < f , f₁ >) g =  cong₂ (λ j k → iv (x *) k ) (d-eval f g) (
+                  cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g ))
+              d-eval (iv x (iv f f₁)) g = begin
+                    eval (iv x (iv f f₁) ・ g)
+                ≡⟨ {!!} ⟩
+                    eval (eval (iv x (iv f f₁)) ・ eval g)
+                ∎  where open ≡-Reasoning
               ore  : {A B C : Objs} (f g : Arrows A B) (h i : Arrows B C) →
                                     eval f ≡ eval g → eval h ≡ eval i → eval (h ・ f) ≡ eval (i ・ g)
               ore f g h i f=g h=i = begin