--- a/CCCGraph.agda	Sat May 02 03:40:56 2020 +0900
+++ b/CCCGraph.agda	Sat May 02 04:21:05 2020 +0900
@@ -216,6 +216,42 @@
         IsFunctor.≈-cong isf refl = refl 
         IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
+   open import subcat
+
+   CSC = FCat PL (Sets {c₁ ⊔ c₂ }) CS 
+
+   cc1 : CCC CSC       -- SCS is CCC
+   cc1 = 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 } {f : Hom CSC 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 } {f f' : Hom CSC (a ∧ b) c} →
+                    Sets [ f ≈ f' ] → Sets [  (λ x y → f (x , y)) ≈ (λ x y → f' (x , y)) ]
+        *-cong refl = refl
+
 
 
 ---
@@ -368,13 +404,21 @@
 ccc-graph-univ {c₁}   = record {
      F = λ g → csc g ;
      η = λ a → record { vmap = λ y → atom y ; emap = λ f x y →  next f (x y) } ;
-     _* = {!!} ;
+     _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
          uniquness = {!!}
       }
   } where
        csc : Graph → Obj Cart
-       csc g = record { cat = {!!} ; ccc = {!!} } where 
+       csc g = record { cat = CSC  ; ccc = cc1 ; ≡←≈ = λ eq → eq } where 
            open ccc-from-graph g
+       cobj  : {g : Obj Grph} {c : Obj (Cart {c₁} {c₁} {c₁})} → Hom Grph g (FObj UX c)  → Obj (cat (csc g)) → Obj (cat c)
+       cobj {g} {c} f (atom x) = {!!}
+       cobj {g} {c} f ⊤ = CCC.１ (ccc c)
+       cobj {g} {c} f (x ∧ y) = CCC._∧_ (ccc c) {!!} {!!}
+       cobj {g} {c} f (b <= a) = CCC._<=_ (ccc c) {!!} {!!}
+       solution : {g : Obj Grph} {c : Obj Cart} → Hom Grph g (FObj UX c) → Hom Cart (csc g) c
+       solution {g} {c} f = record { cmap = record { FObj = λ x → cobj {g} {c} f x ; FMap = {!!} ; isFunctor = {!!} } ; ccf = {!!} }
 
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/subcat.agda	Sat May 02 04:21:05 2020 +0900
@@ -0,0 +1,23 @@
+open import Category
+open import Level
+module subcat {c₁ c₂ ℓ c₁' c₂' ℓ' : Level} (A : Category c₁' c₂' ℓ') (B : Category c₁ c₂ ℓ) (F : Functor A B) where
+
+    open import cat-utility
+    open import Relation.Binary.PropositionalEquality
+    open Functor
+
+    FCat : Category c₁' c₂ ℓ
+    FCat = record {
+          Obj = Obj A
+          ; Hom = λ a b → Hom B (FObj F a) (FObj F b)
+          ; _o_ = Category._o_ B
+          ; _≈_ = Category._≈_ B
+          ; Id  = λ {a} → id1 B (FObj F a)
+          ; isCategory = record {
+                    isEquivalence =  IsCategory.isEquivalence (Category.isCategory B) ;
+                    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) 
+             }
+      }