# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586598434 -32400
# Node ID 6c69d48e60156a86889883ace364e14204c8dc47
# Parent  da0a1dd0c2ee38dc7e389e112860b46ae26ca965
...

diff -r da0a1dd0c2ee -r 6c69d48e6015 CCCGraph1.agda
--- a/CCCGraph1.agda	Sat Apr 11 17:29:45 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 11 18:47:14 2020 +0900
@@ -97,7 +97,76 @@
    refl-<r> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → g ≡ g1
    refl-<r> refl = refl
 
+   iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c  ) ( g : Arrows a (atom b) )
+           → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g)
+   iv-e-arrow x (id (atom _)) = refl
+   iv-e-arrow x (iv f g) with eval (iv f g) 
+   iv-e-arrow x (iv f g) | id (atom _) = refl
+   iv-e-arrow x (iv f g) | iv f₁ t = refl
+   iv-e-ε : { a b c : Objs } → ( g : Arrows a ((c <= b) ∧ b ) )
+           → eval (iv ε g) ≡ iv ε (eval g)
+   iv-e-ε (id _) = refl
+   iv-e-ε < g , g₁ > = refl
+   iv-e-ε (iv f g) with eval (iv f g) 
+   iv-e-ε (iv f g) | id _ = refl
+   iv-e-ε (iv f g) | < t , t₁ > = refl
+   iv-e-ε (iv f g) | iv f₁ t = refl
+   iv-e-* : { a b c d : Objs } → { f : Arrow (d ∧ b) c} → ( g : Arrows a d )
+           → eval (iv (f *) g) ≡ iv (f *) (eval g)
+   iv-e-* (id a) = refl
+   iv-e-* (○ a) = refl
+   iv-e-* < g , g₁ > = refl
+   iv-e-* (iv f g) with eval (iv f g)
+   iv-e-* (iv f g) | id a = refl
+   iv-e-* (iv f g) | ○ a = refl
+   iv-e-* (iv f g) | < t , t₁ > = refl
+   iv-e-* (iv f g) | iv f₁ t = refl
+   iv-e-π : { a b c d : Objs } → { x : Arrow b (c ∧ d)} → ( g : Arrows a b )
+           → eval (iv π (iv x g)) ≡ iv π (eval (iv x g))
+   iv-e-π g with eval g
+   iv-e-π g | id a = {!!}
+   iv-e-π g | < t , t₁ > = {!!}
+   iv-e-π g | iv f t = {!!}
+
    idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
+   iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g))
+   iv-d (arrow x) g = begin
+          eval (iv (arrow x) g) 
+        ≡⟨ iv-e-arrow x g ⟩
+          iv (arrow x) (eval g)
+        ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩
+          iv (arrow x) (eval (eval g))
+        ≡⟨ sym (iv-e-arrow x (eval g)) ⟩
+          eval (iv (arrow x) (eval g))
+        ∎  where open ≡-Reasoning
+   iv-d π (id _) = refl
+   iv-d π < g , g₁ > = sym (idem-eval g)
+   iv-d π (iv f g) with eval (iv f g)
+   iv-d π (iv f g) | id _ = refl
+   iv-d π (iv f g) | < t , t₁ > = {!!}
+   iv-d π (iv f g) | iv f₁ t = {!!}
+   iv-d π' (id _) = refl
+   iv-d π' < g , g₁ > = sym (idem-eval g₁)
+   iv-d π' (iv f g) = {!!}
+   iv-d ε g = begin
+            eval (iv ε g)
+        ≡⟨ iv-e-ε g ⟩
+          iv ε (eval g)
+        ≡⟨ cong (λ k → iv ε k ) ( sym ( idem-eval g) ) ⟩
+          iv ε (eval (eval g))
+        ≡⟨ sym (iv-e-ε (eval g)) ⟩
+          eval (iv ε (eval g))
+        ∎  where open ≡-Reasoning
+   iv-d (x *) g = begin
+            eval (iv (x *) g)
+        ≡⟨ iv-e-* g ⟩
+          iv (x *) (eval g)
+        ≡⟨ cong (λ k → iv (x *) k ) ( sym ( idem-eval g) ) ⟩
+          iv (x *) (eval (eval g))
+        ≡⟨ sym (iv-e-* (eval g)) ⟩
+          eval (iv (x *) (eval g))
+        ∎  where open ≡-Reasoning
+
    idem-eval (id a) = refl
    idem-eval (○ a) = refl
    idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁)
@@ -114,6 +183,8 @@
    idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<r> m
    idem-eval (iv ε (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv ε k ) m
    idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv (f *) k ) m
+   idem-eval (iv ε (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-ε (iv f₁ t)) (cong ( λ k → iv ε k ) m )
+   idem-eval (iv (x *) (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-* (iv f₁ t)) (cong ( λ k → iv (x *) k ) m )
    idem-eval (iv f (iv g h)) | iv f₁ t | m | record { eq = ee } = trans lemma (cong ( λ k → iv f k ) m )  where
       lemma : eval (iv f (iv f₁ t)) ≡ iv f (eval (iv f₁ t))
       lemma = {!!}
@@ -133,32 +204,6 @@
                     associative  = λ{a b c d f g h } →  cong (λ k → eval k ) (associative f g h )
                }
            }  where 
-              iv-e : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ iv x (eval g)
-              iv-e = {!!}
-              iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c  ) ( g : Arrows a (atom b) )
-                   → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g)
-              iv-e-arrow x (id (atom _)) = refl
-              iv-e-arrow x (iv f g) with eval (iv f g) 
-              iv-e-arrow x (iv f g) | id (atom _) = refl
-              iv-e-arrow x (iv f g) | iv f₁ t = refl
-              iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g))
-              iv-d (arrow x) g = begin
-                  eval (iv (arrow x) g) 
-                ≡⟨ iv-e-arrow x g ⟩
-                  iv (arrow x) (eval g)
-                ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩
-                  iv (arrow x) (eval (eval g))
-                ≡⟨ sym (iv-e-arrow x (eval g)) ⟩
-                  eval (iv (arrow x) (eval g))
-                ∎  where open ≡-Reasoning
-              iv-d π (id _) = refl
-              iv-d π < g , g₁ > = sym (idem-eval g)
-              iv-d π (iv f g) = {!!}
-              iv-d π' (id _) = refl
-              iv-d π' < g , g₁ > = sym (idem-eval g₁)
-              iv-d π' (iv f g) = {!!}
-              iv-d ε g = {!!}
-              iv-d (x *) g = {!!}
               d-eval  : {A B C : Objs} (f : Arrows B C) (g : Arrows A B) →
                      eval (f ・ g) ≡ eval (eval f ・ eval g)
               d-eval (id a) g = sym (idem-eval  g)