Mercurial > hg > Members > kono > Proof > category

changeset 1079:d07cfce03236

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 Wed, 12 May 2021 00:42:14 +0900
parents 5aa36440e6fe
children c61639f34e7b
files src/Polynominal.agda
diffstat 1 files changed, 58 insertions(+), 25 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Tue May 11 22:59:27 2021 +0900
+++ b/src/Polynominal.agda	Wed May 12 00:42:14 2021 +0900
@@ -75,29 +75,6 @@
   --   all other cases, arguments are reduced to f ∙ π' .
   --postulate
      -- x-singleon : {a b c : Obj A}  → (f :  Poly a c b ) → (x y : Hom A b a) → x ≡ y  -- minimul equivalende assumption (variables are the same except its name)
-  k-cong : {a b c : Obj A}  → (f g :  Poly a c b )
-        → Poly.x f ≡ Poly.x g 
-        → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f)   ≈ k (Poly.x g) (Poly.phi g) ]
-  k-cong {a} {b} {c} f g refl f=f with Poly.x f | (Poly.phi f) |  (Poly.phi g)
-  ... | x | i {_} {_} {f'} | i = resp refl-hom f=f
-  ... | x | i {_} {_} {f'} | ii = {!!}
-  ... | x | i {_} {_} {h} | iii {_} {_} {_} {f₁} {g₁} t t₁ = begin
-     k x {h} i ≈⟨⟩
-     h ∙ π' ≈⟨ car f=f ⟩
-     < f₁ , g₁ > ∙ π' ≈⟨  IsCCC.distr-π isCCC ⟩
-     <  f₁ ∙ π'   , g₁ ∙ π'  > ≈⟨⟩
-     <  k x {f₁} i    , k x {g₁} i  > ≈⟨ IsCCC.π-cong isCCC (k-cong _ _ refl {!!} ) {!!} ⟩
-     < k x t , k x t₁ > ≈⟨⟩
-     k x (iii t t₁) ∎
-  ... | x | i {_} {_} {f'} | iv t t₁ = {!!}
-  ... | x | i {_} {_} {f'} | v t = {!!}
-  ... | x | i {_} {_} {f'} | φ-cong x₁ t = {!!}
-  ... | _ | ii | t = {!!}
-  ... | x | iii s s₁ | t = {!!}
-  ... | x | iv s s₁ | t = {!!}
-  ... | x | v s | t = {!!}
-  ... | x | φ-cong x₁ s | t = {!!}
-
   -- we may prove k-cong from x-singleon
   -- k-cong' : {a b c : Obj A}  → (f g :  Poly a c b ) → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f)   ≈ k (Poly.x g) (Poly.phi g) ]
   -- k-cong' {a} {b} {c} f g f=g with Poly.phi f | Poly.phi g
@@ -138,6 +115,10 @@
   *-cong = IsCCC.*-cong isCCC
   distr-* = IsCCC.distr-* isCCC
   e2 = IsCCC.e2 isCCC
+  idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a  ≈ id1 A a
+  idx {a} {x} = begin
+      x ∙ ○ a ≈⟨ {!!} ⟩
+      id1 A a ∎
 
   -- proof in p.59 Lambek
   functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p 
@@ -201,13 +182,36 @@
         --
         --   f ∙ <  x ∙ ○ b  , id1 A b >  ≈ f →  f ≈ k x (phi p)
         -- 
+        ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp  :  φ x {b} {c} f ) → A [ f ∙  π' ≈ k x fp ]
+        ki x f i = refl-hom
+        ki {a} x .x ii  = begin
+               x ∙ π'   ≈⟨ {!!} ⟩
+               x ∙ ○ (a ∧ １) ≈⟨ {!!} ⟩
+               x ∙ (○ a ∙ π )  ≈⟨ {!!} ⟩
+               (x ∙ ○ a ) ∙ π   ≈⟨ {!!} ⟩
+               id1 A a ∙ π   ≈⟨ {!!} ⟩
+               k x ii  ∎  
+        ki x .(< f₁  , f₂ > ) (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin
+               < f₁ ,  f₂  > ∙ π'  ≈⟨ IsCCC.distr-π isCCC ⟩
+               < f₁ ∙ π'  ,  f₂   ∙ π' >  ≈⟨ π-cong (ki x f₁ fp₁) (ki x f₂ fp₂) ⟩
+                k x (iii  fp₁ fp₂ )  ∎  
+        ki x .((A Category.o _) _) (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin
+               (f₁ ∙ f₂  ) ∙ π'  ≈⟨ {!!}  ⟩
+               f₁  ∙ ( f₂ ∙ π')  ≈⟨ {!!} ⟩
+               f₁  ∙ ( π'  ∙ < π , (f₂ ∙ π' )  >)  ≈⟨ {!!} ⟩
+               (f₁  ∙ π' ) ∙ < π , (f₂ ∙ π' )  >  ≈⟨ {!!} ⟩
+               k x fp ∙ < π , k x fp₁ >  ≈⟨⟩
+               k x (iv fp fp₁ )  ∎  
+        ki x .((C CCC.*) _) (v fp) = {!!}
+        ki x f (φ-cong x₁ fp) = {!!}
         uniq : {a b c : Obj A}  → (x :  Hom A １ a) (f :  Hom A b c) (phi  :  φ x {b} {c} f ) (f' : Hom A (a ∧ b) c) →
             A [  f' ∙ <  x ∙ ○ b  , id1 A b >  ≈ f ] → A [ f' ≈ k x phi ]
         uniq {a} {b} {c} x f phi  f' fx=p  = sym (begin
-               k x phi ≈↑⟨ k-cong record {x = x ; f = _ ; phi = i } record {x = x ; f = _ ; phi = phi } refl fx=p ⟩
+               k x phi ≈↑⟨ ki x f phi ⟩
+               k x {f} i ≈↑⟨ car fx=p ⟩
                k x {f' ∙ < x ∙ ○ b , id1 A b >} i ≈⟨ trans-hom (sym assoc)  (cdr (IsCCC.distr-π isCCC) ) ⟩ -- ( f' ∙ < x ∙ ○ b , id1 A b> ) ∙ π'
                f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii i i ) -- ( f' ∙ < (x ∙ ○ b) ∙ π'              , id1 A b ∙ π' > ) 
-                  ≈⟨ cdr (π-cong (k-cong record {x = x ; f = _ ; phi = i }  record {x = x ; f = _ ; phi = iv ii i } refl refl-hom ) refl-hom)  ⟩
+                  ≈⟨ cdr (π-cong (ki x ( x ∙ ○ b) (iv ii i) ) refl-hom)  ⟩
                f' ∙ < k x {x ∙ ○ b} (iv ii i ) , k x {id1 A b} i >   ≈⟨ refl-hom ⟩
                f' ∙ < k x {x} ii ∙ < π , k x {○ b} i >  , k x {id1 A b} i >   -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' >  , id1 A b ∙ π' > ) 
                    ≈⟨ cdr (π-cong (cdr (π-cong refl-hom (car e2))) idL ) ⟩ 
@@ -216,6 +220,35 @@
                f' ∙  id1 A _ ≈⟨ idR ⟩
                f' ∎  ) 
 
+  ki : {a b c : Obj A} → (x : Hom A １ a) → (f : Hom A b c ) → (fp  :  φ x {b} {c} f ) → A [ f ∙  π' ≈ k x fp ]
+  ki = {!!}
+  k-cong : {a b c : Obj A}  → (f g :  Poly a c b )
+        → Poly.x f ≡ Poly.x g 
+        → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f)   ≈ k (Poly.x g) (Poly.phi g) ]
+  k-cong {a} {b} {c} f g refl f=f = kcong (Poly.x f ) (Poly.f f) (Poly.f g) f=f ( Poly.phi f ) ( Poly.phi g) where
+     kcong : {a b c : Obj A} → (x : Hom A １ a) → (f g : Hom A b c ) → (f=g : f ≈ g ) → (fp  :  φ x {b} {c} f )( gp :  φ x {b} {c} g ) → A [ k x fp  ≈ k x gp ]
+     kcong {a} {b} {c} x f g f=g i i = resp refl-hom f=g
+     kcong {a} {.(CCC.１ C)} {.a} x f .x f=g i ii = begin
+          k x {f} i ≈⟨⟩
+          f ∙ π' ≈⟨ car f=g ⟩
+          x ∙ π' ≈⟨ ki x x ii ⟩
+          k x ii ∎   
+     kcong {a} {b} {.((C CCC.∧ _) _)} x f .(< g₁ , g₂ >)  f=g i (iii {_} {_} {_} {g₁} {g₂} gp₁ gp₂) = begin
+          k x i ≈⟨ car f=g ⟩
+          < g₁ , g₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩
+          < g₁ ∙ π' , g₂ ∙ π' >  ≈⟨ IsCCC.π-cong isCCC (ki x _ gp₁ ) (ki x _ gp₂) ⟩
+          < k x gp₁  , k x gp₂  >  ≈⟨⟩
+          k x (iii gp₁ gp₂) ∎   
+     kcong {a} {b} {c} x f .((A Category.o _) _) f=g i (iv gp gp₁) = {!!}
+     kcong {a} {b} {.((C CCC.<= _) _)} x f .((C CCC.*) _) f=g i (v gp) = {!!}
+     kcong {a} {b} {c} x f g f=g i (φ-cong x₁ gp) = {!!}
+     kcong {a} {.(CCC.１ C)} {.a} x .x g f=g ii gp = {!!}
+     kcong {a} {b} {.((C CCC.∧ _) _)} x .(CCC.< C , _ > _) g f=g (iii fp fp₁) gp = {!!}
+     kcong {a} {b} {c} x .((A Category.o _) _) g f=g (iv fp fp₁) gp = {!!}
+     kcong {a} {b} {.((C CCC.<= _) _)} x .((C CCC.*) _) g f=g (v fp) gp = {!!}
+     kcong {a} {b} {c} x f g f=g (φ-cong x₁ fp) gp = {!!}
+
+
   -- functional completeness ε form
   --
   --  g : Hom A １ (b <= a)       fun : Hom A (a ∧ １) c