# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586632201 -32400
# Node ID 9c41a7851817e5cb4728ba4e8533fa1f73253f7a
# Parent  1c659deb22f829ae8b0b46b5b908e09c8e87b0d5
fix *

diff -r 1c659deb22f8 -r 9c41a7851817 CCCGraph1.agda
--- a/CCCGraph1.agda	Sun Apr 12 03:34:50 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 12 04:10:01 2020 +0900
@@ -19,14 +19,15 @@
       _∧_ : Objs  → Objs  → Objs 
       _<=_ : Objs → Objs → Objs 
 
+   data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) 
    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 b : Objs } → Arrow ( a ∧ b ) a
       π' : {a b : Objs } → Arrow ( a ∧ b ) b
       ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
-      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )        --- case v
+      _* : {a b c : Objs } → Arrows (c ∧ b ) a → Arrow c ( a <= b )        --- case v
 
-   data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) where
+   data  Arrows 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
@@ -81,7 +82,7 @@
    eval (iv π < g , h >) = eval g
    eval (iv π' < g , h >) = eval h
    eval (iv ε < g , h >) = iv ε < eval g , eval h >
-   eval (iv (f *) < g , h >) = iv (f *) < eval g , eval h >
+   eval (iv (f *) < g , h >) = iv ((eval f) *) < eval g , eval h >
    eval (iv f (iv g h)) with eval (iv g h)
    eval (iv f (iv g h)) | id a = iv f (id a)  
    eval (iv f (iv g h)) | ○ a = iv f (○ a)
@@ -111,11 +112,11 @@
    iv-e-ε (iv f g) | id _ = refl
    iv-e-ε (iv f g) | < t , t₁ > = refl
    iv-e-ε (iv f g) | iv f₁ t = refl
-   iv-e-* : { a b c d : Objs } → { f : Arrow (d ∧ b) c} → ( g : Arrows a d )
+   iv-e-* : { a b c d : Objs } → { f : Arrows (d ∧ b) c} → ( g : Arrows a d )
            → eval (iv (f *) g) ≡ iv (f *) (eval g)
    iv-e-* (id a) = refl
    iv-e-* (○ a) = refl
-   iv-e-* < g , g₁ > = refl
+   iv-e-* < g , g₁ > = {!!}
    iv-e-* (iv f g) with eval (iv f g)
    iv-e-* (iv f g) | id a = refl
    iv-e-* (iv f g) | ○ a = refl
@@ -241,14 +242,14 @@
    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 (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) | inspect 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 | _ = refl-<l> m
    idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<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 (f *) (iv g h)) | < t , t₁ > | m | _ = {!!} -- cong ( λ k → iv (f *) k ) m
    idem-eval (iv ε (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-ε (iv f₁ t)) (cong ( λ k → iv ε k ) m )
    idem-eval (iv (x *) (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-* (iv f₁ t)) (cong ( λ k → iv (x *) k ) m )
    idem-eval (iv π (iv g h)) | iv f₁ t | m | record { eq = ee } = begin
@@ -291,8 +292,8 @@
               d-eval (iv π' < f , f₁ >) g = d-eval f₁ g
               d-eval (iv ε < f , f₁ >) g = cong₂ (λ j k → iv ε k ) (d-eval f g) (
                   cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g ))
-              d-eval (iv (x *) < f , f₁ >) g =  cong₂ (λ j k → iv (x *) k ) (d-eval f g) (
-                  cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g ))
+              d-eval (iv (x *) < f , f₁ >) g =  {!!} -- cong₂ (λ j k → iv (x *) k ) (d-eval f g) (
+                  -- cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g ))
               d-eval (iv x (iv f f₁)) g = begin
                     eval (iv x (iv f f₁) ・ g)
                 ≡⟨⟩