# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1620741567 -32400
# Node ID 5aa36440e6fe79647901b103ad320b09b10cf8b0
# Parent  918319d070b096538446bdb970c3512741ee7ba4
...

diff -r 918319d070b0 -r 5aa36440e6fe src/Polynominal.agda
--- a/src/Polynominal.agda	Mon May 10 16:24:03 2021 +0900
+++ b/src/Polynominal.agda	Tue May 11 22:59:27 2021 +0900
@@ -73,9 +73,30 @@
   --   case i i is π ∙ f ≈ π ∙ g
   --   we have (x y :  Hom A １ a) → x ≡ y (minimul equivalende assumption). this makes all k x ii case valid
   --   all other cases, arguments are reduced to f ∙ π' .
-  postulate
+  --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 ) → 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 : 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) ]
@@ -154,7 +175,7 @@
              k x y ∙ ( < (x ∙ ○ d) ∙ g  , id1 A d ∙ g > ) ≈↑⟨ cdr (IsCCC.distr-π isCCC) ⟩
              k x y ∙ ( < x ∙ ○ d ,  id1 A d > ∙ g ) ≈⟨ assoc ⟩
              (k x y ∙  < x ∙ ○ d ,  id1 A d > ) ∙ g  ≈⟨ car (fc0 x f y ) ⟩
-             f ∙ g  ∎  
+             f ∙ g  ∎   
         ... | v {_} {_} {_} {f} y = begin
             ( (k x y ∙ < π ∙ π , <  π' ∙  π , π' > >) *) ∙ < x ∙ (○ b) , id1 A b > ≈⟨ IsCCC.distr-* isCCC ⟩
             ( (k x y ∙ < π ∙ π , <  π' ∙  π , π' > >) ∙ < < x ∙ ○ b , id1 A _ > ∙ π , π' > ) * ≈⟨  IsCCC.*-cong isCCC ( begin
@@ -183,17 +204,17 @@
         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 = phi }  record { x = x ; f = _ ; phi = i }  (sym fx=p) ⟩
+               k x phi ≈↑⟨ k-cong record {x = x ; f = _ ; phi = i } record {x = x ; f = _ ; phi = phi } refl 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-hom ) refl-hom)  ⟩
+                  ≈⟨ cdr (π-cong (k-cong record {x = x ; f = _ ; phi = i }  record {x = x ; f = _ ; phi = iv ii i } refl refl-hom ) 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 ) ⟩ 
                f' ∙  <  π ∙ < π , (○ b ∙ π' ) >  , π' >   ≈⟨ cdr (π-cong (IsCCC.e3a isCCC)  refl-hom) ⟩
                f' ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
                f' ∙  id1 A _ ≈⟨ idR ⟩
-               f' ∎  )  
+               f' ∎  ) 
 
   -- functional completeness ε form
   --