changeset 809:0976d576f5f6

<_,_> as function on Sets
author Shinji KONO Fri, 26 Apr 2019 21:24:12 +0900 e4cc2ccd0f06 084dc5e170f8 CCChom.agda discrete.agda 2 files changed, 24 insertions(+), 32 deletions(-) [+]
line wrap: on
line diff
```--- a/CCChom.agda	Fri Apr 26 19:50:27 2019 +0900
+++ b/CCChom.agda	Fri Apr 26 21:24:12 2019 +0900
@@ -590,7 +590,7 @@

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

open Graph

@@ -602,14 +602,12 @@

data Arrow {G : Graph } :  Objs {G} → Objs {G} → Set where
arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
-      id : (a : Objs ) → Arrow a a
○ : (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
-      <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
-      _・_ : {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 )
+   --   <_,_> : {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 )

record SM  : Set (suc Level.zero)  where
field
@@ -631,15 +629,11 @@
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 : 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 {a} {c} (arrow x) f) = λ z → smap G x ( k z ) where
k : fobj a → fobj {G} c
k z = fmap f z
-   fmap {G} {a} {b} (next (id b) f) = λ z → k z where
-       k : fobj a → fobj {G} b
-       k z = fmap f z
fmap {G} {a} {⊤} (next (○ b) f) = λ _ → OneObj'
fmap {G} {a} {b} (next {a} {x ∧ y} {b} π f) = λ z → proj₁ ( k z ) where
k : fobj a → fobj x /\ fobj y
@@ -650,29 +644,25 @@
fmap {G} {a} {b} (next {.a} {(x <= y) ∧ y} {.b} ε f) =  λ z → (  proj₁ (k z))(  proj₂ (k z)) where
k :  fobj a →  (fobj y → fobj x) /\ fobj y
k z = fmap f 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 : 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
+   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)
distrCS : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → Sets [ fmap ((DX G) [ g o f ]) ≈ Sets [ fmap g o fmap f ] ]
-       distrCS {a} {.a} {.a} {id a} {id .a} = {!!}
+       distrCS {a} {.a} {.a} {id a} {id .a} = refl
distrCS {a} {.a} {c} {id a} {next x g} = begin
fmap (DX G [ next x g o Chain.id a ])
≈⟨⟩
fmap ( next x ( g ++ (Chain.id a)))
≈⟨ extensionality Sets ( λ y → cong ( λ k → fmap ( next x k ) y ) (idR1 (DX G)) ) ⟩
fmap ( next x  g )
-          ≈↑⟨ {!!} ⟩
+          ≈↑⟨ refl ⟩
Sets [ fmap (next x g) o fmap (Chain.id a) ]
∎  where open ≈-Reasoning Sets
-       distrCS {a} {b} {b} {f} {id b} =  {!!}
+       distrCS {a} {b} {b} {f} {id b} =  refl
distrCS {a} {b} {atom z} {f} {next {.b} {atom y} {atom z} (arrow x) g} = {!!}
-       distrCS {a} {b} {c} {f} {next (id c) g} =  {!!}
distrCS {a} {b} {.⊤} {f} {next (○ a₁) g} = begin
fmap (DX G [ next (○ a₁) g o f ])
≈⟨ {!!} ⟩
@@ -681,11 +671,13 @@
distrCS {a} {b} {c} {f} {next {.b} {c ∧ x} {c} π 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 ・ y) g} = {!!}
-       distrCS {a} {b} {.(_ <= _)} {f} {next (x *) g} = {!!}
isf : IsFunctor (DX G) Sets fobj fmap
-       IsFunctor.identity isf = extensionality Sets ( λ x → {!!} )
+       IsFunctor.identity isf = extensionality Sets ( λ x → refl )
IsFunctor.≈-cong isf refl = refl
IsFunctor.distr isf {a} {b} {c} {g} {f} = distrCS {a} {b} {c} {g} {f}

+   <_,_> : { 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} {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} {a} {b} {c} f  = λ z y → FMap (CS G) ( next f (id (c ∧ b) ) ) ( z , y )```
```--- a/discrete.agda	Fri Apr 26 19:50:27 2019 +0900
+++ b/discrete.agda	Fri Apr 26 21:24:12 2019 +0900
@@ -19,15 +19,15 @@
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 )
+  _・_ : { 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 ;
Hom = λ a b →  Chain {G} a b ;
-            _o_ =  λ{a} {b} {c} x y → x ++ y ;
+            _o_ =  λ{a} {b} {c} x y → x ・ y ;
_≈_ =  λ x y → x  ≡ y ;
Id  =  λ{a} → id a ;
isCategory  = record {
@@ -42,16 +42,16 @@
obj = Graph.vertex G
hom = Graph.edge G

-               identityL : {A B : Graph.vertex G} {f : Chain A B} → (id B ++ f) ≡ f
+               identityL : {A B : Graph.vertex G} {f : Chain A B} → (id B ・ f) ≡ f
identityL = refl
-               identityR : {A B : Graph.vertex G} {f : Chain A B} → (f ++ id A) ≡ f
+               identityR : {A B : Graph.vertex G} {f : Chain A B} → (f ・ id A) ≡ f
identityR {a} {_} {id a} = refl
identityR {a} {b} {next x f} = cong ( λ k → next x k ) ( identityR {_} {_} {f} )
o-resp-≈  : {A B C : Graph.vertex G} {f g : Chain A B} {h i : Chain B C} →
-                            f ≡ g → h ≡ i → (h ++ f) ≡ (i ++ g)
+                            f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
o-resp-≈  refl refl = refl
associative : {a b c d : Graph.vertex G} (f : Chain c d) (g : Chain b c) (h : Chain a b) →
-                            (f ++ (g ++ h)) ≡ ((f ++ g) ++ h)
+                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
associative (id a) g h = refl
associative (next x f) g h = cong ( λ k → next x k ) ( associative f g h )
```