Mercurial > hg > Members > kono > Proof > category

changeset 800:bca72fffdc1a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph to ccc dead end
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 23 Apr 2019 16:34:38 +0900
parents 82a8c1ab4ef5
children aa4fbd007247
files CCChom.agda
diffstat 1 files changed, 150 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Tue Apr 23 11:30:34 2019 +0900
+++ b/CCChom.agda	Tue Apr 23 16:34:38 2019 +0900
@@ -607,15 +607,75 @@
       ε : {a b : Objs } → arrow ((a <= b) ∧ b ) a
       _* : {a b c : Objs } → arrow (c ∧ b ) a → arrow c ( a <= b )
 
-   open import discrete
+   data Arrow { obj : Set } { hom : obj → obj → Set } : ( a b : obj ) → Set where
+     id : ( a : obj ) → Arrow a a
+     mono : { a b : obj } → hom a b → Arrow a b
+     connected : {a b : obj } → {c : obj} → hom b c →  Arrow {obj} {hom} a b → Arrow a c
+ 
+   _+_ : { obj : Set } { hom : obj → obj → Set } {a b c : obj   } (f : (Arrow {obj} {hom} b c )) → (g : (Arrow {obj} {hom} a b )) → Arrow {obj} {hom} a c
+   id a + id .a = id a
+   id b + mono x = mono x
+   id a + connected x y = connected x y
+   mono x + id a = mono x
+   mono x + mono y = connected x (mono y)
+   mono x + connected y z = connected x ( connected y z )
+   connected x y + z = connected x ( y + z )
+ 
+   data _==_ : {a b  : Objs } → (f g : Arrow {Objs} {arrow} a b ) → Set where
+      rrefl  : {a b : Objs } → {f : Arrow {Objs} {arrow} a b } →  f == f
+      irefl  : {a : Objs } → ( id a ) == ( id a )
+      mrefl  : {a b : Objs } {x : arrow a b } → ( mono x ) == ( mono x )
+      trefl  : {a : Objs } { x y : Arrow a ⊤ } → x == y
+      crefl  : {a b c : Objs } { x : arrow b c } → {f g : Arrow a b } → f == g → ( connected x f ) == ( connected x g )
+
+   ==sym : {a b  : Objs } → {f g : Arrow {Objs} {arrow} a b } → f == g  → g == f
+   ==sym rrefl = rrefl
+   ==sym irefl = irefl
+   ==sym mrefl = mrefl
+   ==sym trefl = trefl
+   ==sym (crefl x) = crefl ( ==sym x )
 
-   GLCat : Category Level.zero Level.zero Level.zero
-   GLCat = GraphtoCat Objs arrow
-      where open graphtocat
+   ==trans : {a b : Objs } → {f g h : Arrow {Objs} {arrow} a b } → f == g → g == h  → f == h
+   ==trans rrefl rrefl = rrefl
+   ==trans rrefl irefl = rrefl
+   ==trans rrefl mrefl = rrefl
+   ==trans rrefl trefl = trefl
+   ==trans rrefl (crefl y) = crefl y
+   ==trans irefl rrefl = rrefl
+   ==trans irefl irefl = rrefl
+   ==trans irefl trefl = trefl
+   ==trans mrefl rrefl = rrefl
+   ==trans mrefl mrefl = rrefl
+   ==trans mrefl trefl = trefl
+   ==trans trefl rrefl = trefl
+   ==trans trefl mrefl = trefl
+   ==trans trefl trefl = trefl
+   ==trans (crefl x) rrefl = (crefl x)
+   ==trans (crefl x) trefl = trefl
+   ==trans (crefl x) (crefl y) = crefl ( ==trans x y )
+   ==trans trefl irefl = trefl
+   ==trans trefl (crefl y) = trefl
 
