Mercurial > hg > Members > kono > Proof > category

changeset 1012:5dcbf2b9194e

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 20:33:28 +0900
parents a104c3baefe4
children 39e2b29e3279
files src/Polynominal.agda src/deductive.agda
diffstat 2 files changed, 145 insertions(+), 80 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Sat Mar 20 16:03:45 2021 +0900
+++ b/src/Polynominal.agda	Sat Mar 20 20:33:28 2021 +0900
@@ -87,12 +87,15 @@
     SCat : Category c₁ c₂ ℓ
     SCat = record { Obj = Obj A ; Hom = SHom ; _o_ = _*_ ; _≈_ = _⋍_ ; Id  = λ {a} → S-id a ; isCategory = isSCat }
 
+  module coKleisli' { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { S : Functor A A } (SM : coMonad A S) where
+
   open CCC.CCC C
   open coMonad 
   open Functor
   open NTrans
   open import Category.Cat
   
+  open ≈-Reasoning A
   SA : (a : Obj A) → Functor A A
   SA a = record {
        FObj = λ x → a ∧ x
@@ -103,7 +106,6 @@
         ; distr = sa-distr
        }
     } where
-        open ≈-Reasoning A
         sa-id :  {b : Obj A} →  < π , ( id1 A b o π'  ) > ≈ id1 A (a ∧ b ) 
         sa-id {b} = begin
            < π , ( id1 A b o π'  ) > ≈⟨ IsCCC.π-cong isCCC (sym idR) (trans-hom idL (sym idR) ) ⟩
@@ -130,7 +132,6 @@
          ; assoc = assoc2
         }
      } where
-        open ≈-Reasoning A
         δ-comm :  {a₁ : Obj A} {b : Obj A} {f : Hom A a₁ b} →
              FMap (_○_ (SA a)  (SA a)) f o < π , id1 A _ > ≈ < π , id1 A _ > o FMap (SA a) f 
         δ-comm {x} {b} {f} = begin
@@ -164,7 +165,132 @@
 
 
 
