# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1618841537 -32400
# Node ID 79e7e0367189665b58b87f6deb103bfb48e393bf
# Parent  88f441d5bb18975c0d21b87f680106d88fb8f022
...

diff -r 88f441d5bb18 -r 79e7e0367189 src/Polynominal.agda
--- a/src/Polynominal.agda	Mon Apr 19 17:42:59 2021 +0900
+++ b/src/Polynominal.agda	Mon Apr 19 23:12:17 2021 +0900
@@ -152,17 +152,18 @@
         --
         --   f ∙ <  x ∙ ○ b  , id1 A b >  ≈ f →  f ≈ k x (phi p)
         -- 
-        k-cong : {a b c : Obj A}  → (x :  Hom A １ a) → (f g :  Hom A b c ) → A [ f ≈ g ] →  (fp : φ x {b} {c} f ) (gp :   φ x {b} {c} g )
-           → A [ k x fp   ≈ k x gp ]
-        k-cong = {!!}
+        -- why  k x {x ∙ ○ b} (iv ii i ) ≡  k x {x ∙ ○ b} i?
+        --   if A is locally small, it is ≡-cong.
+        postulate
+           k-cong : {a b c : Obj A}  → (x :  Hom A １ a) → (f g :  Hom A b c ) → A [ f ≈ g ] →  (fp : φ x {b} {c} f ) (gp :   φ x {b} {c} g )
+             → A [ k x fp   ≈ k x gp ]
         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 ≈⟨ uniq x (f ∙ < x ∙ ○ b , id1 A b > ) i (k x phi) {!!} ⟩
                k x phi ≈⟨ k-cong x _ _ (sym fx=p)  phi i ⟩
                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 {!!} refl-hom ) ⟩ 
+               f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii i i ) -- ( f' ∙ < (x ∙ ○ b) ∙ π'              , id1 A b ∙ π' > ) 
+                  ≈⟨ cdr (π-cong (k-cong x (x ∙ ○ b) (x ∙ ○ b) refl-hom i (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 ) ⟩