-   open graphtocat
+   assoc-+ : {a b c d : Objs   }
+        (f : (Arrow  {Objs} {arrow} c d )) → (g : (Arrow {Objs} {arrow} b c )) → (h : (Arrow {Objs} {arrow} a b )) →
+        ( f + (g + h)) ==  ((f + g) + h )
+   assoc-+ (id a) (id .a) (id .a) = irefl
+   assoc-+ (id a) (id .a) (mono x) = mrefl
+   assoc-+ (id a) (id .a) (connected h h₁) = crefl rrefl 
+   assoc-+ (id a) (mono x) (id a₁) = mrefl
+   assoc-+ (id a) (mono x) (mono x₁) = crefl mrefl
+   assoc-+ (id a) (mono x) (connected h h₁) = crefl rrefl
+   assoc-+ (id a) (connected g h) _ = crefl rrefl
+   assoc-+ (mono x) (id a) (id .a) = mrefl
+   assoc-+ (mono x) (id a) (mono x₁) = crefl mrefl
+   assoc-+ (mono x) (id a) (connected h h₁) = crefl rrefl
+   assoc-+ (mono x) (mono x₁) (id a) = crefl mrefl
+   assoc-+ (mono x) (mono x₁) (mono x₂) = crefl ( crefl mrefl )
+   assoc-+ (mono x) (mono x₁) (connected h h₁) = crefl ( crefl rrefl )
+   assoc-+ (mono x) (connected g g₁) _ = crefl rrefl
+   assoc-+ (connected f g) (x) (y) = crefl ( assoc-+ g x y ) 
 
