--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/CCCGraph.agda	Sun Apr 28 12:37:34 2019 +0900
@@ -0,0 +1,237 @@
+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
+
+module ccc-from-graph where
+
+   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
+   open import discrete
+   open graphtocat 
+
+   open Graph
+
+   data Objs (G : Graph ) : Set where    -- formula
+      atom : (vertex G) → Objs G
+      ⊤ : Objs G
+      _∧_ : Objs G → Objs G → Objs G
+      _<=_ : Objs G → Objs G → Objs G
+
+   data Arrow (G : Graph ) :  Objs G → Objs G → Set where  --- proof
+      arrow : {a b : vertex G} →  (edge G) a b → Arrow G (atom a) (atom b)
+      ○ : (a : Objs G ) → Arrow G a ⊤
+      π : {a b : Objs G } → Arrow G ( a ∧ b ) a
+      π' : {a b : Objs G } → Arrow G ( a ∧ b ) b
+      ε : {a b : Objs G } → Arrow G ((a <= b) ∧ b ) a
+      <_,_> : {a b c : Objs G } → Arrow G c a → Arrow G c b → Arrow G c (a ∧ b)
+      _* : {a b c : Objs G } → Arrow G (c ∧ b ) a → Arrow G c ( a <= b )
+
+   record SM {v : Level} : Set (suc v)  where
+      field
+        graph : Graph  {v}
+        sobj : vertex graph → Set
+        smap : { a b : vertex graph } → edge graph a b  → sobj a → sobj b
+
+   open SM
+
+   -- positive intutionistic calculus
+   PL : (G : SM) → Graph
+   PL G = record { vertex = Objs (graph G) ; edge = Arrow (graph G) }
+   DX : (G : SM) → Category  Level.zero Level.zero Level.zero   
+   DX G = GraphtoCat (PL G)
+
+   -- open import Category.Sets
+   -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
+
+   fobj : {G : SM} ( a  : Objs (graph G) ) → Set
+   fobj {G} (atom x) = sobj G x
+   fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
+   fobj {G} (a <= b) = fobj {G} b → fobj {G} a
+   fobj ⊤ = One
+   amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
+   amap {G} (arrow x) = smap G x
+   amap (○ a) _ = OneObj
+   amap π ( x , _) = x
+   amap π'( _ , x) = x
+   amap ε ( f , x ) = f x
+   amap < f , g > x = (amap f x , amap g x)
+   amap (f *) x = λ y → amap f ( x , y )
+   fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
+   fmap {G} {a} (id a) = λ z → z
+   fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]
+
+   --   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 : (G : SM ) → Functor (DX G) (Sets {Level.zero})
+   FObj (CS G) a  = fobj a
+   FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
+   isFunctor (CS G) = isf where
+       _++_ = Category._o_ (DX G)
+       ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
+       distr : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
+       distr {a} {b} {c} {f} {next {b} {d} {c} 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 (graph G) d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next x g ) (fmap f z )
+          adistr eq x = cong ( λ k → amap x k ) eq
+       distr {a} {b} {b} {f} {id b} z =  refl
+       isf : IsFunctor (DX G) Sets fobj fmap 
+       IsFunctor.identity isf = extensionality Sets ( λ x → refl )
+       IsFunctor.≈-cong isf refl = refl
+       IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
+
+---   record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+---     field
+---       cat : Category c₁ c₂ ℓ
+---       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 : {A B : CCCObj {c₁} {c₂} {ℓ} } → CCC (cat A) → CCC (cat B)
+---   
+---   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_ = {!!}
+---     ; _≈_ = {!!}
+---     ; Id  = {!!}
+---     ; isCategory = record {
+---          identityL = {!!}
+---        ; identityR = {!!}
+---        ; o-resp-≈ = {!!}
+---        ; associative = {!!}
+---      }}
+---   
+---   open import discrete
+---   open Graph
+---   
+---   record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where
+---      vmap : vertex x → vertex y
+---      emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
+---   
+---   Grp : {v : Level} → Category (suc v) v v
+---   Grp {v} = record {
+---       Obj = Graph {v} 
+---     ; Hom = {!!}
+---     ; _o_ = {!!}
+---     ; _≈_ = {!!}
+---     ; Id  = {!!}
+---     ; isCategory = record {
+---          identityL = {!!}
+---        ; identityR = {!!}
+---        ; o-resp-≈ = {!!}
+---        ; associative = {!!}
+---      }}
+---   
+---   UX : {c₁ c₂ ℓ : Level} → Functor (Cart {c₁} {c₂} {ℓ} ) (Grp {c₁})
+---   UX = {!!}
+---   
+---   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 (Grp {v}) ) → Obj (Grp {v})
+---   HX {v} x = {!!} -- FObj UX ( record { cat = Sets {v} ;  ccc = sets } )
+---   
+---   
+---   
+---