open import Level
open import Category 
module CCCgraph1 where

open import HomReasoning
open import cat-utility
open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import CCC
open import graph

module ccc-from-graph {c₁  c₂  : Level} (G : Graph {c₁} {c₂} )  where
   open Graph
   
   data Objs : Set (c₁ ⊔ c₂) where
      atom : (vertex G) → Objs 
      ⊤ : Objs 
      _∧_ : Objs  → Objs  → Objs 
      _<=_ : Objs → Objs → Objs 

   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where
      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
      <_,_> : {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

   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') 

   eval1 :  {a b c : Objs } (f : Arrow b c ) → (g : Arrow a b) → Arrows a c
   eval1 {a} {_} {⊤} _ _ = i ( ○ a )
   eval1 f (id a)  = i f
   eval1 (arrow x) g = iv (i (arrow x)) g
   eval1 π < f , g > = i f
   eval1 π g = iv (i π) g
   eval1 π' < f , g > = i g
   eval1 π' g = iv (i π') g
   eval1 ε g = iv (i ε) g
   eval1 < f , g > h = iv (i < f , g >) h
   eval1 (f *) g = iv (i (f *)) g
   eval1 (id a) g = i g

   eval :  {a b c : Objs } (f : Arrow b c ) → (g : Arrows a b) → Arrows a c
   eval {a} {_} {⊤} _ _ = i ( ○ a )
   eval f (i k) = eval1 f k
   eval (id _) f = f
   eval π (iii g h) = g
   eval π' (iii g h) = h
   eval ε (iii g h) = {!!} -- {!!} ・ h -- g  : Arrows a (c <= b)
   eval < f , g > (iii j h) = iii (eval f (iii j h)) (eval g (iii j h))
   eval (f *) (iii g h) = {!!}
   eval f (iv g h) with eval f g
   ... | i k = eval1 k h
   ... | k = iv k h
   eval < f , g > (v h) = iii (eval f (v h)) (eval g (v h))
   eval (f *) (v g) = {!!}

   _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
   _・_ {a} {_} {⊤} _ _ = i ( ○ a )
   i (id _)  ・ f = f
   f ・ i (id _)  = f
   (iv f g) ・ h  = f ・ eval g h 
   f ・ (iv g h)  = iv ( f ・ g ) h
   i f ・ g = eval f g 
   iii f g ・  h = iii (f ・ h) ( g ・ h )
   v f ・ g = v ( f ・ iii (iv g π ) (i π') )