Mercurial > hg > Members > kono > Proof > category

changeset 1010:bfd9c55ac628

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 20 Mar 2021 13:01:16 +0900
parents a611f59932ef
children a104c3baefe4
files src/CCCSets.agda src/deductive.agda
diffstat 2 files changed, 73 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/src/CCCSets.agda	Fri Mar 12 19:36:18 2021 +0900
+++ b/src/CCCSets.agda	Sat Mar 20 13:01:16 2021 +0900
@@ -104,11 +104,11 @@
 --       a -----------→ Ω
 --             h
 
-data II  {c : Level } : Set c where
-     true : II
-     false : II
+data Bool  {c : Level } : Set c where
+     true : Bool
+     false : Bool
 
-data Tker {c : Level} {a : Set c} ( f : a → II {c} ) : Set c where
+data Tker {c : Level} {a : Set c} ( f : a → Bool {c} ) : Set c where
      isTrue : (x : a ) → f x ≡ true → Tker f
 
 irr : { c₂ : Level}  {d : Set c₂ }  { x y : d } ( eq eq' :  x  ≡ y ) → eq ≡ eq'
@@ -116,16 +116,16 @@
 
 topos : {c : Level } → Topos (Sets {c}) sets
 topos {c}  = record {
-         Ω = II
+         Ω = Bool
       ;  ⊤ = λ _ → true
       ;  Ker = tker
       ;  char = tchar
       ;  isTopos = record {
-                 char-uniqueness  = λ {a} {b} {h} m mono →  extensionality Sets ( λ x → {!!} )
+                 char-uniqueness  = λ {a} {b} {h} m mono →  extensionality Sets ( λ x → uniq h m mono x )
               ;  ker-iso = {!!}
          }
     } where
-        tker   : {a : Obj Sets} (h : Hom Sets a II) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ])
+        tker   : {a : Obj Sets} (h : Hom Sets a Bool) → Equalizer Sets h (Sets [ (λ _ → true) o CCC.○ sets a ])
         tker {a} h = record {
                 equalizer-c = Tker h
               ; equalizer = etker 
@@ -151,8 +151,26 @@
                 (k'   : Hom Sets d (Tker h)) (ek=h : Sets [ Sets [ etker o k' ] ≈ h1 ]) (x    : d) →  k h1 eq x ≡ k' x
            uniq h1 eq k' ek=h x with cong (λ j → j x) ek=h --  etker (k h1 eq x) ≡ etker (k' x)
            ... | t = tker-cong (k h1 eq x) (k' x) (sym t)
-        tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a II
+        kiso : {a b : Obj Sets} (m : Hom Sets b a) (mono : Mono Sets m) → IsoL Sets m (Equalizer.equalizer (tker (λ x → true)))
+        kiso {a} {b} m mono = record { iso-L = record {
+            ≅→ = λ x → isTrue (m x) refl ; ≅← = ki1 ; iso→  = {!!} ; iso←  = {!!} } ; iso≈L   = {!!} } where
+          ki1 : Hom Sets (Equalizer.equalizer-c (tker (λ x → true))) b
+          ki1 (isTrue x eq) = {!!}
+        tchar : {a b : Obj Sets} (m : Hom Sets b a) → Mono Sets m → Hom Sets a Bool
         tchar {a} {b} m mono x = true
+        uniq : {a : Obj (Sets {c})} {b : Obj Sets} (h : Hom Sets a Bool) (m : Hom Sets b a) (mono : Mono Sets m) (x : a) → true ≡ h x
+        uniq {a} {b} h m mono x = begin
+            true ≡⟨⟩
+            (λ × → true ) x ≡⟨ {!!} ⟩
+            {!!} ≡⟨ cong (λ k → h (k x)  ) (IsEqualizer.ek=h (Equalizer.isEqualizer (tker h)) {{!!}} {{!!}} )  ⟩
+            h x  ∎  where
+              open ≡-Reasoning 
+              yyy : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
+              yyy f g eq = Mono.isMono mono f g eq
+              yyy1 : {c : Obj Sets } → (f g : c → b ) → Sets [ Sets [ m o f ] ≈ Sets [ m o g ] ] → f ≡ g
+              yyy1 f g eq = Mono.isMono mono f g eq
+
+           
 
 open import graph
 module ccc-from-graph {c₁ c₂ : Level }  (G : Graph {c₁} {c₂})  where
--- a/src/deductive.agda	Fri Mar 12 19:36:18 2021 +0900
+++ b/src/deductive.agda	Sat Mar 20 13:01:16 2021 +0900
@@ -6,32 +6,35 @@
 
 -- positive logic 
 
-record PositiveLogic {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
-     field
-         ⊤ : Obj A 
-         ○ : (a : Obj A ) → Hom A a ⊤ 
-         _∧_ : Obj A → Obj A → Obj A   
-         <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
-         π : {a b : Obj A } → Hom A (a ∧ b) a 
-         π' : {a b : Obj A } → Hom A (a ∧ b) b  
-         _<=_ : (a b : Obj A ) → Obj A 
-         _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
-         ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
+-- record PositiveLogic {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
+--      field
+--          ⊤ : Obj A 
+--          ○ : (a : Obj A ) → Hom A a ⊤ 
+--          _∧_ : Obj A → Obj A → Obj A   
+--          <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
+--          π : {a b : Obj A } → Hom A (a ∧ b) a 
+--          π' : {a b : Obj A } → Hom A (a ∧ b) b  
+--          _<=_ : (a b : Obj A ) → Obj A 
+--          _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
+--          ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 
 
+open import CCC
 
-module deduction-theorem (  L :  PositiveLogic A ) where
+module deduction-theorem (  L :  CCC A ) where
 
-  open PositiveLogic L
+  open CCC.CCC L
   _・_ = _[_o_] A
   
   -- every proof b →  c with assumption a has following forms
-  
-  data  φ  {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ) where
+
+  ⊤ = １
+  data  φ  {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ⊔ ℓ) where
      i   : {b c : Obj A} {k : Hom A b c } → φ x k
      ii  : φ x {⊤} {a} x
      iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
      iv  : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
      v   : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
+     φ-cong   : {b c : Obj A} {k k' : Hom A b c } → A [ k ≈ k' ] → φ x k  → φ x k'
   
   α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
   α = < π  ・ π   , < π'  ・ π  , π'  > >
@@ -44,6 +47,33 @@
   k x∈a (iii ψ χ ) = < k x∈a ψ  , k x∈a χ  >
   k x∈a (iv ψ χ ) = k x∈a ψ  ・ < π , k x∈a χ  >
   k x∈a (v ψ ) = ( k x∈a ψ  ・ α ) *
+  k x∈a (φ-cong  eq ψ) = k x∈a  ψ
 
---  toφ : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
---  toφ {a} {b} {c} x∈a z = {!!}
+  toφ : {a b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
+  toφ {a} {b} {c} x∈a z = i
+
+  record PHom {a : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+    field
+       hom : Hom A b c 
+       phi : φ x {b} {c} hom
+
+  open PHom
+  open import HomReasoning
+  open import cat-utility
+  
+  Polynominal :  {a : Obj A } ( x : Hom A ⊤ a ) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) ℓ 
+  Polynominal {a} x =  record {
+            Obj  = Obj A;
+            Hom = λ b c → PHom {a} {x} b c ;
+            _o_ =  λ{a} {b} {c} x y → record { hom = A [ hom x o hom y ] ; phi = iv (phi x) (phi y) } ;
+            _≈_ =  λ x y → A [ hom x ≈ hom y ] ;
+            Id  =  λ{a} → record { hom = id1 A a ; phi = i } ;
+            isCategory  = record {
+                    isEquivalence =  {!!} ;
+                    identityL  = λ {a b f} → {!!} ;
+                    identityR  = λ {a b f} → {!!} ;
+                    o-resp-≈  = λ {a b c f g h i} → {!!} ;
+                    associative  = λ{a b c d f g h } → {!!} 
+               }
+           } 
+