-  -- functional-completeness : (C : CCC A ) → {a : Obj A} → ( x : Hom A (CCC.１ C) a ) → {!!}
-  -- functional-completeness = {!!}
+  -- open import deductive A C
+
+  _・_ = _[_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
+     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 ) )
+  α = < π  ・ π   , < π'  ・ π  , π'  > >
+  
+  -- genetate (a ∧ b) → c proof from  proof b →  c with assumption a
+  
+  k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x∈a z ) → Hom A (a ∧ b) c
+  k x∈a {k} i = k ・ π'
+  k x∈a ii = π
+  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 = 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
+
+  -- date _≅_ : {a b c : Hom A} → { x : Hom A ⊤ a } → (f g : PHom b c ) → Set (c₁ ⊔ c₂ ⊔ ℓ) where
+  --    pcomp : { a b c : Hom A } → A [ A [ hom g o hom f ] ≈ hom h ] → (A [ hom g o hom f ]) ≅ hom h
+
+  -- this is too easy, so what is A[x]?
+  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 =  record { sym = sym-hom ; trans = trans-hom ; refl = refl-hom } ;
+                    identityL  = λ {a b f} → idL ;
+                    identityR  = λ {a b f} → idR ;
+                    o-resp-≈  = λ {a b c f g h i} → resp ;
+                    associative  = λ{a b c d f g h } → assoc 
+               }
+           }  
+
+  Hx :  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Functor A (Polynominal x)
+  Hx {a} x = record {
+     FObj = λ a → a
+   ; FMap = λ f → record { hom = f ; phi = i }
+   ; isFunctor = record {
+        identity = refl-hom
+      ; distr = refl-hom
+      ; ≈-cong = λ eq → eq
+     }
+   } 
+
+  record Functional-completeness {a : Obj A} ( x : Hom A １ a ) : Set  (c₁ ⊔ c₂ ⊔ ℓ) where
+    field 
+      fun  : {b c : Obj A} →  PHom {a} {１} {x} b c  → Hom A (a ∧ b) c
+      fp   : {b c : Obj A} →  (p : PHom b c)  → A [ A [ fun p o < A [ x o ○ b ]  , id1 A b  > ] ≈ hom p ] 
+      uniq : {b c : Obj A} →  (p : PHom b c)  → (f : Hom A (a ∧ b) c) → A [ A [ f o < A [ x o ○ b ]  , id1 A b  > ] ≈ hom p ] 
+         → A [ f  ≈ fun p ]
+
+  functional-completeness : {a : Obj A} ( x : Hom A １ a ) → Functional-completeness  x 
+  functional-completeness {a} x = record {
+         fun = λ y → k x (phi y)
+       ; fp = fc0
+       ; uniq = {!!}
+     } where
+        open φ
+        fc0 :  {b c : Obj A} (p : PHom b c) → A [ A [ k x (phi p) o < A [ x o ○ b ] , id1 A b > ] ≈ hom p ]
+        fc0 {b} {c} p with phi p
+        ... | i {_} {_} {s} = begin
+             (s o π') o < ( x o ○ b ) , id1 A b > ≈↑⟨ assoc ⟩
+             s o (π' o < ( x o ○ b ) , id1 A b >) ≈⟨ cdr (IsCCC.e3b isCCC ) ⟩
+             s o id1 A b ≈⟨ idR ⟩
+             s ∎
+        ... | ii = begin
+             π o < ( x o ○ b ) , id1 A b > ≈⟨ IsCCC.e3a isCCC ⟩
+             x o ○ b  ≈↑⟨ cdr (IsCCC.e2 isCCC ) ⟩
+             x o id1 A b  ≈⟨ idR ⟩
+             x ∎
+        ... | iii {_} {_} {_} {f} {g} y z  = begin
+             < k x y , k x z > o < (x o ○ b ) , id1 A b > ≈⟨ IsCCC.distr-π isCCC  ⟩
+             < k x y o < (x o ○ b ) , id1 A b > , k x z o < (x o ○ b ) , id1 A b > >
+                 ≈⟨ IsCCC.π-cong isCCC (fc0 record { hom = f ; phi = y } ) (fc0 record { hom = g ; phi = z } ) ⟩
+             < f , g > ≈⟨⟩
+             hom p ∎
+        ... | iv {_} {_} {d} {f} {g} y z  = begin
+             (k x y o < π , k x z >) o < ( x o ○ b ) , id1 A b > ≈↑⟨ assoc ⟩
+             k x y o ( < π , k x z > o < ( x o ○ b ) , id1 A b > ) ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
+             k x y o ( < π  o < ( x o ○ b ) , id1 A b > ,  k x z  o < ( x o ○ b ) , id1 A b > > )
+                 ≈⟨ cdr (IsCCC.π-cong isCCC (IsCCC.e3a isCCC) (fc0 record { hom = g ; phi = z} ) ) ⟩
+             k x y o ( < x o ○ b  ,  g > ) ≈↑⟨ cdr (IsCCC.π-cong isCCC (cdr (IsCCC.e2 isCCC)) refl-hom ) ⟩
+             k x y o ( < x o ( ○ d o g ) ,  g > ) ≈⟨  cdr (IsCCC.π-cong isCCC assoc (sym idL)) ⟩
+             k x y o ( < (x o ○ d) o g  , id1 A d o g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩
+             k x y o ( < x o ○ d ,  id1 A d > o g ) ≈⟨ assoc ⟩
+             (k x y o  < x o ○ d ,  id1 A d > ) o g  ≈⟨ car (fc0 record { hom = f ; phi = y }) ⟩
+             f o g  ∎
+        ... | v {_} {_} {_} {f} y = begin
+            ( (k x y o < π o π , <  π' o  π , π' > >) *) o < x o (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩
+            ( (k x y o < π o π , <  π' o  π , π' > >) o < < x o ○ b , id1 A _ > o π , π' > ) * ≈⟨ {!!} ⟩
+            ( k x y o ( < π o π , <  π' o  π , π' > > o < < x o ○ b , id1 A _ > o π , π' > ) ) * ≈⟨ {!!} ⟩
+             ( k x y o < (π o π) o < < x o ○ b , id1 A _ > o π , π' >  , <  π' o  π , π' > o < < x o ○ b , id1 A _ > o π , π' >  > ) * ≈⟨ {!!} ⟩
+             ( k x y o < π o (π o < < x o ○ b , id1 A _ > o π , π' > ) , <  (π' o  π) o < < x o ○ b , id1 A _ > o π , π' > , π'  o < < x o ○ b , id1 A _ > o π , π' > > >  ) * ≈⟨ {!!} ⟩
+             ( k x y o < π o ( < x o ○ b , id1 A _ > o π  ) , <  π' o  (π o < < x o ○ b , id1 A _ > o π , π' >) ,  π'  > >  ) * ≈⟨ {!!} ⟩
+             ( k x y o < (π o  < x o ○ b , id1 A _ > o π  ) , <  π' o  (< x o ○ b , id1 A _ > o π ) , π' > >  ) * ≈⟨ {!!} ⟩
+             ( k x y o < (π o  < x o ○ b , id1 A _ > ) o π   , <  (π' o  < x o ○ b , id1 A _ > ) o π  , π' > >  ) * ≈⟨ {!!} ⟩
+             ( k x y o < ( (x o ○ b ) o π )  , <   id1 A _  o π  , π' > >  ) * ≈⟨ {!!} ⟩
+             ( k x y o < ( (x o ○ b ) o π )  , <    π  , π' > >  ) * ≈⟨  IsCCC.*-cong isCCC ( cdr (IsCCC.π-cong isCCC {!!} {!!} )) ⟩
+             ( k x y o  < x o ○ _ , id1 A _  >  ) * ≈⟨ IsCCC.*-cong isCCC (fc0 record { hom = f ; phi = y}) ⟩
+             f * ∎
+        ... | φ-cong y z = {!!}
+        
 
 -- end
--- a/src/deductive.agda	Sat Mar 20 16:03:45 2021 +0900
+++ b/src/deductive.agda	Sat Mar 20 20:33:28 2021 +0900
@@ -1,32 +1,14 @@
 open import Level
 open import Category
-module deductive {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where
-
--- Deduction Theorem
-
--- 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 
-
 open import CCC
 
-module deduction-theorem (  L :  CCC A ) where
+module deductive {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (  L :  CCC A ) where
 
-  open CCC.CCC L
-  _・_ = _[_o_] A
+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 > 
@@ -34,61 +16,18 @@
      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 ) )
-  α = < π  ・ π   , < π'  ・ π  , π'  > >
+α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
+α = < π  ・ π   , < π'  ・ π  , π'  > >
   
   -- genetate (a ∧ b) → c proof from  proof b →  c with assumption a
   
-  k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x∈a z ) → Hom A (a ∧ b) c
-  k x∈a {k} i = k ・ π'
-  k x∈a ii = π
-  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 = 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
-
-  -- date _≅_ : {a b c : Hom A} → { x : Hom A ⊤ a } → (f g : PHom b c ) → Set (c₁ ⊔ c₂ ⊔ ℓ) where
-  --    pcomp : { a b c : Hom A } → A [ A [ hom g o hom f ] ≈ hom h ] → (A [ hom g o hom f ]) ≅ hom h
+k : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x∈a z ) → Hom A (a ∧ b) c
+k x∈a {k} i = k ・ π'
+k x∈a ii = π
+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  ψ
 
-  -- this is too easy, so what is A[x]?
-  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 =  record { sym = sym-hom ; trans = trans-hom ; refl = refl-hom } ;
-                    identityL  = λ {a b f} → idL ;
-                    identityR  = λ {a b f} → idR ;
-                    o-resp-≈  = λ {a b c f g h i} → resp ;
-                    associative  = λ{a b c d f g h } → assoc 
-               }
-           }  where
-              open ≈-Reasoning A
-
-  Hx :  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Functor A (Polynominal x)
-  Hx {a} x = record {
-     FObj = λ a → a
-   ; FMap = λ f → record { hom = f ; phi = i }
-   ; isFunctor = record {
-        identity = refl-hom
-      ; distr = refl-hom
-      ; ≈-cong = λ eq → eq
-     }
-   } where
-      open ≈-Reasoning 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 = i