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 import  Relation.Binary.PropositionalEquality hiding ( [_] )
   open import  Relation.Binary.Core 
   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                       --- 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

   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  >
   f ・ id b = f
   iv f (id _) ・ h = iv f h
   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₂)
   _==_ {a} {b} x y   = (x  ・ id _ ) ≡ ( y ・ id _ )

   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≡  identityR≡  
   identityR≡ {a} {b} {iv x y} = refl
   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
   identityR {a} {b} {f} = cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} )

   ≡←== : {A B : Objs} {f g : Arrows A B} → f == g → f ≡ g
   ≡←== eq = subst₂ (λ j k → j ≡ k ) identityR≡ identityR≡ eq

   ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
   ==←≡ eq = cong (λ k → k ・ id _) eq

   PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
   PL = record {
            Obj  = Objs;
            Hom = λ a b →  Arrows  a b ;
            _o_ =  λ{a} {b} {c} x y → x ・ y ;
            _≈_ =  λ x y → x  == y ;
            Id  =  λ{a} → id a ;
            isCategory  = record {
                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
                    identityL  = λ {a b f} → identityL {a} {b} {f} ; 
                    identityR  = λ {a b f} → identityR {a} {b} {f} ; 
                    o-resp-≈  = λ {a b c f g h i} → o-resp-≈ {a} {b} {c} {f} {g} {h} {i}  ; 
                    associative  = λ{a b c d f g h } → associative  f g h
               }
           }  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
               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
               associative (○ a) g h = refl
               associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
               associative {a} (iv x f) g h = begin
                      (iv x f ・ (g ・ h)) ・ id a
                    ≡⟨ cong ( λ k → k ・ id a) (assoc-iv x f ( g ・ h )) ⟩
                      iv x (f ・ (g ・ h)) ・ id a
                    ≡⟨ cong ( λ k → iv x k ・ id a) (≡←== (associative f g _ ) ) ⟩
                      iv x ((f ・ g ) ・ h) ・ id a
                    ≡⟨ sym (cong ( λ k → k ・ id a) (assoc-iv x (f ・ g ) _))  ⟩
                      ( iv x (f ・ g ) ・ h) ・ id a
                    ≡⟨ sym (cong ( λ k → (k ・  h ) ・ id a) (assoc-iv x f _)) ⟩
                      ((iv x f ・ g) ・ h) ・ id a
                    ∎  where open ≡-Reasoning
                    --  {!!} ( cong ( λ k → iv x k ) ( ≡←== (associative f g h ) ) ) 
               o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
                            f == g → h == i → (h ・ f) == (i ・ g)
               o-resp-≈  f=g h=i = {!!}