--- a/CCCGraph1.agda	Thu Apr 09 20:00:23 2020 +0900
+++ b/CCCGraph1.agda	Fri Apr 10 09:21:54 2020 +0900
@@ -38,13 +38,19 @@
    < 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 {
@@ -60,15 +66,73 @@
                     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 = 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 )
-               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 
+           } 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 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) 
+
+   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} → o-resp-≈-e {a} {b} {c} {f} {g} {h} {i}  ; 
+                    associative  = λ{a b c d f g h } →  cong (λ k → eval k ) (associative f g h )
+               }
+           }  where 
+              o-resp-≈-e  : {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)
+              o-resp-≈-e f=g h=i = {!!} 
+
+   fmap : {A B : Obj PL} → Hom PL A B → Hom PL A B
+   fmap (id a) = id _
+   fmap (○ a) = ○ a
+   fmap < f , g > = < fmap f , fmap g >
+   fmap (iv (arrow x) g) = iv (arrow x) (fmap g)
+   fmap (iv π (id _)) = {!!}
+   fmap (iv π < g , g₁ >) = fmap g
+   fmap (iv π (iv f g)) = {!!}
+   fmap (iv π' (id _)) = {!!}
+   fmap (iv π' < g , g₁ >) = fmap g₁
+   fmap (iv π' (iv f g)) = {!!}
+   fmap (iv ε (id _)) = {!!}
+   fmap (iv ε < f , g >) = {!!}
+   fmap (iv ε (iv f g)) = {!!}
+   fmap (iv (f *) g) = {!!}
+
+   PLCCC :  Functor PL PL
+   PLCCC = record {
+         FObj = λ x → x
+       ; FMap = {!!}
+       ; isFunctor = record {
+              identity = {!!}
+            ; distr = {!!}
+            ; ≈-cong = {!!}
+          }
+      }