# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585907055 -32400
# Node ID 18bbd9e31c4879fbb31c2ee651bbc3db0b7be09e
# Parent  f2729064016dd4a078e1d296596f18b08e5f3326
...

diff -r f2729064016d -r 18bbd9e31c48 CCCGraph1.agda
--- a/CCCGraph1.agda	Fri Apr 03 17:50:48 2020 +0900
+++ b/CCCGraph1.agda	Fri Apr 03 18:44:15 2020 +0900
@@ -62,6 +62,16 @@
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
    ==←≡ eq = cong (λ k → k ・ id _) eq
 
+   assoc-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → iv x f ・ g ≡ iv x ( f ・ g )
+   assoc-iv x f (id _) = {!!}
+   assoc-iv x (id a) g = {!!}
+   assoc-iv x (○ a) g = {!!}
+   assoc-iv π < f , f₁ > g = {!!}
+   assoc-iv π' < f , f₁ > g = {!!}
+   assoc-iv ε < f , f₁ > g = {!!}
+   assoc-iv (x *) < f , f₁ > g = {!!}
+   assoc-iv x (iv f f₁) g = {!!}
+
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
             Obj  = Objs;
@@ -82,23 +92,6 @@
                identityL {_} {_} {○ a} = refl
                identityL {a} {b} {< f , f₁ >} = refl
                identityL {_} {_} {iv f f₁} = refl
-               assoc-iv1 : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → (iv x f ・ g) == (iv x ( f ・ g ))
-               assoc-iv1 (arrow x) f g = ?
-               assoc-iv1 π f g = {!!}
-               assoc-iv1 π' f g = {!!}
-               assoc-iv1 ε f g = {!!}
-               assoc-iv1 (x *) f g = {!!}
-               assoc-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → iv x f ・ g ≡ iv x ( f ・ g )
-               assoc-iv (arrow x) (id .(atom _)) g = {!!}
-               assoc-iv (arrow x) (iv f f₁) g = {!!}
-               assoc-iv π (id .(_ ∧ _)) g = {!!}
-               assoc-iv π < f , f₁ > g = {!!}
-               assoc-iv π (iv f f₁) g = {!!}
-               assoc-iv π' f g = {!!}
-               assoc-iv ε (id .((_ <= _) ∧ _)) g = {!!}
-               assoc-iv ε < f , f₁ > g = {!!}
-               assoc-iv ε (iv f f₁) g = {!!}
-               assoc-iv (x *) f g = {!!}
                associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
                             (f ・ (g ・ h)) == ((f ・ g) ・ h)
                associative (id a) g h = refl