--- a/CCCGraph.agda	Sun Mar 15 14:26:39 2020 +0900
+++ b/CCCGraph.agda	Mon Mar 23 02:42:41 2020 +0900
@@ -197,40 +197,28 @@
       <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
       _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
       id : ( a : Objs ) → Arrow a a
-      next : { a b c : Objs } → Arrow b c  → Arrow a b → Arrow a c
 
-   _・_ :  {a b c : Objs } (f : Arrow b c ) → (g : Arrow a b) → Arrow a c
-   id _ ・ f = f
-   (next x f) ・ g = next x ( f ・ g )
-   f ・ g = next f g 
-
-   -- data  φ  {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ) where
-   --   i   : {b c : Obj A} {k : Hom A b c } → φ x k
-   --   ii  : φ x {⊤} {a} x
-   --   iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
-   --   iv  : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
-   --   v   : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
+   data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) where
+      i   : {b c : Objs} (k : Arrow b c ) → Arrows b c
+      iii : {b c' c'' : Objs } ( f : Arrows b c' ) ( g : Arrows b c'' ) → Arrows b (c'  ∧ c'')  
+      iv  : {b c d : Objs } ( f : Arrows d c ) ( g : Arrow b d ) → Arrows b c
+      v   : {b c' c'' : Objs } ( f : Arrows (b ∧ c') c'' ) → Arrows b (c'' <= c') 
 
-   data  φ  : {b c : Objs } → Arrow b c → Set ( c₁  ⊔  c₂ ) where
-      i   : {b c : Objs} {k : Arrow b c } → φ k
-      iii : {b c' c'' : Objs } { f : Arrow b c' } { g : Arrow b c'' } (ψ : φ f ) (χ : φ g ) → φ {b} {c'  ∧ c''} < f , g > 
-      iv  : {b c d : Objs } { f : Arrow d c } { g : Arrow b d } (ψ : φ f ) (χ : φ g ) → φ ( f ・ g )
-      v   : {b c' c'' : Objs } { f : Arrow (b ∧ c') c'' }  (ψ : φ f )  → φ {b} {c'' <= c'} ( f * )
-
-
-   eval : {a b : Objs} → (f : Arrow a b ) → {fe : Arrow a b } → φ {a} {b} fe
-   eval {atom a} {atom b} (arrow f) = i
-   eval {a} {⊤} (○ a) = i
-   eval {b ∧ _} {b} π = i
-   eval {.(_ ∧ b)} {b} π' = i
-   eval {.((b <= _) ∧ _)} {b} ε = i
-   eval {a} {_ ∧ _} < f , g > = {!!} -- iii (eval f) (eval g)
-   eval {a} {_ <= _} (f *) = {!!} -- v {!!}
-   eval {a} {a} (id a) = i
-   eval {a} {b} (next {a} {a} {b} f (id a)) = eval f
-   eval {a} {b} (next {a} {c} {b} f (next {a} {d} {c} g h) ) = iv {a} {b} {d} (iv {d} {b} {c} (eval f) (eval g) ) (eval h)
-   eval {a} {b} (next {a} {c} {b} f g) with eval g
-   ... | t = {!!}
+   _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
+   i (id _) ・ g = g
+   f ・ i (id _)  = f
+   f ・ i g = iv f g
+   f ・ iii g h  = {!!} -- iii ( f ・ g ) ( f ・ h )
+   f ・ (iv g h ) = iv ( f ・ g ) h
+   f ・  v g = ?
+--   v ( f ・ iii (g1 g) (iv (id _) (i π') )) where
+--      g1 :  {a b c' : Objs} → Arrows a b → Arrows (a ∧ c') b
+--      g1 {a} {b} {c'} (i k) = ? -- iv k (i π)
+--      g1 {a} {.(_ ∧ _)} {c'} (iii g g₁) = iii (g1 g) (g1 g₁)
+--      g1 {a} {b} {c'} (iv f g) = iv f ? -- (g1 g)
+--      g1 {a} {b  <= d } {c'} (v g) = v (g2 g) where
+--          g2 : Arrows (a ∧ d) b → Arrows ((a ∧ c') ∧ d) b
+--          g2 = {!!}
 
    -- e2 :  {a : Objs } {f : Arrow a ⊤ } → {!!} -- eval f ≡ eval (next (○ a) (id a))
    -- e2 {⊤} {id ⊤} = refl
@@ -243,7 +231,7 @@
    GtoCCC : Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    GtoCCC = record {
             Obj = Objs 
-          ; Hom = Arrow
+          ; Hom = Arrows
           ; _o_ = λ {A} {B} {C} f g → f ・ g
           ; _≈_ = λ {a} {b} f g → {!!}
           ; Id  = λ {a} → {!!}