Mercurial > hg > Members > kono > Proof > category

changeset 903:2f0ffd5733a8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Positive Logic with equivalence
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 30 Apr 2020 17:42:12 +0900
parents 6633314ba902
children 3e164b00155f
files CCCGraph.agda
diffstat 1 files changed, 55 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/CCCGraph.agda	Thu Apr 30 11:18:11 2020 +0900
+++ b/CCCGraph.agda	Thu Apr 30 17:42:12 2020 +0900
@@ -134,39 +134,74 @@
    < f , g > ・ h = < f ・ h , g ・ h >
    iv f g ・ h = iv f ( g ・ h )
 
-   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
-   identityR {a} {a} {id a} = refl
-   identityR {a} {⊤} {○ a} = refl
-   identityR {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j  , k > ) identityR identityR
-   identityR {a} {b} {iv f g} = cong (λ k → iv f k ) identityR
-   identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≡ f
-   identityL = refl
-   associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
-                            (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)
-   associative (id a) g h = refl
-   associative (○ a) g h = refl
-   associative < f , f₁ > g h = cong₂ (λ j k → < j  , k > )  (associative f g h) (associative f₁ g h) 
-   associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h )
+   data _≐_ : {a b : Objs } → Arrows a b → Arrows a b → Set ℓ where
+       prefl : {a b : Objs } → {f : Arrows a b } → f ≐ f
+       p⊤ : {a : Objs } → {f g : Arrows a ⊤ } → f ≐ g
+       <p> : {a b c : Objs } → {f h : Arrows a b } {g i : Arrows a c } → f ≐ h → g ≐ i → < f , g > ≐ < h , i >
+       piv : {a b c : Objs } → {f : Arrow b c } {g i : Arrows a b } → g ≐ i → iv f  g  ≐ iv f  i 
+       aiv : { a : Objs } {b c :  vertex G } → {f h : edge G b c } → {g i : Arrows a (atom b) } → _≅_ G f h → g ≐ i → iv (arrow f)  g  ≐ iv (arrow h)  i 
+
+   psym : {a b : Objs } → { f g  : Arrows a b} → f ≐ g → g ≐ f 
+   psym prefl = prefl
+   psym p⊤ = p⊤
+   psym (<p> eq eq₁) = <p> (psym eq) (psym eq₁)
+   psym (piv eq) = piv (psym eq)
+   psym (aiv x eq) = aiv (IsEquivalence.sym (Graph.isEq G) x) (psym eq)
+
+   ptrans : {a b : Objs } → { f g h : Arrows a b} → f ≐ g → g ≐ h → f ≐ h
+   ptrans prefl g=h = g=h
+   ptrans p⊤ g=h = p⊤
+   ptrans (<p> f=g f=g₁) prefl = <p> f=g f=g₁
+   ptrans (<p> f=g f=g₁) (<p> g=h g=h₁) = <p> ( ptrans f=g g=h ) ( ptrans f=g₁ g=h₁ )
+   ptrans (piv f=g) prefl = piv f=g
+   ptrans (piv f=g) p⊤ = p⊤
+   ptrans (piv f=g) (piv g=h) = piv ( ptrans f=g g=h )
+   ptrans (piv f=g) (aiv x g=h) = aiv x (ptrans f=g g=h)
+   ptrans (aiv x f=g) prefl = aiv x f=g
+   ptrans (aiv x f=g) (piv g=h) =  aiv x (ptrans f=g g=h)
+   ptrans (aiv x f=g) (aiv x₁ g=h) = aiv (IsEquivalence.trans (Graph.isEq G) x x₁) (ptrans f=g g=h) 
+
+   identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) ≐ f
+   identityL = prefl
+
+   identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≐ f
+   identityR {a} {a} {id a} = prefl
+   identityR {a} {⊤} {○ a} = p⊤
+   identityR {a} {_} {< f , f₁ >} = <p> identityR identityR
+   identityR {a} {b} {iv f g} = piv identityR
+
+   assoc≐ : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
+                            (f ・ (g ・ h)) ≐ ((f ・ g) ・ h)
+   assoc≐ (id a) g h = prefl
+   assoc≐ (○ a) g h = p⊤
+   assoc≐ < f , f₁ > g h = <p> (assoc≐ f g h) (assoc≐ f₁ g h) 
+   assoc≐ (iv f f1) g h = piv ( assoc≐ f1 g h )
 
    -- positive intutionistic calculus
-   PL :  Category  c₁  (c₁ ⊔ c₂) (c₁ ⊔ c₂)
+   PL :  Category  c₁  (c₁ ⊔ c₂) ℓ
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
             _o_ =  λ{a} {b} {c} x y → x ・ y ;
-            _≈_ =  λ x y → x ≡  y ;
+            _≈_ =  λ x y → x ≐  y ;
             Id  =  λ{a} → id a ;
             isCategory  = record {
-                    isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } ;
+                    isEquivalence =  record {refl = prefl ; trans = ptrans ; sym = psym} ;
                     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 } → associative  f g h
+                    associative  = λ{a b c d f g h } → assoc≐  f g h
                }
            } where  
               o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
-                                    f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
-              o-resp-≈ refl refl = refl 
+                                    f ≐  g → h ≐  i → (h ・ f) ≐ (i ・ g)
+              o-resp-≈ {_} {_} {⊤} {f} {g} {h} {i} f=g h=i = p⊤
+              o-resp-≈ {_} {_} {_} {f} {g} {id a} {id a} f=g h=i = ptrans (ptrans f=g (psym identityR) ) identityR
+              o-resp-≈ {_} {_} {_} {f} {g} {< h , h₁ >} {< h , h₁ >} f=g prefl = <p> (o-resp-≈ f=g prefl ) (o-resp-≈ f=g prefl )
+              o-resp-≈ {_} {_} {_} {f} {g} {< h , h₁ >} {< i , i₁ >} f=g (<p> h=i h=i₁) = <p> (o-resp-≈ f=g h=i ) (o-resp-≈ f=g h=i₁)
+              o-resp-≈ {_} {_} {_} {f} {g} {iv f₁ h} {iv f₁ h} f=g prefl = piv ( o-resp-≈ f=g prefl )
+              o-resp-≈ {_} {_} {_} {f} {g} {iv f₁ h} {iv f₁ i} f=g (piv h=i) = piv ( o-resp-≈ f=g  h=i)
+              o-resp-≈ {_} {_} {_} {f} {g} {iv (arrow x) h} {iv (arrow y) i} f=g (aiv x=y h=i) = aiv x=y (o-resp-≈ f=g  h=i)
 
 --------
 --
@@ -221,7 +256,7 @@
            adistr eq x = cong ( λ k → amap x k ) eq
         isf : IsFunctor PL Sets fobj fmap 
         IsFunctor.identity isf = extensionality Sets ( λ x → refl )
-        IsFunctor.≈-cong isf refl = refl
+        IsFunctor.≈-cong isf = {!!}
         IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
    open import subcat