### changeset 812:4ff300e1e98c

graph to CCC done
author Shinji KONO Sat, 27 Apr 2019 08:42:36 +0900 2de0358ea10a 9b8ee2ddd92d CCChom.agda discrete.agda 2 files changed, 58 insertions(+), 57 deletions(-) [+]
line wrap: on
line diff
```--- 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 )```
```--- 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 {```