# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585787588 -32400
# Node ID f9167bc017cdaa4e1267f7a925c1619a849f8596
# Parent  111ee96c09abe02619c8c877eea949da1a3a0b96
...

diff -r 111ee96c09ab -r f9167bc017cd CCCGraph1.agda
--- a/CCCGraph1.agda	Thu Apr 02 09:15:52 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 09:33:08 2020 +0900
@@ -64,7 +64,10 @@
                identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
                identityR {a} {_} {id a} = refl
                identityR {a} {b} {< f , g >} = cong₂ ( λ j k → < j , k > ) ( identityR {_} {_} {f} ) ( identityR {_} {_} {g} )
-               identityR {a} {b} {iv x f} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
+               identityR {a} {b} {iv x (id a)} = refl
+               identityR {a} {b} {iv π < f , f₁ >} = {!!}
+               identityR {a} {b} {iv x < f , f₁ >} = {!!}
+               identityR {a} {b} {iv x (iv f f₁)} = {!!} -- cong ( λ k → iv x k ) ( identityR {_} {_} {f} )
                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-≈  refl refl = refl
@@ -72,5 +75,5 @@
                             (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
                associative (id a) g h = refl
                associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
-               associative (iv x f) g h = ? -- cong ( λ k → iv x k ) ( associative f g h )
+               associative (iv x f) g h = {!!} -- cong ( λ k → iv x k ) ( associative f g h )