# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586566177 -32400
# Node ID 73bce40fd1c1cd343f7ff962e43289f45a38df7a
# Parent  0793d9adbbdd24cb378ab5bf34ee5078f1be28db
...

diff -r 0793d9adbbdd -r 73bce40fd1c1 CCCGraph1.agda
--- a/CCCGraph1.agda	Fri Apr 10 23:07:00 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 11 09:49:37 2020 +0900
@@ -91,6 +91,12 @@
    eval (iv (f *) (iv g h)) | < t , t₁ > = iv (f *) < t , t₁ > 
    eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) 
 
+   refl-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → f ≡ f1
+   refl-<l> refl = refl
+
+   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
+
    PL1 :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL1 = record {
             Obj  = Objs;
@@ -106,16 +112,25 @@
                     associative  = λ{a b c d f g h } →  cong (λ k → eval k ) (associative f g h )
                }
            }  where 
+              id-case : {a b : Objs } → (f g : Arrows a b) → (h : Arrows b b) →
+                 eval f ≡ eval g → 
+                 id b ≡ eval h → eval f ≡ eval (h ・ g)
+              id-case {a} {b} f g (id b) f=g h=i = f=g
+              id-case {a} {b} f g (iv π  < h1 , h2 >)  f=g h=i = id-case f g h1 f=g h=i
+              id-case {a} {b} f g (iv π' < h1 , h2 >)  f=g h=i = id-case f g h2 f=g h=i
+              id-case {a} {b} f g (iv x (iv f₁ h)) f=g h=i with eval (iv f₁ h) | inspect eval (iv f₁ h)
+              id-case {a} {b} f g (iv π (iv f₁ h)) f=g h=i | < t , t₁ > | record { eq = ee } = lemma where
+                  lemma : eval f ≡ eval (iv π (iv f₁ (h ・ g)))
+                  lemma = {!!}
+              id-case {a} {b} f g (iv π' (iv f₁ h)) f=g h=i | < t , t₁ > | record { eq = ee } = {!!}
               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 (id a) (id a) f=g refl = cong (λ k → id a ・ k) f=g
-              ore f g (id a) (iv x < i1 , i2 >) f=g h=i = {!!}
-              ore f g (id a) (iv x (iv i1 i2)) f=g h=i = {!!}
+              ore f g (id a) i1 f=g h=i = id-case f g i1 f=g h=i  
               ore f g (○ a) (○ a) f=g h=i = refl
               ore f g (○ a) (iv x i) f=g h=i = {!!}
               ore f g < h1 , h2 > < i1 , i2 > f=g h=i = cong₂ (λ j k → < j , k >) (ore f g h1 i1 f=g {!!}) (ore f g h2 i2 f=g {!!})
               ore f g < h1 , h2 > (iv x i) f=g h=i = {!!}
-              ore f g (iv x h) (id a) f=g h=i = {!!}
+              ore f g (iv x h) (id a) f=g h=i = sym ( id-case g f (iv x h) (sym f=g) (sym h=i))
               ore f g (iv x h) (○ a) f=g h=i = {!!}
               ore f g (iv x h) < i , i₁ > f=g h=i = {!!}
               ore f g (iv x h) (iv y i) f=g h=i = {!!}