# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1556322156 -32400
# Node ID 4ff300e1e98cdd95b32f0632122f387c88500f71
# Parent  2de0358ea10af9b03375026bac00c27f56e42e77
graph to CCC done

diff -r 2de0358ea10a -r 4ff300e1e98c CCChom.agda
--- a/CCChom.agda	Sat Apr 27 07:09:35 2019 +0900
+++ b/CCChom.agda	Sat Apr 27 08:42:36 2019 +0900
@@ -594,18 +594,18 @@
 
    open Graph
 
-   data Objs {G : Graph } : Set where
-      atom : (vertex G) → Objs
-      ⊤ : Objs
-      _∧_ : Objs {G} → Objs {G} → Objs
-      _<=_ : Objs {G} → Objs {G} → Objs
+   data Objs (G : Graph ) : Set where
+      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
-      arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
-      ○ : (a : Objs ) → Arrow a ⊤
-      π : {a b : Objs } → Arrow ( a ∧ b ) a
-      π' : {a b : Objs } → Arrow ( a ∧ b ) b
-      ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
+   data Arrow (G : Graph ) :  Objs G → Objs G → Set where
+      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 } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
    --   _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
 
@@ -619,25 +619,27 @@
 
    -- positive intutionistic calculus
    PL : (G : SM) → Graph
-   PL G = record { vertex = Objs {graph G} ; edge = Arrow {graph G}} 
+   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  : Obj (DX G) ) → Set
+   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'
-   fmap : {G : SM} { a b : Obj (DX G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
+   amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
+   amap {G} {.(atom _)} {.(atom _)} (arrow x) = smap G x
+   amap {G} {a} {.⊤} (○ a) _ = OneObj'
+   amap {G} {.(b ∧ _)} {b} π ( x , _) = x
+   amap {G} {.(_ ∧ b)} {b} π'( _ , x) = x
+   amap {G} {.((b <= _) ∧ _)} {b} ε ( f , x ) = f x
+   fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
    fmap {G} {a} {a} (id a) = λ z → z
-   fmap {G} {a} {(atom b)} (next {a} {c} (arrow x) f) = λ (z : fobj a) → smap G x ( fmap f z ) 
-   fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
-   fmap {G} {a} {b} (next {a} {.b ∧ y} {b} π f) = λ z → proj₁ ( fmap {G} {a} {b ∧ y} f z ) 
-   fmap {G} {a} {b} (next {.a} {x ∧ .b} {.b} π' f) =  λ z → proj₂ ( fmap f z ) where
-   fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) =  λ z → (  proj₁ (fmap f z))(  proj₂ (fmap f z)) 
+   fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ]
 
    CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
    FObj (CS G) a  = fobj a
@@ -646,12 +648,45 @@
        _++_ = 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} {.c ∧ x} {.c} π g} z =  begin
