Mercurial > hg > Members > kono > Proof > category

changeset 802:7bc41fc7b563

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
graph with positive logic to Sets
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Apr 2019 03:50:30 +0900
parents aa4fbd007247
children 984d20c10c87
files CCChom.agda
diffstat 1 files changed, 56 insertions(+), 125 deletions(-) [+]
line wrap: on
line diff
--- a/CCChom.agda	Wed Apr 24 11:09:41 2019 +0900
+++ b/CCChom.agda	Thu Apr 25 03:50:30 2019 +0900
@@ -588,138 +588,69 @@
 
 module ccc-from-graph ( Atom : Set ) ( homm : Atom → Atom → Set ) where
 
-   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
+   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
 
-   data Objs : Set where
-      ⊤ : Objs
-      atom : Atom → Objs
-      _∧_ : Objs → Objs → Objs
-      _<=_ : Objs → Objs → Objs
+   data objs : Set where
+      atom : Atom → objs
+      ⊤ : objs
+      _∧_ : objs → objs → objs
+      _<=_ : objs → objs → objs
 
-   data arrow  : Objs → Objs → Set where
+   data arrow  : objs → objs → Set where
       hom : {a b : Atom} →  homm a b → arrow (atom a) (atom b)
-      id : (a : Objs ) → arrow a a
-      _・_ : {a b c : Objs } → arrow b c → arrow a b → arrow a c
-      ○ : (a : Objs ) → arrow a ⊤
-      π : {a b : Objs } → arrow ( a ∧ b ) a
-      π' : {a b : Objs } → arrow ( a ∧ b ) b
-      <_,_> : {a b c : Objs } → arrow c a → arrow c b → arrow c (a ∧ b)
-      ε : {a b : Objs } → arrow ((a <= b) ∧ b ) a
-      _* : {a b c : Objs } → arrow (c ∧ b ) a → arrow c ( a <= 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 )
 
    open import discrete
    open graphtocat
 
-   GC :   Category  Level.zero Level.zero Level.zero   
-   GC = GraphtoCat Objs arrow
-
-   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 > )
-   product {a} {b} {.a} (id a) (mono x) = mono ( < id a , x > )
-   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 : 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 )
-
-
-   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
-      trefl : {a b : Objs} → {h i : Arrow {Objs} {arrow} ⊤ b } {f g : Arrow {Objs} {arrow} a ⊤ } → h == i → (h + f) == (i + g)
-
-   ≡→== : {a b  : Objs } → {f g : Arrow {Objs} {arrow} a b } → f ≡ g → f == g
-   ≡→== refl = rrefl
+   -- positive intutionistic calculus
+   DX :   Category  Level.zero Level.zero Level.zero   
+   DX = GraphtoCat objs arrow
 
