Mercurial > hg > Members > kono > Proof > category

changeset 809:0976d576f5f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
<_,_> as function on Sets
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Apr 2019 21:24:12 +0900
parents e4cc2ccd0f06
children 084dc5e170f8
files CCChom.agda discrete.agda
diffstat 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 )