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

diff -r 6c69d48e6015 -r 0173a5dc6a42 CCCGraph1.agda
--- a/CCCGraph1.agda	Sat Apr 11 18:47:14 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 11 20:32:37 2020 +0900
@@ -121,12 +121,26 @@
    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 = {!!}
+
+   π-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c )
+      → eval g ≡ < f1 , f2 > → eval (iv π g ) ≡ f1
+   π-lemma < g , g₁ > f1 f2 refl = refl
+   π-lemma (iv π g) f1 f2 eq with eval (iv π g)
+   π-lemma (iv π g) f1 f2 refl | < t , t₁ > = refl
+   π-lemma (iv π' g) f1 f2 eq with eval (iv π' g)
+   π-lemma (iv π' g) f1 f2 refl | < t , t₁ > = refl
+   π-lemma (iv ε g) f1 f2 eq with eval (iv ε g)
+   π-lemma (iv ε g) f1 f2 refl | < t , t₁ > = refl
+
+   π'-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c )
+      → eval g ≡ < f1 , f2 > → eval (iv π' g ) ≡ f2
+   π'-lemma < g , g₁ > f1 f2 refl = refl
+   π'-lemma (iv π g) f1 f2 eq with eval (iv π g)
+   π'-lemma (iv π g) f1 f2 refl | < t , t₁ > = refl
+   π'-lemma (iv π' g) f1 f2 eq with eval (iv π' g)
+   π'-lemma (iv π' g) f1 f2 refl | < t , t₁ > = refl
+   π'-lemma (iv ε g) f1 f2 eq with eval (iv ε g)
+   π'-lemma (iv ε g) f1 f2 refl | < t , t₁ > = refl
 
    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))
@@ -141,10 +155,20 @@
         ∎  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 π (iv f (id a)) = refl
+   iv-d π (iv x f ) with eval (iv x f) | inspect eval (iv x f)
+   ... | id _ | m = refl
+   ... | < f1 , f2 > | record {eq = ee } = begin
+           f1
+        ≡⟨ sym ( π-lemma (iv x f) f1 f2 ee ) ⟩
+           eval (iv π (iv x f))
+        ≡⟨ sym (idem-eval (iv π (iv x f))) ⟩
+           eval (eval (iv π (iv x f)))
+        ≡⟨ cong (λ k → eval k ) (π-lemma (iv x f) f1 f2 ee ) ⟩
+           eval f1 
+        ∎  where open ≡-Reasoning
+   ... | iv x1 f1 | m = {!!}
+   iv-d π (iv f (iv f₁ g)) = {!!}
    iv-d π' (id _) = refl
    iv-d π' < g , g₁ > = sym (idem-eval g₁)
    iv-d π' (iv f g) = {!!}
@@ -185,9 +209,9 @@
    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 = {!!}
+   idem-eval (iv π (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!}
+   idem-eval (iv π' (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!}
+   idem-eval (iv (arrow x) (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-arrow x (iv f₁ t)) (cong ( λ k → iv (arrow x) k ) m )  
 
    PL1 :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL1 = record {