-   product : {a b c : Obj GLCat} → Hom GLCat c a → Hom GLCat c b → Hom GLCat c ( a ∧ b )
+   product : {a b c : Objs } → Arrow c a → Arrow c b → Arrow {Objs} {arrow} c ( a ∧ b )
    product {a} {b} {c} y (connected {_} {_} {d} x g) =   connected (< π , x ・ π'  >) ( product y g )
    product {a} {b} {c} (connected {_} {_} {d} x g) y =   connected (< x ・ π , π'  >) ( product g y )
    product {a} {.a} {.a} (id a) (id .a) = mono ( < id a , id a > )
@@ -623,21 +683,92 @@
    product {a} {.a₁} {.a₁} (mono x) (id a₁) = mono ( < x , id a₁ > )
    product {a} {b} {c} (mono x) (mono x₁) = mono ( < x , x₁ > )
 
-   star : {a b c : Obj GLCat} → Hom GLCat (a ∧ b) c → Hom GLCat a (c <= b)
+   star : {a b c : Objs} → Arrow (a ∧ b) c → Arrow {Objs} {arrow} a (c <= b)
    star {a} {b} {.(a ∧ b)} (id .(a ∧ b)) = mono ( id (a ∧ b ) * )
    star {a} {b} {c} (mono x) = mono ( x * )
    star {a} {b} {c} (connected {_} {d} {_} x y) = connected (  ( x  ・  ε  ) * ) ( star y )
 
---   GL :  PositiveLogic GLCat
---   GL = record {
---         ⊤ = ⊤
---       ; ○ = λ f → mono (○ f)
---       ; _∧_ =  _∧_
---       ; <_,_> = λ f g → product f g
---       ; π =  mono π
---       ; π' = mono π'
---       ; _<=_ = _<=_
---       ; _* =  star
---       ; ε = mono ε
---    }
+   GraphtoCCC :   Category  Level.zero Level.zero Level.zero   
+   GraphtoCCC  = record {
+            Obj  = Objs ;
+            Hom = λ a b →   Arrow a b  ;
+            _o_ =  λ{a} {b} {c} x y → _+_  x y ;
+            _≈_ =  λ x y → x  == y ;
+            Id  =  λ{a} → id a ;
+            isCategory  = record {
+                    isEquivalence =  record {refl = rrefl ; trans = ==trans ; sym = ==sym } ;
+                    identityL  = λ{a b f} → identityL    {a} {b} {f} ;
+                    identityR  = λ{a b f} → identityR    {a} {b} {f} ;
+                    o-resp-≈  = λ{a b c f g h i} →  o-resp-≈     {a} {b} {c} {f} {g} {h} {i} ;
+                    associative  = λ{a b c d f g h } → assoc-+  f g h
+               }
+           }  where
+                identityL :   {A B : Objs } {f : ( Arrow    A B) } →  ((id B)  + f) ==  f
+                identityL {_} {_} {id a} = irefl
+                identityL {_} {_} {mono x} = mrefl
+                identityL {_} {_} {connected x f} = crefl rrefl
+                identityR :   {A B : Objs } {f : ( Arrow {Objs} {arrow}  A B) } →   ( f + id A )  == f
+                identityR {_} {_} {id a} = irefl
+                identityR {_} {_} {mono x} = mrefl
+                identityR {_} {_} {connected x f} = crefl ( identityR )
+                o-resp-≈ :   {A B C : Objs   } {f g :  ( Arrow    A B)} {h i : ( Arrow B C)} →
+                    f  == g → h  == i → ( h + f )  == ( i + g )
+                o-resp-≈ {_} {_} {_} {f} {.f} {h} {.h} rrefl rrefl = rrefl
+                o-resp-≈ {_} {_} {_} {f} {.f} {.(id _)} {.(id _)} rrefl irefl = rrefl
+                o-resp-≈ {_} {_} {_} {f} {.f} {.(mono _)} {.(mono _)} rrefl mrefl = rrefl
+                o-resp-≈ {_} {_} {_} {f} {.f} {h} {i} rrefl trefl = trefl
+                o-resp-≈ {_} {_} {_} {f} {.f} {.(connected _ _)} {.(connected _ _)} rrefl (crefl h=i) = crefl ( o-resp-≈ rrefl h=i )
+                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {h} {.h} irefl rrefl = rrefl
+                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {.(id _)} {.(id _)} irefl irefl = rrefl
+                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {.(mono _)} {.(mono _)} irefl mrefl = rrefl
+                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {h} {i} irefl trefl = trefl
+                o-resp-≈ {_} {_} {_} {.(id _)} {.(id _)} {.(connected _ _)} {.(connected _ _)} irefl (crefl h=i) = crefl ( o-resp-≈ rrefl h=i )
+                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {h} {.h} mrefl rrefl = rrefl
+                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {.(id _)} {.(id _)} mrefl irefl = rrefl
+                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {.(mono _)} {.(mono _)} mrefl mrefl = rrefl
+                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {h} {i} mrefl trefl = trefl
+                o-resp-≈ {_} {_} {_} {.(mono _)} {.(mono _)} {.(connected _ _)} {.(connected _ _)} mrefl (crefl h=i) = crefl ( o-resp-≈ rrefl h=i )
+                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {id a} {.(id a)} (crefl f=g) rrefl = crefl f=g
+                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {mono x} {.(mono x)} (crefl f=g) rrefl = crefl ( crefl f=g )
+                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {connected x h} {.(connected x h)} (crefl f=g) rrefl =
+                   crefl ( o-resp-≈ (crefl f=g) rrefl )
+                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {.(id _)} {.(id _)} (crefl f=g) irefl = crefl f=g
+                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {.(mono _)} {.(mono _)} (crefl f=g) mrefl = crefl (crefl f=g) 
+                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {h} {i} (crefl f=g) trefl = trefl
+                o-resp-≈ {_} {_} {_} {.(connected _ _)} {.(connected _ _)} {.(connected _ _)} {.(connected _ _)} (crefl f=g) (crefl h=i) = 
+                   crefl ( o-resp-≈ (crefl f=g) h=i  )
+                o-resp-≈ {_} {_} {_} {f} {g} {h} {.h} trefl rrefl = {!!}
+                o-resp-≈ {_} {_} {_} {f} {g} {.(id ⊤)} {.(id ⊤)} trefl irefl = {!!}
+                o-resp-≈ {_} {_} {_} {f} {g} {.(mono _)} {.(mono _)} trefl mrefl = {!!}
+                o-resp-≈ {_} {_} {_} {f} {g} {h} {i} trefl trefl = trefl
+                o-resp-≈ {_} {_} {_} {f} {g} {.(connected _ _)} {.(connected _ _)} trefl (crefl h=i) = {!!}
 
+
+--      GLCCC : CCC GraphtoCCC 
+--      GLCCC = record {
+--             １ =  ⊤
+--          ;  ○ = λ f → mono (○ f)
+--          ;  _∧_  = _∧_
+--          ;  <_,_> = λ f g → product f g
+--          ;  π = mono π
+--          ;  π' = mono π'
+--          ;  _<=_ =  _<=_
+--          ;  _* = star
+--          ;  ε = mono ε
+--          ;  isCCC = isc
+--        } where
+--           GC = GraphtoCCC 
+--           isc : ? -- IsCCC GC ⊤ (λ f → mono (○ f)) _∧_ ( λ f g → product f g) (mono π) (mono π') _<=_ star (mono ε ) 
+--           e2 : {a : Obj GC } → ∀ { f : Hom GC a ⊤ } →  GC [ f ≈ mono (○ a) ]
+--           e2 {.⊤} {id .⊤} = {!!}
+--           e2 {a} {mono x} = {!!}
+--           e2 {a} {connected x f} = {!!}
+--           e3a = {!!}
+--           e3b = {!!}
+--           e3c = {!!}
+--           π-cong = {!!}
+--           e4a = {!!}
+--           e4b = {!!}
+--           *-cong = {!!}
+--   
+--