-   r== : {a b : Objs } →  { f : Arrow {Objs} {arrow} a b } → f == f
-   r== = ≡→== refl
-
-   s== : {a b : Objs } →  { f g : Arrow {Objs} {arrow} a b } → f == g → g == f
-   s== rrefl = rrefl
-   s== (trefl rrefl) = trefl rrefl
-   s== (trefl (trefl eq)) = trefl {!!}
-
-   t== : {a b : Objs } →  { i j k : Arrow {Objs} {arrow} a b } → i == j → j == k → i == k
-   t== rrefl rrefl = rrefl
-   t== eq eq1 = {!!}
-
-   ctcong : {a b c : Objs } →  { f g : Arrow {Objs} {arrow} a b } → { x : arrow b c } → f == g  → connected x f == connected x g
-   ctcong rrefl = rrefl
-   ctcong (trefl eq) = trefl {!!}
-
-   ccc-e2 : {a : Objs } → ∀ { f : Arrow {Objs} {arrow} a ⊤ } →  f ==  mono (○ a) 
-   ccc-e2 {a} {f} = {!!}
-
-   -- Reflexive : ∀ {a ℓ} {A : Set a} → Rel A ℓ → Set _
-   -- Reflexive _∼_ = ∀ {x} → x ∼ x
-
-   open  import  Relation.Binary.Core
-   open  import  Relation.Binary
-   import Relation.Binary.EqReasoning as EqR
+   -- open import Category.Sets
+   -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-   cccIEQ : {a b : Objs } → Setoid Level.zero Level.zero
-   cccIEQ {a} {b} = record {
-        Carrier   = Arrow {Objs} {arrow} a b 
-      ; _≈_       = _==_
-      ; isEquivalence = record {refl = r== ; trans = t== ; sym = s== }
-    }
-
+   CS : Functor DX (Sets {Level.zero})
+   FObj CS (atom x) = Atom
+   FObj CS ⊤ = One'
+   FObj CS (x ∧ x₁) =  FObj CS x /\ FObj CS  x₁ 
+   FObj CS (x <= x₁) = FObj CS x₁ → FObj CS x
+   FMap CS {a} {.a} (id a) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
+   FMap CS {a} {b} (mono (x ・ y )) = Sets [ FMap CS (mono x) o FMap CS (mono y) ]
+   FMap CS {atom a} {atom b} (mono (hom f)) = λ x → b 
+   FMap CS {a} {.a} (mono (id a)) = id1 Sets (FObj CS a) where open ≈-Reasoning (Sets {Level.zero})
+   FMap CS {a} {⊤} (mono (○ a)) = λ x → OneObj'
+   FMap CS {(b ∧ _)} {b} (mono π) = proj₁
+   FMap CS {(_ ∧ b)} {b} (mono π') = proj₂
+   FMap CS {((b <= _) ∧ _)} {b} (mono ε) = λ x → ( proj₁ x ) ( proj₂ x )
+   FMap CS {a} {(_ ∧ _)} (mono < f , g >) = λ x → ( FMap CS (mono f) x , FMap CS (mono g) x )
+   FMap CS {a} {(_ <= _)} (mono (f *)) = λ x → λ y → FMap CS (mono f) ( x , y )
+   FMap CS {a} {⊤} (connected x f) = λ x → OneObj'
+   FMap CS {a} {b} (connected x f) = Sets [ FMap CS (mono x) o FMap CS f ]
+   isFunctor CS = isf where
+       distrCS : {a b c : Obj DX } { g : Hom DX b c } { f : Hom DX a b } → Sets [ FMap CS (DX [ g o f ]) ≈ Sets [ FMap CS g o FMap CS f ] ]
+       distrCS {a} {.a} {.a} {id a} {id a} = refl
+       distrCS {a} {b} {.b} {id b} {mono x} = refl
+       distrCS {a} {b} {.b} {id b} {connected x g} = refl
+       distrCS {a} {.(atom _)} {.(atom _)} {mono (hom x)} {g} = {!!}
+       distrCS {a} {.a₁} {.a₁} {mono (id a₁)} {g} = {!!}
+       distrCS {a} {.a₁} {.⊤} {mono (○ a₁)} {g} = {!!}
+       distrCS {a} {.(c ∧ _)} {c} {mono π} {g} = {!!}
+       distrCS {a} {.(_ ∧ c)} {c} {mono π'} {g} = {!!}
+       distrCS {a} {.((c <= _) ∧ _)} {c} {mono ε} {g} = {!!}
+       distrCS {a} {b} {.(_ ∧ _)} {mono < x , x₁ >} {g} = {!!}
+       distrCS {a} {b} {c} {mono (x ・ x₁)} {g} = {!!}
+       distrCS {a} {b} {.(_ <= _)} {mono (x *)} {g} = {!!}
+       distrCS {a} {b} {c} {connected x f} {g} = {!!}
+       isf : IsFunctor DX Sets (FObj CS) ( FMap CS ) 
+       IsFunctor.identity isf = extensionality Sets ( λ x → refl )
+       IsFunctor.distr isf = distrCS
+       IsFunctor.≈-cong isf refl = refl
 
-   GraphtoCCC :   Category  Level.zero Level.zero Level.zero   
-   GraphtoCCC  = record {
-            Obj  = Objs ;
-            Hom = λ a b →   Arrow  {Objs} {arrow} a b  ;
-            _o_ =  _+_ ;
-            _≈_ =   _==_  ;
-            Id  =  λ{a} → id a ;
-            isCategory  = record {
-                    isEquivalence =  record {refl = r== ; trans = t== ; sym = s== }
-                 ;  identityL  = identityL
-                 ;  identityR  = identityR
-                 ;  o-resp-≈  = λ{a b c f g h i} →  {!!}
-                 ;  associative  = λ{a b c d f g h } → {!!}
-               }
-           } where
-       identityL : {a b : Objs } →  { f : Arrow {Objs} {arrow} a b } → (id b + f) == f
-       identityL {a} {.a} {id a} = rrefl
-       identityL {a} {b} {mono x} = rrefl
-       identityL {a} {b} {connected x f} = rrefl
-       identityR : {a b : Objs } →  { f : Arrow {Objs} {arrow} a b } → (f + id a ) == f
-       identityR {a} {.a} {id a} = rrefl
-       identityR {a} {b} {mono x} = rrefl
-       identityR {a} {b} {connected x f} = ctcong identityR
-
---          ≈⟨ {!!} ⟩
---          ∎ where open EqR cccIEQ -- open IsEquivalence cccIEQ
-
---      GLCCC : CCC GraphtoCCC 
---      GLCCC = record {
---             １ =  ⊤
---          ;  ○ = λ f → mono (○ f)
---          ;  _∧_  = _∧_
---          ;  <_,_> = λ f g → product f g
---          ;  π = mono π
---          ;  π' = mono π'
---          ;  _<=_ =  _<=_
---          ;  _* = star
---          ;  ε = mono ε
---          ;  isCCC = isc
---        } where
---           GC = GraphtoCCC 
---           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 = {!!}
---   
---