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

   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 f (id a)
   eval (iv f (○ a)) = iv 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 (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)
   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 (f *) < t , t₁ > 
   eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) 

   pi : {a b c : Objs} → Arrows a ( b ∧ c) → Arrows a b
   pi (id .(_ ∧ _)) = iv π (id _)
   pi < x , x₁ > = x
   pi (iv f x) =  iv π (iv f x)

   pi' : {a b c : Objs} → Arrows a ( b ∧ c) → Arrows a c
   pi' (id .(_ ∧ _)) = iv π' (id _)
   pi' < x , x₁ > = x₁
   pi' (iv f x) =  iv π' (iv f x)

   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

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

   _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
   _==_ {a} {b} x y   = eval x  ≡ eval  y 

   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
   identityR {a} {.a} {id a} = refl
   identityR {a} {⊤} {○ a} = refl
   identityR {_} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
   identityR {_} {_} {iv f (id a)} = refl
   identityR {_} {_} {iv f (○ a)} = refl
   identityR {_} {_} {iv π < g , g₁ >} = identityR {_} {_} {g} 
   identityR {_} {_} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} 
   identityR {_} {_} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
   identityR {_} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
   identityR {_} {_} {iv f (iv g h)} = {!!}

   open import Data.Empty 
   open import Relation.Nullary 

   open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)

   std-iv : {a b c d : Objs} (x : Arrow c d) (y : Arrow b c ) (f : Arrows a b) 
        →  ( {b1 b2 : Objs } → {g : Arrows a b1 } {h : Arrows a b2 } → ¬ (eval f) ≅ < g , h > )
        → eval (iv x ( iv y f ) ) ≡ iv x ( eval (iv y f ) )
   std-iv x y (id a) _ = refl
   std-iv x y (○ a) _ = refl
   std-iv x y < f , f₁ > ne = ⊥-elim (ne refl)
   std-iv x y (iv z f) ne with eval (iv z f) 
   std-iv x y (iv z f) ne | id a = refl
   std-iv x y (iv z f) ne | ○ a = refl
   std-iv x y (iv z f) ne | < t , t₁ > = ⊥-elim (ne refl)
   std-iv (arrow x) _ (iv z f) ne | iv z1 t = refl
   std-iv π y (iv z f) ne | iv z1 t = refl
   std-iv π' y (iv z f) ne | iv z1 t = refl
   std-iv ε y (iv z f) ne | iv z1 t = refl
   std-iv (x *) y (iv z f) ne | iv z1 t = refl

   std-iv' : {a b c : Objs}  (y : Arrow b c ) (f : Arrows a b) 
        →  ( {b1 b2 : Objs } → {g : Arrows a b1 } {h : Arrows a b2 } → ¬ (eval f) ≅ < g , h > )
        → eval ( iv y f )  ≡  iv y (eval f ) 
   std-iv' y (id a) ne = refl
   std-iv' y (○ a) ne = refl
   std-iv' y < f , f₁ > ne = ⊥-elim (ne refl)
   std-iv' y (iv f z) ne with eval (iv f z)  
   std-iv' y (iv f z) ne | id a = refl
   std-iv' y (iv f z) ne | ○ a = refl
   std-iv' y (iv f z) ne | < t , t₁ > = ⊥-elim (ne refl)
   std-iv' (arrow x) (iv f z) ne | iv f₁ t = refl
   std-iv' π (iv f z) ne | iv f₁ t = refl
   std-iv' π' (iv f z) ne | iv f₁ t = refl
   std-iv' ε (iv f z) ne | iv f₁ t = refl
   std-iv' (y *) (iv f z) ne | iv f₁ t = refl

   idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
   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)) = refl
   idem-eval (iv f (○ a)) = refl
   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 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)) | iv f₁ t | m | record { eq = ee } = {!!}
   -- trans lemma (cong ( λ k → iv f k ) m )  where
   --   lemma : eval (iv f (iv f₁ t)) ≡ iv f (eval (iv f₁ t))
   --   lemma =  std-iv f f₁ t {!!}

   assoc-iv : {a b c d : Objs} (x : Arrow c d) (f : Arrows b c) (g : Arrows a b ) → eval (iv x (f ・ g)) ≡ eval (iv x f ・ g)
   assoc-iv x (id a) g = {!!}
   assoc-iv x (○ a) g = refl
   assoc-iv π < f , f₁ > g = refl
   assoc-iv π' < f , f₁ > g = refl
   assoc-iv ε < f , f₁ > g = refl
   assoc-iv (x *) < f , f₁ > g = refl
   assoc-iv x (iv f g) h = begin
            eval (iv x (iv f g ・ h)) 
        ≡⟨ {!!} ⟩
            eval (iv x (iv f g) ・ h)
        ∎  where open ≡-Reasoning


   ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
   ==←≡ eq = cong (λ k → eval k ) 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₁ >} = cong₂ (λ j k → < j , k > ) (identityL {_} {_} {f}) (identityL {_} {_} {f₁})
               identityL {_} {_} {iv f f₁} = {!!}
               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 = {!!}
               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 π < f , f1 > ) g h = associative f g h
               associative {a} (iv π' < f , f1 > ) g h = associative f1 g h
               associative {a} (iv ε < f , f1 > ) g h = cong ( λ k → iv ε k ) ( associative  < f , f1 >  g h )
               associative {a} (iv (x *) < f , f1 > ) g h = cong ( λ k → iv (x *) k ) ( associative  < f , f1 >  g h )
               associative {a} (iv x (id _)) g h =  begin
                       eval (iv x (id _) ・ (g ・ h))
                    ≡⟨ {!!} ⟩
                       eval (iv x (g ・ h))
                    ≡⟨ assoc-iv x g h ⟩
                       eval (iv x g ・ h)
                    ≡⟨ {!!} ⟩
                       eval ((iv x (id _) ・ g) ・ h)
                    ∎  where open ≡-Reasoning
               associative {a} (iv x (○ _)) g h =  refl
               associative {a} (iv x (iv y f)) g h = begin
                       eval (iv x (iv y f) ・ (g ・ h))
                    ≡⟨ sym (assoc-iv x (iv y f) ( g ・ h)) ⟩
                       eval (iv x ((iv y f) ・ (g ・ h)))
                    ≡⟨ {!!}  ⟩
                       eval ((iv x (iv y f) ・ g) ・ h)
                    ∎  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 = {!!}