open import Level
open import Category 
module CCCgraph where

open import HomReasoning
open import cat-utility
open import Data.Product renaming (_×_ to _/\_  ) hiding ( <_,_> )
open import Category.Constructions.Product
open  import  Relation.Binary.PropositionalEquality hiding ( [_] )
open import CCC

open Functor

--   ccc-1 : Hom A a 1 ≅ {*}
--   ccc-2 : Hom A c (a × b) ≅ (Hom A c a ) × ( Hom A c b )
--   ccc-3 : Hom A a (c ^ b) ≅ Hom A (a × b) c

open import Category.Sets

------------------------------------------------------
-- Sets is a CCC
------------------------------------------------------

postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂

data One {l : Level}  : Set l where
  OneObj : One   -- () in Haskell ( or any one object set )

sets : {l : Level } → CCC (Sets {l})
sets {l} = record {
         １  = One
       ; ○ = λ _ → λ _ → OneObj
       ; _∧_ = _∧_
       ; <_,_> = <,>
       ; π = π
       ; π' = π'
       ; _<=_ = _<=_
       ; _* = _*
       ; ε = ε
       ; isCCC = isCCC
  } where
         １ : Obj Sets 
         １ = One 
         ○ : (a : Obj Sets ) → Hom Sets a １
         ○ a = λ _ → OneObj
         _∧_ : Obj Sets → Obj Sets → Obj Sets
         _∧_ a b =  a /\  b
         <,> : {a b c : Obj Sets } → Hom Sets c a → Hom Sets c b → Hom Sets c ( a ∧ b)
         <,> f g = λ x → ( f x , g x )
         π : {a b : Obj Sets } → Hom Sets (a ∧ b) a
         π {a} {b} =  proj₁ 
         π' : {a b : Obj Sets } → Hom Sets (a ∧ b) b
         π' {a} {b} =  proj₂ 
         _<=_ : (a b : Obj Sets ) → Obj Sets
         a <= b  = b → a
         _* : {a b c : Obj Sets } → Hom Sets (a ∧ b) c → Hom Sets a (c <= b)
         f * =  λ x → λ y → f ( x , y )
         ε : {a b : Obj Sets } → Hom Sets ((a <= b ) ∧ b) a
         ε {a} {b} =  λ x → ( proj₁ x ) ( proj₂ x )
         isCCC : CCC.IsCCC Sets １ ○ _∧_ <,> π π' _<=_ _* ε
         isCCC = record {
               e2  = e2
             ; e3a = λ {a} {b} {c} {f} {g} → e3a {a} {b} {c} {f} {g}
             ; e3b = λ {a} {b} {c} {f} {g} → e3b {a} {b} {c} {f} {g}
             ; e3c = e3c
             ; π-cong = π-cong
             ; e4a = e4a
             ; e4b = e4b
             ; *-cong = *-cong
           } where
                e2 : {a : Obj Sets} {f : Hom Sets a １} → Sets [ f ≈ ○ a ]
                e2 {a} {f} = extensionality Sets ( λ x → e20 x )
                  where
                        e20 : (x : a ) → f x ≡ ○ a x
                        e20 x with f x
                        e20 x | OneObj = refl
                e3a : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
                    Sets [ ( Sets [  π  o ( <,> f g)  ] ) ≈ f ]
                e3a = refl
                e3b : {a b c : Obj Sets} {f : Hom Sets c a} {g : Hom Sets c b} →
                    Sets [ Sets [ π' o ( <,> f g ) ] ≈ g ]
                e3b = refl
                e3c : {a b c : Obj Sets} {h : Hom Sets c (a ∧ b)} →
                    Sets [ <,> (Sets [ π o h ]) (Sets [ π' o h ]) ≈ h ]
                e3c = refl
                π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
                    Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ <,> f g ≈ <,> f' g' ]
                π-cong refl refl = refl
                e4a : {a b c : Obj Sets} {h : Hom Sets (c ∧ b) a} →
                    Sets [ Sets [ ε o <,> (Sets [ h * o π ]) π' ] ≈ h ]
                e4a = refl
                e4b : {a b c : Obj Sets} {k : Hom Sets c (a <= b)} →
                    Sets [ (Sets [ ε o <,> (Sets [ k o π ]) π' ]) * ≈ k ]
                e4b = refl
                *-cong : {a b c : Obj Sets} {f f' : Hom Sets (a ∧ b) c} →
                    Sets [ f ≈ f' ] → Sets [ f * ≈ f' * ]
                *-cong refl = refl


--------
--
-- Graph to positive logic
--

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

   data _≐_ : {a b : Objs } → Arrows a b → Arrows a b → Set ℓ where
       prefl : {a b : Objs } → {f : Arrows a b } → f ≐ f
       p⊤ : {a : Objs } → {f g : Arrows a ⊤ } → f ≐ g
       <p> : {a b c : Objs } → {f h : Arrows a b } {g i : Arrows a c } → f ≐ h → g ≐ i → < f , g > ≐ < h , i >
       piv : {a b c : Objs } → {f : Arrow b c } {g i : Arrows a b } → g ≐ i → iv f  g  ≐ iv f  i 
       aiv : { a : Objs } {b c :  vertex G } → {f h : edge G b c } → {g i : Arrows a (atom b) } → _≅_ G f h → g ≐ i → iv (arrow f)  g  ≐ iv (arrow h)  i 

   psym : {a b : Objs } → { f g  : Arrows a b} → f ≐ g → g ≐ f 
   psym prefl = prefl
   psym p⊤ = p⊤
   psym (<p> eq eq₁) = <p> (psym eq) (psym eq₁)
   psym (piv eq) = piv (psym eq)
   psym (aiv x eq) = aiv (IsEquivalence.sym (Graph.isEq G) x) (psym eq)

   ptrans : {a b : Objs } → { f g h : Arrows a b} → f ≐ g → g ≐ h → f ≐ h
   ptrans prefl g=h = g=h
   ptrans p⊤ g=h = p⊤
   ptrans (<p> f=g f=g₁) prefl = <p> f=g f=g₁
   ptrans (<p> f=g f=g₁) (<p> g=h g=h₁) = <p> ( ptrans f=g g=h ) ( ptrans f=g₁ g=h₁ )
   ptrans (piv f=g) prefl = piv f=g
   ptrans (piv f=g) p⊤ = p⊤
   ptrans (piv f=g) (piv g=h) = piv ( ptrans f=g g=h )
   ptrans (piv f=g) (aiv x g=h) = aiv x (ptrans f=g g=h)
   ptrans (aiv x f=g) prefl = aiv x f=g
   ptrans (aiv x f=g) (piv g=h) =  aiv x (ptrans f=g g=h)
   ptrans (aiv x f=g) (aiv x₁ g=h) = aiv (IsEquivalence.trans (Graph.isEq G) x x₁) (ptrans f=g g=h) 

   identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≐ f
   identityL = prefl

   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≐ f
   identityR {a} {a} {id a} = prefl
   identityR {a} {⊤} {○ a} = p⊤
   identityR {a} {_} {< f , f₁ >} = <p> identityR identityR
   identityR {a} {b} {iv f g} = piv identityR

   assoc≐ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
                            (f ・ (g ・ h)) ≐ ((f ・ g) ・ h)
   assoc≐ (id a) g h = prefl
   assoc≐ (○ a) g h = p⊤
   assoc≐ < f , f₁ > g h = <p> (assoc≐ f g h) (assoc≐ f₁ g h) 
   assoc≐ (iv f f1) g h = piv ( assoc≐ f1 g h )

   -- positive intutionistic calculus
   PL :  Category  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 = prefl ; trans = ptrans ; sym = psym} ;
                    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 } → assoc≐  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-≈ {_} {_} {⊤} {f} {g} {h} {i} f=g h=i = p⊤
              o-resp-≈ {_} {_} {_} {f} {g} {id a} {id a} f=g h=i = ptrans (ptrans f=g (psym identityR) ) identityR
              o-resp-≈ {_} {_} {_} {f} {g} {< h , h₁ >} {< h , h₁ >} f=g prefl = <p> (o-resp-≈ f=g prefl ) (o-resp-≈ f=g prefl )
              o-resp-≈ {_} {_} {_} {f} {g} {< h , h₁ >} {< i , i₁ >} f=g (<p> h=i h=i₁) = <p> (o-resp-≈ f=g h=i ) (o-resp-≈ f=g h=i₁)
              o-resp-≈ {_} {_} {_} {f} {g} {iv f₁ h} {iv f₁ h} f=g prefl = piv ( o-resp-≈ f=g prefl )
              o-resp-≈ {_} {_} {_} {f} {g} {iv f₁ h} {iv f₁ i} f=g (piv h=i) = piv ( o-resp-≈ f=g  h=i)
              o-resp-≈ {_} {_} {_} {f} {g} {iv (arrow x) h} {iv (arrow y) i} f=g (aiv x=y h=i) = aiv x=y (o-resp-≈ f=g  h=i)


--------
--
-- Functor from Positive Logic to Sets
--

   -- open import Category.Sets
   -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂

   C = graphtocat.Chain G

   tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
   tr f x y  = graphtocat.next f (x y) 
   
   fobj :  ( a  : Objs  ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
   fobj  (atom x) = ( y : vertex G ) → C y x
   fobj ⊤ = One
   fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
   fobj  (a <= b) = fobj  b → fobj  a

   fmap :  { a b : Objs  } → Hom PL a b → fobj  a → fobj  b
   amap :  { a b : Objs  } → Arrow  a b → fobj  a → fobj  b
   amap  (arrow x) =  tr x
   amap π ( x , y ) = x 
   amap π' ( x , y ) = y
   amap ε (f , x ) = f x
   amap (f *) x = λ y →  fmap f ( x , y ) 
   fmap (id a) x = x
   fmap (○ a) x = OneObj
   fmap < f , g > x = ( fmap f x , fmap g x )
   fmap (iv x f) a = amap x ( fmap f a )


--   CS is a map from Positive logic to Sets
--    Sets is CCC, so we have a cartesian closed category generated by a graph
--       as a sub category of Sets

   smallGraph : (G : Graph {c₁} { c₂} {ℓ} ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
   smallGraph G = {b c :  vertex G } → {f h : edge G b c } →  _≅_ G f h  → f ≡ h

   CS :  smallGraph G → Functor PL (Sets {c₁ ⊔ c₂ ⊔ ℓ})
   FObj (CS sg) a  = fobj  a
   FMap (CS sg) {a} {b} f = fmap  {a} {b} f
   isFunctor ( CS sg) = isf where
        _+_ = Category._o_ PL
        ++idR = IsCategory.identityR ( Category.isCategory PL )
        distr : {a b c : Obj PL}  { f : Hom PL a b } { g : Hom PL b c } → (z : fobj  a ) → fmap (g + f) z ≡ fmap g (fmap f z)
        distr {a} {a₁} {a₁} {f} {id a₁} z = refl
        distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
        distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k  →  j , k  ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z)
        distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr  {a} {b} {d} {f} {g} z) x where 
           adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
                ( x : Arrow d c ) → fmap ( iv x (g + f) ) z  ≡ fmap ( iv x g ) (fmap f z )
           adistr eq x = cong ( λ k → amap x k ) eq
        isf : IsFunctor PL Sets fobj fmap 
        IsFunctor.identity isf = extensionality Sets ( λ x → refl )
        IsFunctor.≈-cong isf f=g = extensionality Sets ( λ x → lemma _ _ f=g ) where
           lemma : {a b : Obj PL} → {x : fobj a } → (f g : Hom PL a b ) → PL [ f ≈ g ] → fmap f x ≡ fmap g x
           lemma f f prefl = refl
           lemma {a} {⊤} {x} f g p⊤ with fmap f x | fmap g x
           lemma {a} {⊤} {x} f g p⊤ | OneObj | OneObj = refl
           lemma (< f , g >) (< h , i >) (<p> f=h g=i) = cong₂ (λ j k → ( j , k ) ) (lemma f h f=h) (lemma g i g=i) 
           lemma {_} {_} {x} (iv f g) (iv f i) (piv g=i) = cong ( λ k → amap f k ) (lemma g i g=i)
           lemma (iv (arrow x) f) (iv (arrow y) g) (aiv x=y f=g) = cong₂ ( λ j k → amap (arrow j) k ) (sg x=y ) (lemma f g f=g)
        IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 

   open import subcat

   CSC = λ (gs : smallGraph G) → FCat PL (Sets {c₁ ⊔ c₂ ⊔ ℓ}) (CS gs)

   cc1 : (gs : smallGraph G) → CCC (CSC gs)      -- SCS is CCC
   cc1 gs = record {
         １ = ⊤ ;
         ○ =  λ a x → OneObj ;
         _∧_ = λ x y →  x ∧ y   ;
         <_,_> = λ f g x  → ( f x , g x ) ;
         π = proj₁ ;
         π' = proj₂ ;
         _<=_ = λ b a → b <= a ;
         _* = λ f x y → f ( x , y ) ;
         ε = λ x → ( proj₁ x) (proj₂ x) ;
         isCCC = record {
               e2  = λ {a} {f} → extensionality Sets ( λ x → e20 {a} {f} x ) ;
               e3a = refl ;
               e3b = refl ;
               e3c = refl ;
               π-cong = π-cong ;
               e4a = refl ;
               e4b = refl ;
               *-cong = *-cong
           }
     } where
        e20 : {a : Obj (CSC gs) } {f : Hom (CSC gs) a ⊤} (x : fobj a ) → f x ≡ OneObj
        e20 {a} {f} x with f x
        e20 x | OneObj = refl
        π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
                    Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
        π-cong refl refl = refl
        *-cong : {a b c : Obj (CSC gs) } {f f' : Hom (CSC gs) (a ∧ b) c} →
                    Sets [ f ≈ f' ] → Sets [  (λ x y → f (x , y)) ≈ (λ x y → f' (x , y)) ]
        *-cong refl = refl

------------------------------------------------------
--  Cart     Category of CCC and CCC preserving Functor
------------------------------------------------------

---
---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
---
---     CCC ( SC (CS G)) Sets   have to be proved
---  SM can be eliminated if we have
---    sobj (a : vertex g ) → {a}              a set have only a
---    smap (a b : vertex g ) → {a} → {b}


record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
   field
     cat : Category c₁ c₂ ℓ
     csmall : {a b : Obj cat } → { f g : Hom cat a b } → cat [ f ≈ g ] → f ≡ g
     ccc : CCC cat
 
open CCCObj 
 
record CCCMap  {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
   field
     cmap : Functor (cat A ) (cat B )
     ccf :  CCC (cat A) → CCC (cat B)

open import Category.Cat

open  CCCMap
open import Relation.Binary.Core

Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ))
Cart {c₁} {c₂} {ℓ} = record {
    Obj = CCCObj {c₁} {c₂} {ℓ}
  ; Hom = CCCMap
  ; _o_ = λ {A} {B} {C} f g → record { cmap = (cmap f) ○ ( cmap g ) ; ccf = λ _ → ccf f ( ccf g (ccc A )) }
  ; _≈_ = λ {a} {b} f g → cmap f ≃ cmap g
  ; Id  = λ {a} → record { cmap = identityFunctor ; ccf = λ x → x }
  ; isCategory = record {
     isEquivalence = λ {A} {B} → record {
          refl = λ {f} →  let open ≈-Reasoning (CAT) in refl-hom {cat A} {cat B} {cmap f} 
        ; sym = λ {f} {g}  → let open ≈-Reasoning (CAT) in sym-hom {cat A} {cat B} {cmap f} {cmap g} 
        ; trans = λ {f} {g} {h} → let open ≈-Reasoning (CAT) in trans-hom {cat A} {cat B} {cmap f} {cmap g} {cmap h}  }
     ; identityL = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idL {cat x} {cat y} {cmap f} {_} {_}
     ; identityR = λ {x} {y} {f} → let open ≈-Reasoning (CAT) in idR {cat x} {cat y} {cmap f}
     ; o-resp-≈ = λ {x} {y} {z} {f} {g} {h} {i}  → IsCategory.o-resp-≈ ( Category.isCategory CAT) {cat x}{cat y}{cat z} {cmap f} {cmap g} {cmap h} {cmap i}
     ; associative =  λ {a} {b} {c} {d} {f} {g} {h} → let open ≈-Reasoning (CAT) in assoc {cat a} {cat b} {cat c} {cat d} {cmap f} {cmap g} {cmap h}
   }} 

------------------------------------------------------
--  Grph     Category of Graph and Graph mapping
------------------------------------------------------

open import graph
open Graph

record GMap {v v'  ℓ : Level} (x y : Graph {v} {v'} {ℓ} )  : Set (suc (v ⊔ v' ⊔ ℓ) ) where
  field
   vmap : vertex x → vertex y
   emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
   econg : {a b : vertex x} → { f g : edge x a b } →  Graph._≅_ x f g  → Graph._≅_ y (emap f) (emap g)

open GMap

-- open import Relation.Binary.HeterogeneousEquality using (_≅_;refl ) renaming ( sym to ≅-sym ; trans to ≅-trans ; cong to ≅-cong )

data [_]_==_ {c₁ c₂ ℓ} (C : Graph {c₁} {c₂} {ℓ}) {A B : vertex C} (f : edge C A B)
     : ∀{X Y : vertex C} → edge C X Y → Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
  mrefl : {g : edge C A B} → (eqv : Graph._≅_ C f g ) → [ C ] f == g

_=m=_ : ∀ {c₁ c₂ ℓ} {C D : Graph {c₁} {c₂} {ℓ}} 
    → (F G : GMap C D) → Set (suc (c₂ ⊔ c₁ ⊔ ℓ))
_=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f

_&_ :  {v v' ℓ : Level} {x y z : Graph {v} {v'} {ℓ}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
f & g = record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) ; econg = λ eq → econg f ( econg g eq) }

erefl : {v v' ℓ : Level}  (C : Graph {v} {v'} {ℓ}) → { x y : vertex C } → {f : edge C x y }  → Graph._≅_ C f f
erefl C = IsEquivalence.refl (Graph.isEq C)

Grph : {v v' ℓ : Level} → Category (suc (v ⊔ v' ⊔ ℓ )) (suc (v ⊔ v' ⊔ ℓ)) (suc ( v ⊔ v' ⊔ ℓ))
Grph {v} {v'} {ℓ} = record {
    Obj = Graph {v} {v'} {ℓ}
  ; Hom = GMap {v} {v'}
  ; _o_ = _&_
  ; _≈_ = _=m=_
  ; Id  = record { vmap = λ y → y ; emap = λ f → f ; econg = λ eq → eq }
  ; isCategory = record {
       isEquivalence = λ {A} {B} →  ise
     ; identityL = λ {a} {b} {f} e → mrefl ( erefl b )
     ; identityR =  λ {a} {b} {f} e → mrefl ( erefl b)
     ; o-resp-≈ = λ {a} {b} {c} {f} {g} {h} {i} f=g h=i  → m--resp-≈ {a} {b} {c} {f} {g} {h} {i} f=g h=i
     ; associative = λ {a} {b} {c} {d} {f} {g} {h} e → mrefl (erefl d ) 
   }}  where
       msym :  {x y : Graph {v} {v'} {ℓ}}  { f g : GMap x y } → f =m= g → g =m= f
       msym  {x} {y} f=g f = lemma ( f=g f ) where
            lemma  : ∀{a b c d} {f : edge y a b} {g : edge y c d} → [ y ] f == g → [ y ] g == f
            lemma (mrefl Ff≈Gf) = mrefl  (IsEquivalence.sym (Graph.isEq y) Ff≈Gf) 
       mtrans : {x y : Graph {v} {v'} {ℓ}}  { f g h : GMap x y } → f =m= g → g =m= h → f =m= h
       mtrans  {x} {y} f=g g=h f = lemma ( f=g f ) ( g=h f ) where
           lemma : ∀{a b c d e f} {p : edge y a b} {q : edge y c d} → {r : edge y e f}  → [ y ] p == q → [ y ] q == r → [ y ] p == r
           lemma (mrefl eqv) (mrefl eqv₁) = mrefl ( (IsEquivalence.trans (Graph.isEq y)) eqv  eqv₁ )
       ise :  {x y : Graph {v} {v'} {ℓ}}  → IsEquivalence {_} {suc v ⊔ suc v' ⊔ suc ℓ} {_} ( _=m=_  {v} {v'}  {ℓ} {x} {y}) 
       ise  {x} {y} = record {
          refl =  λ {C} f → mrefl (erefl y ) 
        ; sym = λ {x} {y} eq → msym  {_} {_} {x} {y} eq
        ; trans = λ {x} {y} {z} eq → mtrans {_} {_} {x} {y} {z} eq
          }
       m--resp-≈ :  {A B C : Graph {v} {v'}{ℓ} }  
           {f g : GMap A B} {h i : GMap B C} → f =m= g → h =m= i → ( h & f ) =m= ( i & g )
       m--resp-≈ {A} {B} {C} {f} {g} {h} {i} f=g h=i e =
          lemma (emap f e) (emap g e) (emap i (emap g e)) (f=g e) (h=i ( emap g e )) where
            lemma : {a b c d : vertex B } {z w : vertex C } (ϕ : edge B a b) (ψ : edge B c d) (π : edge C z w) →
                [ B ] ϕ  == ψ → [ C ] (emap h ψ) == π → [ C ] (emap h ϕ) == π
            lemma  ϕ ψ π (mrefl f=g ) (mrefl h=i ) = mrefl ( (IsEquivalence.trans (Graph.isEq C)) (econg h f=g ) h=i ) 

------------------------------------------------------
--- CCC → Grph  Forgetful functor
------------------------------------------------------

≃-cong : {c₁ c₂ ℓ : Level}  (B : Category c₁ c₂ ℓ ) → {a b a' b' : Obj B }
      → { f f'   : Hom B a b }
      → { g g' : Hom B a' b' }
      → [_]_~_ B f g → B [ f ≈ f' ] → B [ g ≈ g' ] → [_]_~_ B f' g'
≃-cong B {a} {b} {a'} {b'} {f} {f'} {g} {g'}  (refl {g2} eqv) f=f' g=g' = let open ≈-Reasoning B in refl {_} {_} {_} {B} {a'} {b'} {f'} {g'} ( begin
             f'
          ≈↑⟨ f=f' ⟩
             f
          ≈⟨ eqv  ⟩
             g
          ≈⟨ g=g' ⟩
             g'
          ∎  )
  
fobj : {c₁ c₂ ℓ : Level} → Obj (Cart {c₁} {c₂} {ℓ} )  → Obj (Grph {c₁} {c₂}{ℓ})
fobj a = record { vertex = Obj (cat a) ; edge = Hom (cat a) ; _≅_ = Category._≈_ (cat a) ; isEq = IsCategory.isEquivalence (Category.isCategory (cat a)) }
fmap : {c₁ c₂ ℓ : Level} → {a b : Obj (Cart {c₁} {c₂} {ℓ} ) } → Hom (Cart {c₁} {c₂} {ℓ} ) a b → Hom (Grph {c₁} {c₂}) ( fobj a ) ( fobj b )
fmap f =  record { vmap = FObj (cmap f) ; emap = FMap (cmap f) ; econg = IsFunctor.≈-cong (Functor.isFunctor (cmap f))  }

UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grph {c₁} {c₂} {ℓ} )
FObj UX a = fobj a
FMap UX f =  fmap f
isFunctor UX  = isf where
  isf : IsFunctor Cart Grph fobj fmap
  IsFunctor.identity isf {a} {b} {f} e = mrefl (erefl (fobj a))
  IsFunctor.distr isf {a} {b} {c} f = mrefl (erefl (fobj c))
  IsFunctor.≈-cong isf {a} {b} {f} {g} f=g e = lemma ( (extensionality Sets ( λ z → lemma4 (
               ≃-cong (cat b) (f=g (id1 (cat a) z)) (IsFunctor.identity (Functor.isFunctor (cmap f))) (IsFunctor.identity (Functor.isFunctor (cmap g)))
          )))) (f=g e) where
    lemma4 : {x y : vertex (fobj b) } →  [_]_~_ (cat b)  (id1 (cat b) x) (id1 (cat b) y) → x ≡ y
    lemma4 (refl eqv) = refl 
    lemma : vmap (fmap f) ≡ vmap (fmap g) → [ cat b ] FMap (cmap f) e ~ FMap (cmap g) e → [ fobj b ] emap (fmap f) e == emap (fmap g) e
    lemma refl (refl eqv) = mrefl eqv 


open ccc-from-graph.Objs
open ccc-from-graph.Arrow
open ccc-from-graph.Arrows
open graphtocat.Chain

ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {c₁} {c₁} {c₁ } ) (Cart {c₁} {c₁} {c₁} ) UX
ccc-graph-univ {c₁}   = record {
     F = λ g → csc g ;
     η = λ a → record { vmap = λ y → atom y ; emap = λ f x y →  next f (x y) ; econg = λ eq → econg1 a _ _ eq } ;
     _* = {!!} ;
     isUniversalMapping = record {
         universalMapping = {!!} ;
         uniquness = {!!}
      }
  } where
       csc : Graph → Obj Cart
       csc g = record { cat = CSC {!!} ; ccc = cc1 {!!} } where 
           open ccc-from-graph g
       econg1 : (G : Graph {c₁} {c₁} {c₁}) → { a b : vertex G} → ( f  g : edge G a b ) → _≅_ G f g
          → _≅_ (FObj UX (csc G)) {atom a} {atom b} (λ x y → next f (x y)) (λ x y → next g (x y))
       econg1 G f g eq = {!!}