--- a/src/Polynominal.agda	Mon Apr 19 16:05:52 2021 +0900
+++ b/src/Polynominal.agda	Mon Apr 19 17:42:59 2021 +0900
@@ -162,7 +162,8 @@
                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 (trans-hom (IsCCC.e3a isCCC)  k x {< x ∙ ○ b , id1 A b >} (iii i i ){!!}) refl-hom ) ⟩ 
+                   ≈↑⟨ cdr (π-cong {!!} 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) ⟩