Mercurial > hg > Members > kono > Proof > category

changeset 875:ad42e7661215

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 09 Apr 2020 19:38:05 +0900
parents 484f19f16712
children
files CCCGraph.agda
diffstat 1 files changed, 42 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Thu Apr 09 18:12:33 2020 +0900
+++ b/CCCGraph.agda	Thu Apr 09 19:38:05 2020 +0900
@@ -179,16 +179,24 @@
        IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
    data Sequence {G : Graph} : (a b : Objs G) → Set where
+      s○ : (a : Objs G) → Sequence a ⊤
       sid : (a : Objs G) → Sequence a a
       sprod : {a b c d : Objs G} → Sequence a b → Sequence c d → Sequence (a ∧ c) (b ∧ d)
-      snext : {a b c : vertex G} → edge G b c → Sequence {G} (atom a) (atom b) → Sequence (atom a) (atom c)
+      snext : {a b c : Objs G} → Arrow G b c → Sequence {G} a b → Sequence a c
 
    _+_ : {G : Graph} → {a b c : Objs G} → Sequence b c → Sequence a b → Sequence a c
    sid a + g = g
+   s○ a + g = s○ _
    sprod f g + sid _ = sprod f g
    sprod f g + sprod h h₁ = sprod ( f + h ) ( g + h₁ )
    snext f g + sid _ = snext f g
    snext f g + snext x h = snext f ( g + snext x h )
+   sprod x x₁ + snext π g = {!!}
+   sprod x x₁ + snext π' g = {!!}
+   sprod x x₁ + snext ε g = {!!}
+   sprod x x₁ + snext < f , f₁ > g = {!!}
+   snext x x₁ + s○ a = snext x ( x₁ + (s○ a ))
+   snext x x₁ + sprod x₂ x₃ = snext x (x₁ + sprod x₂ x₃ )
 
    SC :  Graph → Category  Level.zero Level.zero Level.zero
    SC G = record {
@@ -208,11 +216,13 @@
                identityL : {A B : Objs G} {f : Sequence A B} → (sid B + f) ≡ f
                identityL {a} {b} {f} = refl
                identityR : {A B : Objs G} {f : Sequence A B} → (f + sid A) ≡ f
+               identityR {a} {⊤} {s○ a} = refl
                identityR {a} {a} {sid a} = refl
                identityR {_} {_} {sprod f f₁} = refl
                identityR {_} {_} {snext x f} = refl
                associative : {a b c d : Objs G} (f : Sequence c d) (g : Sequence b c) (h : Sequence a b) →
                             (f + (g + h)) ≡ ((f + g) + h)
+               associative (s○ a) g h = refl
                associative (sid a) g h = refl
                associative (sprod f f₁) (sid _) h = refl
                associative (sprod f f₁) (sprod g g₁) (sid _) = refl
@@ -220,28 +230,52 @@
                associative (snext x f) (sid _) h = refl
                associative (snext x f) (snext y g) (sid _) = refl
                associative (snext x f) (snext y g) (snext z h) = cong ( λ k → snext x k ) (associative f (snext y g) (snext z h))
+               associative (sprod f f₁) (sprod g g₁) (snext x h) = {!!}
+               associative (sprod f f₁) (snext x g) h = {!!}
+               associative (snext x f) (s○ a) h = {!!}
+               associative (snext x f) (sprod g g₁) h = {!!}
+               associative (snext x f) (snext x₁ g) (s○ a) = {!!}
+               associative (snext x f) (snext x₁ g) (sprod h h₁) = {!!}
                o-resp-≈  : {A B C : Objs G} {f g : Sequence A B} {h i : Sequence B C} →
                             f ≡ g → h ≡ i → (h + f) ≡ (i + g)
                o-resp-≈  refl refl  = refl
 
    DD : (G : Graph) → Category  Level.zero Level.zero Level.zero
    DD G = GraphtoCat (record { vertex = Objs G ; edge = Arrow G })
+
+   samap : {G : Graph } → { a b : Objs G } → Arrow G a b → Hom (SC G) a b
+   samap (arrow x) = snext {!!} (sid _)
+   samap (○ a) = s○ _
+   samap π = {!!}
+   samap π' = {!!}
+   samap ε = {!!}
+   samap < f , f₁ > = {!!}
+   samap (f *) = {!!}
+
    scmap : {G : Graph} { a b : Objs G } → Hom (DD G) a b → Hom (SC G) a b
-   scmap = ?
+   scmap (id a) = sid a
+   scmap (next (arrow x) f) = snext {!!} (sid _) + scmap f
+   scmap (next (○ a) f) = s○ _
+   scmap (next π (id _)) = {!!}
+   scmap (next π (next x f)) = {!!}
+   scmap (next π' f) = {!!}
+   scmap (next ε f) = {!!}
+   scmap (next < x , x₁ > f) = {!!}
+   scmap (next (x *) f) = {!!}
 
    GtoSC : (G : Graph ) → Functor (DD G) (SC G)
    FObj (GtoSC G) a  = a
-   FMap (GtoSC G) {a} {b} f = ?
+   FMap (GtoSC G) {a} {b} f = {!!}
    isFunctor (GtoSC G) = isf where
        _++_ = Category._o_ (DD G)
        ++idR = IsCategory.identityR ( Category.isCategory ( DD G ) )
        distr : {a b c d : Obj (DD G)}  { f : Hom (DD G) b c } { g : Hom (DD G) c d } → (z : Hom (SC G) a b ) → scmap (g ++ f) + z ≡ scmap g + (scmap f + z)
-       distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = ?
-       distr {a} {b} {b} {f} {id b} z =  ?
-       isf : IsFunctor (DD G) (SC G) ? scmap 
-       IsFunctor.identity isf = ?
+       distr {a} {b} {c} {f} {next {b} {d} {c} x g} z = {!!}
+       distr {a} {b} {b} {f} {id b} z =  {!!}
+       isf : IsFunctor (DD G) (SC G) {!!} scmap 
+       IsFunctor.identity isf = {!!}
        IsFunctor.≈-cong isf refl = refl
-       IsFunctor.distr isf {a} {b} {c} {g} {f} = ?
+       IsFunctor.distr isf {a} {b} {c} {g} {f} = {!!}