# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586770798 -32400
# Node ID 4d64a90410c67d3c2fe2463ca276697e2c633d77
# Parent  2e52bb0a409729a43fd0113770dbef405245b705
clean up

diff -r 2e52bb0a4097 -r 4d64a90410c6 CCCGraph.agda
--- a/CCCGraph.agda	Mon Apr 13 18:01:05 2020 +0900
+++ b/CCCGraph.agda	Mon Apr 13 18:39:58 2020 +0900
@@ -96,6 +96,12 @@
                     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 ( [_] )
@@ -162,6 +168,11 @@
                                     f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
               o-resp-≈ refl refl = refl 
 
+--------
+--
+-- 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₂
 
@@ -190,9 +201,9 @@
    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
+--   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
 
    CS :  Functor PL (Sets {c₁ ⊔ c₂})
    FObj CS a  = fobj  a
@@ -217,7 +228,7 @@
 
    CSC = FCat PL (Sets {c₁ ⊔ c₂}) CS
 
-   cc1 : CCC CSC
+   cc1 : CCC CSC       -- SCS is CCC
    cc1 = record {
          １ = ⊤ ;
          ○ =  λ a x → OneObj ;
@@ -229,17 +240,25 @@
          _* = λ f x y → f ( x , y ) ;
          ε = λ x → ( proj₁ x) (proj₂ x) ;
          isCCC = record {
-               e2  =  extensionality Sets ( λ x → {!!} ) ;
+               e2  = λ {a} {f} → extensionality Sets ( λ x → e20 {a} {f} x ) ;
                e3a = refl ;
                e3b = refl ;
                e3c = refl ;
-               π-cong = {!!} ;
+               π-cong = π-cong ;
                e4a = refl ;
                e4b = refl ;
-               *-cong = {!!} 
+               *-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
 
 ------------------------------------------------------
 --  Cart     Category of CCC and CCC preserving Functor
@@ -394,17 +413,9 @@
       lemma refl (refl eqv) = mrefl ( ≈-to-≡ (cat b) eqv )
 
 
----   
----   open ccc-from-graph
----   
----   sm : {v : Level } → Graph {v} → SM {v}
----   SM.graph (sm g) = g
----   SM.sobj (sm  g) = {!!}
----   SM.smap (sm  g) = {!!}
----   
----   HX : {v : Level } ( x : Obj (Grph {v}) ) → Obj (Grph {v})
----   HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ;  ccc = sets } )
----   
----   
----   
----   
+
+open ccc-from-graph
+
+--- HX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) →  {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g  )
+---     → Functor (Grph {c₁} {c₂}) (Cart {c₁} {c₂} {ℓ} ) 
+--- HX = {!!}