+             fmap (DX G [ next π g o f ]) z
+          ≡⟨⟩
+             fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z
+          ≡⟨⟩
+             proj₁ ( fmap {G} {a} {c ∧ x} (g ++ f ) z ) 
+          ≡⟨ cong ( λ k → proj₁ k ) ( distr {a} {b} {(c ∧ x)} {f} {g} z )  ⟩
+             proj₁ ( fmap g ( fmap f z ))
+          ≡⟨⟩
+             (Sets [ fmap (next π g) o fmap f ]) z
+          ∎  where open ≡-Reasoning 
+       distr {a} {b} {c} {f} {next {b} {x ∧ c} π' g} z =   begin
+             fmap (DX G [ next π' g o f ]) z
+          ≡⟨⟩
+             fmap (next π' (g ++ f)) z
+          ≡⟨⟩
+             proj₂ (fmap (g ++ f) z)
+          ≡⟨ cong ( λ k → proj₂ k ) ( distr {a} {b} {x ∧ c} {f} {g}  z )  ⟩
+             ( Sets [ fmap (next π' g) o fmap f ] ) z
+          ∎  where open ≡-Reasoning 
+       distr {a} {b} {c} {f} {next {b} {(c <= x) ∧ x} {c} ε g} z =  begin
+             fmap (DX G [ next ε g o f ] ) z
+          ≡⟨⟩
+              fmap (next ε (g ++ f)) z
+          ≡⟨⟩
+             proj₁ (fmap (g ++ f)  z) (  proj₂ (fmap (g ++ f) z) ) 
+          ≡⟨  cong ( λ k → proj₁ k (  proj₂ k)) (distr {a} {b} {(c <= x) ∧ x} {f} {g} z)   ⟩
+             proj₁ (fmap g (fmap f z)) ( proj₂ (fmap g (fmap f z)))
+          ≡⟨⟩
+             fmap (next ε g) (fmap f z) 
+          ≡⟨⟩
+             ( Sets [ fmap (next ε g) o fmap f ] ) z
+          ∎  where open ≡-Reasoning 
        distr {a} {.a} {.a} {id a} {id .a} z =  refl
-       distr {a} {.a} {c} {id a} {next x g} z = begin
+       distr {a} {.a} {c} {id a} {next {a} {b} x g} z = begin
              fmap (DX G [ next x g o Chain.id a ]) z
           ≡⟨⟩
              fmap ( next x ( g ++ (Chain.id a))) z
-          ≡⟨ cong ( λ k → fmap ( next x k ) z ) ++idR  ⟩
+          ≡⟨ cong ( λ k → fmap ( next x k ) z ) ( ++idR {a} {b} {g} ) ⟩
              fmap ( next x  g ) z
           ≡⟨ refl ⟩
              ( Sets [ fmap (next x g) o fmap (Chain.id a) ] ) z
@@ -675,46 +710,13 @@
           ≡⟨⟩
              (Sets [ fmap (next (○ a₁) g) o fmap f ]) z
           ∎  where open ≡-Reasoning 
-       distr {a} {b} {c} {f} {next {.b} {.c ∧ x} {.c} π g} z =  begin
-             fmap (DX G [ next π g o f ]) z
-          ≡⟨⟩
-             fmap {G} {a} {c} (next {PL G} {a} {c ∧ x} {c} π ( g ++ f)) z
-          ≡⟨ {!!} ⟩
-             proj₁ ( fmap {G} {a} {c ∧ x} (g ++ f ) z ) 
-          ≡⟨ cong ( λ k → proj₁ k ) ( distr {a} {b} {(c ∧ x)} {f} {g} z )  ⟩
-             proj₁ ( fmap g ( fmap f z ))
-          ≡⟨ {!!} ⟩
-             (Sets [ fmap (next π g) o fmap f ]) z
-          ∎  where open ≡-Reasoning 
-       distr {a} {b} {c} {f} {next π' g} z =   begin
-             fmap (DX G [ next π' g o f ]) z
-          ≡⟨⟩
-             fmap (next π' (g ++ f)) z
-          ≡⟨ {!!} ⟩
-             proj₂ (fmap (g ++ f) z)
-          ≡⟨ {!!} ⟩
-             ( Sets [ fmap (next π' g) o fmap f ] ) z
-          ∎  where open ≡-Reasoning 
-       distr {a} {b} {c} {f} {next {b} {(c <= x) ∧ x} {c} ε g} z =  begin
-             fmap (DX G [ next ε g o f ] ) z
-          ≡⟨⟩
-              fmap (next ε (g ++ f)) z
-          ≡⟨ {!!} ⟩
-             proj₁ (fmap (g ++ f)  z) (  proj₂ (fmap (g ++ f) z) ) 
-          ≡⟨  cong ( λ k → proj₁ k (  proj₂ k)) (distr {a} {b} {(c <= x) ∧ x} {f} {g} z)   ⟩
-             proj₁ (fmap g (fmap f z)) ( proj₂ (fmap g (fmap f z)))
-          ≡⟨ {!!} ⟩
-             fmap (next ε g) (fmap f z) 
-          ≡⟨⟩
-             ( Sets [ fmap (next ε g) o fmap f ] ) z
-          ∎  where open ≡-Reasoning 
        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 ) 
 
-   <_,_> : { G : SM } → {a b c : Objs {graph G}} → Arrow c a → Arrow c b → Hom Sets (FObj (CS G) c ) (FObj (CS G) (a ∧ b) )
+   <_,_> : { G : SM } → {a b c : Objs (graph G)} → Arrow (graph G) c a → Arrow (graph G) c b → Hom Sets (FObj (CS G) c ) (FObj (CS G) (a ∧ b) )
    <_,_> {G} {a} {b} {c}   f  g  = λ z → ( (FMap (CS G) ( next f (id c)))  z , FMap (CS G) (next g (id c)) z )
 
-   _* : { G : SM } → {a b c : Objs {graph G}} → Arrow (c ∧ b ) a →  Hom Sets (FObj (CS G) c)  (FObj (CS G) ( a <= b ))
+   _* : { G : SM } → {a b c : Objs (graph G)} → Arrow (graph G) (c ∧ b ) a →  Hom Sets (FObj (CS G) c)  (FObj (CS G) ( a <= b ))
    _* {G} {a} {b} {c} f  = λ z y → FMap (CS G) ( next f (id (c ∧ b) ) ) ( z , y )
diff -r 2de0358ea10a -r 4ff300e1e98c discrete.agda
--- a/discrete.agda	Sat Apr 27 07:09:35 2019 +0900
+++ b/discrete.agda	Sat Apr 27 08:42:36 2019 +0900
@@ -22,7 +22,6 @@
   _・_ : { G : Graph} {a b c : Graph.vertex G } (f : Chain {G} b c ) → (g : Chain {G} a b) → Chain {G} a c
   id _ ・ f = f
   (next x f) ・ g = next x ( f ・ g )
-  -- _・_ {G} {a} {b} {c} (next {b} {d} {c} x f)  g = next {G} {a} {d} {c} x ( f ・ g )
 
   GraphtoCat : (G : Graph )  →  Category  Level.zero Level.zero Level.zero   
   GraphtoCat G = record {