# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1589811194 -32400
# Node ID 095fd0829ccfce1d1e19fd7e0af209de2adb346b
# Parent  f8e6e9128f3d33523ad2379f3cf6efbd7bfc409b
use postulate on Hom of FCat

diff -r f8e6e9128f3d -r 095fd0829ccf CCCGraph.agda
--- a/CCCGraph.agda	Mon May 18 18:41:55 2020 +0900
+++ b/CCCGraph.agda	Mon May 18 23:13:14 2020 +0900
@@ -428,25 +428,6 @@
 
   open ccc-from-graph g
 
-  FCat' : Obj (Cart {suc c₁} {suc c₁ ⊔ c₂} {c₁ ⊔ c₂})
-  FCat'  = record { cat = record {
-          Obj = Obj PL 
-          ; Hom = λ a b → {f : Hom PL a b } → Hom B (FObj CS a) (FObj CS b)
-          ; _o_ = {!!}
-          ; _≈_ = {!!}
-          ; Id  = λ {a} → id1 B (FObj CS a)
-          ; isCategory = record {
-                    isEquivalence =  {!!};
-                    identityL  = λ {a b f} → {!!};
-                    identityR  = λ {a b f} → {!!};
-                    o-resp-≈  = λ {a b c f g h i} → {!!};
-                    associative  = λ{a b c d f g h } → {!!} } 
-          } ; 
-         ≡←≈  = λ eq → {!!} ;
-         ccc = {!!}
-      } where
-          B = Sets {c₁ ⊔ c₂}
-
   FCat : Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
   FCat  = record { cat = record {
           Obj = Obj PL 
@@ -459,7 +440,7 @@
                     identityL  = λ {a b f} → IsCategory.identityL (Category.isCategory B) ;
                     identityR  = λ {a b f} → IsCategory.identityR (Category.isCategory B) ;
                     o-resp-≈  = λ {a b c f g h i} → IsCategory.o-resp-≈ (Category.isCategory B);
-                    associative  = λ{a b c d f g h } → IsCategory.associative (Category.isCategory B) 
+                    associative  = λ {a b c d f g h } → IsCategory.associative (Category.isCategory B) 
              }
           } ;
          ≡←≈  = λ eq → eq ;
@@ -467,6 +448,11 @@
       } where
           B = Sets {c₁ ⊔ c₂}
 
+  -- Hom FCat is an image of Fucntor CS, but I don't know how to write it
+  postulate
+      fcat-pl : {a b : Obj (cat FCat) } → Hom (cat FCat) a b → Hom PL a b
+      fcat-eq :  {a b : Obj (cat FCat) } → (f : Hom (cat FCat) a b ) → FMap CS (fcat-pl f) ≡ f
+
 
 ccc-graph-univ :  {c₁ c₂ : Level} → UniversalMapping (Grph {c₁} {c₂}) (Cart {suc c₁ } {c₁ ⊔ c₂} {c₁ ⊔ c₂}) forgetful.UX 
 ccc-graph-univ {c₁} {c₂} = record {
@@ -493,7 +479,7 @@
        --  Sets  ((z : vertx g) → C z x)  ----> ((z : vertx g) → C z y)  = h : Hom Sets (fobj (atom x)) (fobj (atom y))
        --
        F : Obj (Grph {c₁} {c₂}) → Obj (Cart {suc c₁} {c₁ ⊔ c₂} {c₁ ⊔ c₂})
-       F g = FCat'  where open fcat g 
+       F g = FCat  where open fcat g 
        η : (a : Obj (Grph {c₁} {c₂}) ) → Hom Grph a (FObj UX (F a))
        η a = record { vmap = λ y → vm y ;  emap = λ f → em f }  where
             fo : Graph  {suc c₁ } {c₁ ⊔ c₂}
@@ -511,7 +497,13 @@
        cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) (cobj {g} {c} f b) (cobj {g} {c} f a) 
        c-map :  {g : Obj (Grph  )} {c : Obj Cart} {A B : Objs g} 
            → (f : Hom Grph g (FObj UX c) ) → (fobj g A → fobj g B) → Hom (cat c) (cobj {g} {c} f A) (cobj {g} {c} f B)
-       c-map {g} {c} {a} {atom b} f y = {!!} 
+       c-map {g} {c} {a} {atom b} f y with fcat.fcat-pl {c₁} {c₂} g {a} {atom b} y
+       c-map {g} {c} {atom b} {atom b} f y | id (atom b) = id1 (cat c) _
+       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} (arrow x) t =
+          (cat c) [ emap (m12 (uobj {c₁} {c₂} c)) ( emap f x)  o c-map {g} {c} {a} {d} f (fmap g t) ]
+       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} π t = (cat c) [ CCC.π (ccc c) o c-map {g} {c} {a} {d} f (fmap g t)]
+       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} π' t = (cat c) [ CCC.π' (ccc c) o c-map {g} {c} {a} {d} f (fmap g t) ]
+       c-map {g} {c} {a} {atom b} f y | iv {_} {_} {d} ε t = (cat c) [ CCC.ε (ccc c) o c-map {g} {c} {a} {d} f (fmap g t) ]
        -- with emap (m12 (uobj {c₁} {c₂} c)) ( emap f {!!} )
        c-map {g} {c} {a} {⊤} f x = CCC.○ (ccc c) (cobj f a)
        c-map {g} {c} {a} {x ∧ y} f z = CCC.<_,_> (ccc c) (c-map f (λ k → proj₁ (z k))) (c-map f (λ k → proj₂ (z k)))