### changeset 806:dd0d0a201990

...
author Shinji KONO Fri, 26 Apr 2019 16:54:18 +0900 979c0bf97a5a 91a2efb67462 CCChom.agda discrete.agda 2 files changed, 32 insertions(+), 32 deletions(-) [+]
line wrap: on
line diff
```--- a/CCChom.agda	Thu Apr 25 17:56:30 2019 +0900
+++ b/CCChom.agda	Fri Apr 26 16:54:18 2019 +0900
@@ -590,7 +590,7 @@

open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
open import discrete
-   open graphtocat
+   open graphtocat hiding ( _++_ )

open Graph

@@ -611,33 +611,40 @@
_・_ : {a b c : Objs } → Arrow b c → Arrow a b → Arrow a c
_* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )

+   record SM  : Set (suc Level.zero)  where
+      field
+        graph : Graph
+        sobj : vertex graph → Set
+        smap : { a b : vertex graph } → edge graph a b  → sobj a → sobj b
+
+   open SM

-- positive intutionistic calculus
-   DX : (G : Graph) → Category  Level.zero Level.zero Level.zero
-   DX G = GraphtoCat ( record { vertex = Objs {G} ; edge = Arrow {G}} )
+   DX : (G : SM) → Category  Level.zero Level.zero Level.zero
+   DX G = GraphtoCat ( record { vertex = Objs {graph G} ; edge = Arrow {graph G}} )

-- open import Category.Sets
-- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂

-   fobj : {G : Graph} ( a  : Obj (DX G) ) → Set
-   fobj {G} (atom x) = vertex G
-   fobj (a ∧ b) = (fobj a ) /\ (fobj b )
-   fobj (a <= b) = fobj b → fobj a
+   fobj : {G : SM} ( a  : Obj (DX 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'
{-# TERMINATING #-}
-   fmap : {G : Graph} { a b : Obj (DX G) } → Hom (DX G) a b → fobj a → fobj b
-   fmap {G} {a} {a} (id a) = id1 Sets (fobj a) where open ≈-Reasoning (Sets {Level.zero})
-   fmap {G} {a} {(atom b)} (next (arrow x) f) = λ _ → b
+   fmap : {G : SM} { a b : Obj (DX 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 (arrow x) f) = λ z → smap G x ( fmap f z )
fmap {G} {a} {b} (next (id b) f) = fmap f
fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
-   fmap {G} {a} {b} (next π f) = λ z → proj₁ ( fmap f z )
+   fmap {G} {a} {b} (next {a} {.b ∧ y} {b} π f) = λ z → proj₁ ( fmap f z )
fmap {G} {a} {b} (next π' f) =  λ z → proj₂ ( fmap f z )
fmap {G} {a} {b} (next ε f) =  λ z → (  proj₁ (fmap f z) )(  proj₂ (fmap f z) )
-   fmap {G} {a} {b} (next (f ・ g) h) = λ z →  fmap ( next f (next g h ) ) z
+   fmap {G} {a} {b} (next (f ・ g) h) =  λ z →  fmap (next f (next g h)) z
fmap {G} {a} {(_ ∧ _)} (next < f , g > h) = λ z → ( fmap (next f h) z ,  fmap (next g h) z)
fmap {G} {a} {(c <= b)} (next {_} {d} (f *) g ) = λ x y → fmap (next f (id (d ∧ b))) ( fmap g x , y )

-   CS : {G : Graph } → Functor (DX G) (Sets {Level.zero})
+   CS : {G : SM } → Functor (DX G) (Sets {Level.zero})
FObj CS a  = fobj a
FMap (CS {G}) {a} {b} f = fmap {G} {a} {b} f
isFunctor (CS {G}) = isf where
@@ -654,27 +661,19 @@
Sets [ fmap (next x g) o fmap (Chain.id a) ]
∎  where open ≈-Reasoning Sets
distrCS {a} {b} {b} {f} {id b} = refl
-       distrCS {a} {b} {.(atom _)} {f} {next (arrow x) g} = refl
-       distrCS {a} {b} {c} {f} {next (id c) g} = begin
-             fmap (DX G [ next (Arrow.id c) g o f ])
-          ≈⟨ {!!} ⟩
-             Sets [ fmap (next (Arrow.id c) g) o fmap f ]
-          ∎  where open ≈-Reasoning Sets
+       distrCS {a} {b} {atom z} {f} {next (arrow x) g} = distrCS
+       distrCS {a} {b} {c} {f} {next (id c) g} = distrCS
distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
fmap (DX G [ next (○ a₁) g o f ])
≈⟨ extensionality Sets ( λ x → refl ) ⟩
Sets [ fmap (next (○ a₁) g) o fmap f ]
∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {c} {f} {next π g} = {!!}
-       distrCS {a} {b} {c} {f} {next π' g} = {!!}
-       distrCS {a} {b} {c} {f} {next ε g} = {!!}
-       distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = {!!}
-       distrCS {a} {b} {c} {f} {next (x ・ x₁) g} = extensionality Sets ( λ z → begin
-             fmap (DX G [ next (x ・ x₁) g o f ]) z
-          ≡⟨ {!!} ⟩
-             ( Sets [ fmap (next (x ・ x₁) g) o fmap f ]  ) z
-          ∎ ) where open ≡-Reasoning
-       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = {!!}
+       distrCS {a} {b} {c} {f} {next {.b} {c ∧ x} {c} π g} = distrCS
+       distrCS {a} {b} {c} {f} {next π' g} = distrCS
+       distrCS {a} {b} {c} {f} {next ε g} = distrCS
+       distrCS {a} {b} {.(_ ∧ _)} {f} {next < x , x₁ > g} = distrCS
+       distrCS {a} {b} {c} {f} {next (x ・ y) g} = distrCS
+       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = distrCS
isf : IsFunctor (DX G) Sets fobj fmap
IsFunctor.identity isf = extensionality Sets ( λ x → refl )
IsFunctor.≈-cong isf refl = refl```
```--- a/discrete.agda	Thu Apr 25 17:56:30 2019 +0900
+++ b/discrete.agda	Fri Apr 26 16:54:18 2019 +0900
@@ -19,6 +19,10 @@
id : ( a : Graph.vertex g ) → Chain a a
next : { a b c : Graph.vertex g } → (Graph.edge g b c ) → Chain {g} a b → Chain  a c

+  _++_ : { 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 )
+
GraphtoCat : (G : Graph )  →  Category  Level.zero Level.zero Level.zero
GraphtoCat G = record {
Obj  = Graph.vertex G ;
@@ -37,9 +41,6 @@
open Chain
obj = Graph.vertex G
hom = Graph.edge G
-               _++_ : {a b c : obj } (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 )

identityL : {A B : Graph.vertex G} {f : Chain A B} → (id B ++ f) ≡ f
identityL = refl```