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  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 } → Arrows (c ∧ b ) a → Arrow c ( a <= b )        --- case v

   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
      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 g ・ h = iv f ( g ・ h )

   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 f g} = cong (λ k → iv f k ) identityR
   identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
   identityL = refl
   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 , f₁ > g h = cong₂ (λ j k → < j  , k > )  (associative f g h) (associative f₁ g h) 
   associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h )

   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  
              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-≈ refl refl = refl 


   eval :  {a b : Objs } (f : Arrows a b ) → Arrows a b
   eval (id a) = id a
   eval (○ a) = ○ a
   eval < f , f₁ > = < eval f , eval f₁ >
   eval (iv (f *) (id a)) = iv ((eval f) *) (id a)
   eval (iv f (id a)) = iv f (id a)
   eval (iv (f *) (○ a)) = iv ((eval f)*) (○ a)
   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 ((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 ((eval f)*) (id a)  
   eval (iv f (iv g h)) | id a = iv f (id a)  
   eval (iv (f *) (iv g h)) | ○ a = iv ((eval f)*) (○ a)
   eval (iv π (iv g h)) | < t , t₁ > = t
   eval (iv π' (iv g h)) | < t , t₁ > = t₁
   eval (iv ε (iv g h)) | < t , t₁ > =  iv ε < t , t₁ > 
   eval (iv (f *) (iv g h)) | < t , t₁ > = iv ((eval f) *) < t , t₁ > 
   eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) 

   refl-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → f ≡ f1
   refl-<l> refl = refl

   refl-<r> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → g ≡ g1
   refl-<r> refl = refl

   idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f

   iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c  ) ( g : Arrows a (atom b) )
           → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g)
   iv-e-arrow x (id (atom _)) = refl
   iv-e-arrow x (iv f g) with eval (iv f g) 
   iv-e-arrow x (iv f g) | id (atom _) = refl
   iv-e-arrow x (iv f g) | iv f₁ t = refl
   iv-e-ε : { a b c : Objs } → ( g : Arrows a ((c <= b) ∧ b ) )
           → eval (iv ε g) ≡ iv ε (eval g)
   iv-e-ε (id _) = refl
   iv-e-ε < g , g₁ > = refl
   iv-e-ε (iv f g) with eval (iv f g) 
   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 : Arrows (d ∧ b) c} → ( g : Arrows a d )
           → eval (iv (f *) g) ≡ iv ((eval f) *) (eval g)
   iv-e-* (id a) = refl
   iv-e-* (○ a) = refl
   iv-e-* < g , g₁ > = refl
   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
   iv-e-* (iv f g) | < t , t₁ > = refl
   iv-e-* (iv (f *) g) | iv f₁ t = {!!}
   iv-e-* (iv f g) | iv f₁ t = {!!}

   iv-e : { a b c : Objs } → (x : Arrow b c ) ( f : Arrows a b) 
           → { d : Objs } { y : Arrow d b } { g : Arrows a d } → eval f ≡ iv y g 
           → eval (iv x f) ≡ iv x (eval f)
   iv-e x (id a) ()
   iv-e x (○ a) ()
   iv-e x < f , f₁ > ()
   iv-e x (iv f g) {_} {y} {h} eq with eval (iv f g) 
   iv-e x (iv f g) {_} {y} {h} refl | iv y h = {!!}

   π-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c )
      → eval g ≡ < f1 , f2 > → eval (iv π g ) ≡ f1
   π-lemma < g , g₁ > f1 f2 refl = refl
   π-lemma (iv π g) f1 f2 eq with eval (iv π g)
   π-lemma (iv π g) f1 f2 refl | < t , t₁ > = refl
   π-lemma (iv π' g) f1 f2 eq with eval (iv π' g)
   π-lemma (iv π' g) f1 f2 refl | < t , t₁ > = refl
   π-lemma (iv ε g) f1 f2 eq with eval (iv ε g)
   π-lemma (iv ε g) f1 f2 refl | < t , t₁ > = refl

   π'-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c )
      → eval g ≡ < f1 , f2 > → eval (iv π' g ) ≡ f2
   π'-lemma < g , g₁ > f1 f2 refl = refl
   π'-lemma (iv π g) f1 f2 eq with eval (iv π g)
   π'-lemma (iv π g) f1 f2 refl | < t , t₁ > = refl
   π'-lemma (iv π' g) f1 f2 eq with eval (iv π' g)
   π'-lemma (iv π' g) f1 f2 refl | < t , t₁ > = refl
   π'-lemma (iv ε g) f1 f2 eq with eval (iv ε g)
   π'-lemma (iv ε g) f1 f2 refl | < t , t₁ > = refl

   iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g))
   iv-d (arrow x) g = begin
          eval (iv (arrow x) g) 
        ≡⟨ iv-e-arrow x g ⟩
          iv (arrow x) (eval g)
        ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩
          iv (arrow x) (eval (eval g))
        ≡⟨ sym (iv-e-arrow x (eval g)) ⟩
          eval (iv (arrow x) (eval g))
        ∎  where open ≡-Reasoning
   iv-d π (id _) = refl
   iv-d π < g , g₁ > = sym (idem-eval g)
   iv-d π (iv x f ) with eval (iv x f) | inspect eval (iv x f)
   ... | id _ | m = refl
   ... | < f1 , f2 > | record {eq = ee } = begin
           f1
        ≡⟨ sym ( π-lemma (iv x f) f1 f2 ee ) ⟩
           eval (iv π (iv x f))
        ≡⟨ sym (idem-eval (iv π (iv x f))) ⟩
           eval (eval (iv π (iv x f)))
        ≡⟨ cong (λ k → eval k ) (π-lemma (iv x f) f1 f2 ee ) ⟩
           eval f1 
        ∎  where open ≡-Reasoning
   iv-d π (iv x f) | iv x1 f1 | record { eq = ee }  = begin
           iv π (iv x1 f1)
        ≡⟨ sym (cong (λ k → iv π k ) ee) ⟩
           iv π (eval (iv x f))
        ≡⟨ sym (iv-e π (iv x f) ee )  ⟩
           eval (iv π (iv x f))
        ≡⟨ sym (idem-eval (iv π (iv x f))) ⟩
           eval (eval (iv π (iv x f)))
        ≡⟨ cong (λ k → eval k ) ( iv-e π (iv x f) ee ) ⟩
           eval (iv π (eval (iv x f)))
        ≡⟨ cong (λ k → eval (iv π k)) ee ⟩
           eval (iv π (iv x1 f1))
        ∎  where open ≡-Reasoning
   iv-d π' (id _) = refl
   iv-d π' < g , g₁ > = sym (idem-eval g₁)
   iv-d π' (iv x f ) with eval (iv x f) | inspect eval (iv x f)
   ... | id _ | m = refl
   ... | < f1 , f2 > | record {eq = ee } = begin
           f2
        ≡⟨ sym ( π'-lemma (iv x f) f1 f2 ee ) ⟩
           eval (iv π' (iv x f))
        ≡⟨ sym (idem-eval (iv π' (iv x f))) ⟩
           eval (eval (iv π' (iv x f)))
        ≡⟨ cong (λ k → eval k ) (π'-lemma (iv x f) f1 f2 ee ) ⟩
           eval f2 
        ∎  where open ≡-Reasoning
   iv-d π' (iv x f) | iv x1 f1 | record { eq = ee }  = begin
           iv π' (iv x1 f1)
        ≡⟨ sym (cong (λ k → iv π' k ) ee) ⟩
           iv π' (eval (iv x f))
        ≡⟨ sym (iv-e π' (iv x f) ee )  ⟩
           eval (iv π' (iv x f))
        ≡⟨ sym (idem-eval (iv π' (iv x f))) ⟩
           eval (eval (iv π' (iv x f)))
        ≡⟨ cong (λ k → eval k ) ( iv-e π' (iv x f) ee ) ⟩
           eval (iv π' (eval (iv x f)))
        ≡⟨ cong (λ k → eval (iv π' k)) ee ⟩
           eval (iv π' (iv x1 f1))
        ∎  where open ≡-Reasoning
   iv-d ε g = begin
            eval (iv ε g)
        ≡⟨ iv-e-ε g ⟩
          iv ε (eval g)
        ≡⟨ cong (λ k → iv ε k ) ( sym ( idem-eval g) ) ⟩
          iv ε (eval (eval g))
        ≡⟨ sym (iv-e-ε (eval g)) ⟩
          eval (iv ε (eval g))
        ∎  where open ≡-Reasoning
   iv-d (x *) g = begin
            eval (iv (x *) g)
        ≡⟨ iv-e-* g ⟩
          iv ((eval x) *) (eval g)
        ≡⟨ cong (λ k → iv ((eval x) *) k ) ( sym ( idem-eval g) ) ⟩
          iv ((eval x) *) (eval (eval g))
        ≡⟨ sym (iv-e-* (eval g)) ⟩
          eval (iv (x *) (eval g))
        ∎  where open ≡-Reasoning

   idem-eval (id a) = refl
   idem-eval (○ a) = refl
   idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁)
   idem-eval (iv (f *) (id a)) = {!!}
   idem-eval (iv f (id a)) = {!!}
   idem-eval (iv (f *) (○ a)) = {!!}
   idem-eval (iv f (○ a)) = {!!}
   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 ((eval 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 | _ = {!!}
   idem-eval (iv f (iv g h)) | ○ a | m | _ = {!!}
   idem-eval (iv π (iv g h)) | < t , t₁ > | m | _ = refl-<l> {!!}
   idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<r> {!!}
   idem-eval (iv ε (iv g h)) | < t , t₁ > | m | _ = {!!} -- cong ( λ k → iv ε k ) ?
   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
           {!!}
        ≡⟨ {!!} ⟩
          eval (iv π ( iv f₁ t))
        ≡⟨ {!!} ⟩
          eval (iv π (eval (iv g h )))
        ≡⟨ {!!} ⟩
          eval (iv π (iv g h)) 
        ≡⟨ iv-e π (iv g h) ee ⟩
          iv π (eval (iv g h))
        ≡⟨ cong (λ k → iv π k ) ee  ⟩
          iv π ( iv f₁ t)
        ≡⟨ {!!} ⟩
           {!!}
        ∎  where open ≡-Reasoning
   idem-eval (iv π' (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!}
   idem-eval (iv (arrow x) (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!} -- trans (iv-e-arrow x (iv f₁ t)) (cong ( λ k → iv (arrow x) k ) m )  

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


   fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B
   fmap f = {!!}

   PLCCC :  Functor PL PL
   PLCCC = record {
         FObj = λ x → x
       ; FMap = fmap
       ; isFunctor = record {
              identity = {!!}
            ; distr = {!!}
            ; ≈-cong = {!!}
          }
      }