Mercurial > hg > Members > kono > Proof > category

changeset 1014:4f1db956d3b4

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 Sun, 21 Mar 2021 00:47:00 +0900
parents 39e2b29e3279
children e01a1d29492b
files src/Polynominal.agda src/deductive.agda
diffstat 2 files changed, 36 insertions(+), 41 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Sat Mar 20 20:48:46 2021 +0900
+++ b/src/Polynominal.agda	Sun Mar 21 00:47:00 2021 +0900
@@ -170,6 +170,10 @@
   _・_ = _[_o_] A
   
   -- every proof b →  c with assumption a has following forms
+  --
+  -- Here, A is actualy A[x]. It contains x and all the arrow generated from x.
+  -- If we can put constraints on rule i, then A is strictly smaller than A[x].
+  --
   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
@@ -245,7 +249,7 @@
   functional-completeness {a} x = record {
          fun = λ y → k x (phi y)
        ; fp = fc0
-       ; uniq = {!!}
+       ; uniq = 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 ]
@@ -284,16 +288,40 @@
               k x y o ( < π o π , <  π' o  π , π' > > o < < x o ○ b , id1 A _ > o π , π' > )   ≈⟨ cdr (IsCCC.distr-π isCCC) ⟩
               k x y o < (π o π) o < < x o ○ b , id1 A _ > o π , π' >  , <  π' o  π , π' > o < < x o ○ b , id1 A _ > o π , π' >  >
                   ≈⟨ cdr (IsCCC.π-cong isCCC (sym assoc) (IsCCC.distr-π isCCC )) ⟩
-              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 π )  , <    π  , π' > >    ≈⟨   cdr (IsCCC.π-cong isCCC {!!} {!!} ) ⟩
+              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 π , π' > > >
+                    ≈⟨ cdr ( IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC))( IsCCC.π-cong isCCC (sym assoc) (IsCCC.e3b isCCC) )) ⟩
+              k x y o < π o ( < x o ○ b , id1 A _ > o π  ) , <  π' o  (π o < < x o ○ b , id1 A _ > o π , π' >) ,  π'  > >
+                ≈⟨  cdr ( IsCCC.π-cong isCCC refl-hom (  IsCCC.π-cong isCCC (cdr (IsCCC.e3a isCCC)) refl-hom )) ⟩
+              k x y o < (π o  < x o ○ b , id1 A _ > o π  ) , <  π' o  (< x o ○ b , id1 A _ > o π ) , π' > >
+                ≈⟨ cdr ( IsCCC.π-cong isCCC  assoc (IsCCC.π-cong isCCC  assoc refl-hom )) ⟩
+              k x y o < (π o  < x o ○ b , id1 A _ > ) o π   , <  (π' o  < x o ○ b , id1 A _ > ) o π  , π' > >
+                  ≈⟨ cdr (IsCCC.π-cong isCCC (car (IsCCC.e3a isCCC)) (IsCCC.π-cong isCCC (car (IsCCC.e3b isCCC)) refl-hom ))  ⟩
+              k x y o < ( (x o ○ b ) o π )  , <   id1 A _  o π  , π' > >    ≈⟨ cdr (IsCCC.π-cong isCCC (sym assoc)  (IsCCC.π-cong isCCC idL refl-hom ))  ⟩
+              k x y o <  x o (○ b  o π )  , <    π  , π' > >    ≈⟨   cdr (IsCCC.π-cong isCCC (cdr (IsCCC.e2 isCCC)) (IsCCC.π-id isCCC) ) ⟩
               k x y o  < x o ○ _ , id1 A _  >    ≈⟨ fc0 record { hom = f ; phi = y} ⟩
              f  ∎ )  ⟩
              f * ∎ 
-        ... | φ-cong y z = {!!}
+        ... | φ-cong {_} {_} {f} {f'} f=f' y = trans-hom (fc0 record { hom = f ; phi = y}) f=f'
+        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 ≈ k x (phi p) ]
+        uniq {b} {c} p f fx=p with phi p
+        ... | i {_} {_} {s} = begin -- f o  < x o ○ b  , id1 A b >  ≈ s
+             f ≈↑⟨ idR ⟩
+             f o  id1 A (a ∧ b)  ≈⟨ {!!} ⟩
+             f o  (< x o ○ b  , id1 A b >  o π' ) ≈⟨ assoc ⟩
+             (f o  < x o ○ b  , id1 A b > ) o π'  ≈⟨ car fx=p ⟩
+             s o π'  ∎ 
+        ... | ii = begin -- fx=p : f o < x o ○ b  , id1 A b > ≈ x
+             f  ≈⟨ {!!} ⟩
+             π  ∎ 
+        ... | iii {_} {_} {_} {g} {h} y z = begin -- fx=p : f o < x o ○ b  , id1 A b > ≈ < g , h >
+             f  ≈⟨ {!!} ⟩
+             < k x y , k x z > ∎ 
+        ... | iv t t₁ = {!!}
+        ... | v t = {!!}
+        ... | φ-cong x t = {!!}
+
         
 
 -- end
--- a/src/deductive.agda	Sat Mar 20 20:48:46 2021 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-open import Level
-open import Category
-open import CCC
-
-module deductive {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (  L :  CCC A ) where
-
-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
-     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