# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586055180 -32400
# Node ID d3cf372ac8cd217941e91d9c41895aeccc0b473d
# Parent  ed0b3d2d10374160d330836cdae2c6afa95ea309
give update idempotent

diff -r ed0b3d2d1037 -r d3cf372ac8cd CCCGraph1.agda
--- a/CCCGraph1.agda	Sun Apr 05 11:15:41 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 11:53:00 2020 +0900
@@ -51,46 +51,11 @@
    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) 
 
-   idem-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → f ≡ f1
-   idem-<l> refl = refl
-
-   idem-<r> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → g ≡ g1
-   idem-<r> refl = refl
+   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
 
-   idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
-   idem-eval (id a) = refl
-   idem-eval (○ a) = refl
-   idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁)
-   idem-eval (iv f (id a)) = refl
-   idem-eval (iv f (○ a)) = refl
-   idem-eval (iv π < g , g₁ >) = idem-eval g 
-   idem-eval (iv π' < g , g₁ >) = idem-eval g₁
-   idem-eval (iv ε < f , f₁ >) = cong₂ ( λ j k → iv ε < j , k > ) (idem-eval f) (idem-eval f₁)
-   idem-eval (iv (x *) < f , f₁ >) =  cong₂ ( λ j k → iv (x *) < j , k > ) (idem-eval f) (idem-eval f₁)
-   idem-eval (iv f (iv g h)) with eval (iv g h) | idem-eval (iv g h) 
-   idem-eval (iv f (iv g h)) | id a | m = refl
-   idem-eval (iv f (iv g h)) | ○ a | m = refl
-   idem-eval (iv π (iv g h)) | < t , t₁ > | m = idem-<l> m 
-   idem-eval (iv π' (iv g h)) | < t , t₁ > | m = idem-<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 (arrow x) (iv g h)) | iv f1 (id a) | m =  cong ( λ k → iv (arrow x) k ) m
-   idem-eval (iv π (iv g h)) | iv f1 (id a) | m =  cong ( λ k → iv π k ) m
-   idem-eval (iv π' (iv g h)) | iv f1 (id a) | m =  cong ( λ k → iv π' k ) m
-   idem-eval (iv ε (iv g h)) | iv f1 (id a) | m =  cong ( λ k → iv ε k ) m
-   idem-eval (iv (f *) (iv g h)) | iv f1 (id a) | m =  cong ( λ k → iv (f *) k ) m
-   idem-eval (iv (f *) (iv g h)) | iv f1 (○ a) | m =  cong ( λ k → iv (f *) k ) m
-   idem-eval (iv f (iv g h)) | iv π < t , t₁ > | m = {!!}
-   idem-eval (iv f (iv g h)) | iv π' < t , t₁ > | m = {!!}
-   idem-eval (iv (arrow x) (iv g h)) | iv ε < t , t₁ > | m = cong ( λ k → iv (arrow x) k ) m
-   idem-eval (iv π (iv g h)) | iv ε < t , t₁ > | m = cong ( λ k → iv π k ) m
-   idem-eval (iv π' (iv g h)) | iv ε < t , t₁ > | m =  cong ( λ k → iv π' k ) m
-   idem-eval (iv ε (iv g h)) | iv ε < t , t₁ > | m =  cong ( λ k → iv ε k ) m
-   idem-eval (iv (f *) (iv g h)) | iv ε < t , t₁ > | m =  cong ( λ k → iv (f *) k ) m
-   idem-eval (iv (f *) (iv g h)) | iv (f1 *) < t , t₁ > | m =  cong ( λ k → iv (f *) k ) m
-   idem-eval (iv f (iv g h)) | iv f1 (iv f₁ t) | m =  {!!}
-   --     lemma : eval (iv f (  iv f1 (iv f₁ t))) ≡ iv f ( iv f1 (iv f₁ t))
-   --     lemma = {!!}
+   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
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = g
@@ -110,17 +75,15 @@
 
    identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
    identityR {a} {.a} {id a} = refl
-   identityR {a} {.⊤} {○ a} = refl
-   identityR {a} {.(_ ∧ _)} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
-   identityR {a} {b} {iv f (id a)} = refl
-   identityR {a} {b} {iv f (○ a)} = refl
-   identityR {a} {b} {iv π < g , g₁ >} = identityR {_} {_} {g} 
-   identityR {a} {b} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} 
-   identityR {a} {b} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
-   identityR {a} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
-   identityR {a} {b} {iv {c} {d} {e} π (iv g h)} = refl
-   identityR {a} {b} {iv {c} {d} {e} π' (iv g h)} = refl
-   identityR {a} {b} {iv {c} {d} {e} f (iv g h)} = refl
+   identityR {a} {⊤} {○ a} = refl
+   identityR {_} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
+   identityR {_} {_} {iv f (id a)} = refl
+   identityR {_} {_} {iv f (○ a)} = refl
+   identityR {_} {_} {iv π < g , g₁ >} = identityR {_} {_} {g} 
+   identityR {_} {_} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} 
+   identityR {_} {_} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
+   identityR {_} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
+   identityR {_} {_} {iv f (iv g h)} = refl
 
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
    ==←≡ eq = cong (λ k → eval k ) eq
@@ -150,7 +113,8 @@
                associative (id a) g h = refl
                associative (○ a) g h = refl
                associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
-               associative {a} (iv x f) g h = {!!} -- cong ( λ k → iv x k ) (associative f g h) 
+               associative {a} (iv x f) g h = {!!} 
+                  -- cong ( λ k → iv x k ) (associative f g h) 
                o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
                             f == g → h == i → (h ・ f) == (i ・ g)
                o-resp-≈  f=g h=i = {!!}