# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585827738 -32400
# Node ID 3b8c1ca0d73760577c368b1a668217cc12e156d2
# Parent  a73acfdef6436792ae37438809a5147fd7cec47c
...

diff -r a73acfdef643 -r 3b8c1ca0d737 CCCGraph1.agda
--- a/CCCGraph1.agda	Thu Apr 02 13:43:43 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 20:42:18 2020 +0900
@@ -21,7 +21,6 @@
 
    data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where                       --- case i
       arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
-      ○ : (a : Objs ) → Arrow a ⊤
       π : {a b : Objs } → Arrow ( a ∧ b ) a
       π' : {a b : Objs } → Arrow ( a ∧ b ) b
       ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
@@ -29,18 +28,20 @@
 
    data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) where
       id : ( a : Objs ) → Arrows a a                                      --- case i
+      ○ : ( a : Objs ) → Arrows a ⊤                                       --- case i
       <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b)   --- case iii
       iv  : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c   -- cas iv
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = g
+   ○ a ・ g = ○ _
    < f , g > ・  h = <  f ・ h  ,  g ・ h  >
    iv f (id _) ・ h = iv f h
-   iv (○ a) g ・  h = iv (○ _) (id _)
    iv π < g , g₁ > ・  h = g ・ h
    iv π' < g , g₁ > ・  h = g₁ ・ h
    iv ε < g , g₁ > ・  h = iv ε < g ・ h , g₁ ・ h >
    iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > 
+   iv f ( (○ a)) ・ g = iv f ( ○ _ )
    iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )
 
    _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
@@ -63,15 +64,23 @@
            }  where
                identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) == f
                identityL {_} {_} {id a} = refl
+               identityL {_} {_} {○ a} = refl
                identityL {a} {b} {< f , f₁ >} = refl
                identityL {_} {_} {iv f f₁} = refl
+               identyR-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrow b c) (f₁ :  Arrows a b ) → iv x (iv f f₁) ・ id a ≡ iv x ((iv f f₁) ・ id a)
+               identyR-iv (arrow x) f f₁ = refl
+               identyR-iv π f f₁ = refl
+               identyR-iv π' f f₁ = refl
+               identyR-iv ε f f₁ = refl
+               identyR-iv (x *) f f₁ = refl
                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≡ {a} {_} {f} ) (identityR≡ {a} {_} {f₁} )
                identityR≡ {a} {b} {iv x (id a)} = refl
-               identityR≡ {a} {b} {iv π < f , f₁ >} = {!!}
+               identityR≡ {a} {b} {iv x (○ a)} = refl
+               identityR≡ {a} {b} {iv π < f , f₁ >} = ?
                identityR≡ {a} {b} {iv π' < f , f₁ >} = {!!}
-               identityR≡ {a} {⊤} {iv (○ .(_ ∧ _)) < f , f₁ >} = {!!}
                identityR≡ {a} {b} {iv ε < f , f₁ >} = cong ( λ k → iv ε k ) ( identityR≡ {_} {_} {< f , f₁ >} )
                identityR≡ {a} {_} {iv (x *) < f , f₁ >} = cong ( λ k → iv (x *) k ) ( identityR≡ {_} {_} {< f , f₁ >} )
                identityR≡ {a} {b} {iv {a} {c} {d} x (iv {a} {d} {c1} f f₁)} = begin -- cong ( λ k → iv x k ・ id a ) {!!} -- ( identityR {_} {_} {iv f f₁} )
@@ -86,6 +95,7 @@
                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
+               associative (○ 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 )