--- a/src/Polynominal.agda	Mon Apr 19 04:49:28 2021 +0900
+++ b/src/Polynominal.agda	Mon Apr 19 05:21:41 2021 +0900
@@ -102,12 +102,12 @@
   FC {a} {b} φ = record {
      sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ ,  ○ a  > ] 
      ; isSelect = begin
-        ε ∙ <  (( ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ π ) ∙ < id1 A a , ○ a > ) ∙ π')  * ,  Poly.x φ  > ≈↑⟨ cdr (π-cong (*-cong assoc)  refl-hom) ⟩
-        ε ∙ < (((k (Poly.x φ) (Poly.phi φ) ∙ < id1  A _ , ○ a >) ∙ π) ∙ (< id1  A _ , ○ a > ∙ π' )) * , Poly.x φ > ≈⟨ {!!} ⟩
-        ε ∙ <  ( (k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ {!!} )  * ,  Poly.x φ  > ≈⟨ {!!} ⟩
+        ε ∙ <  (( ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ π ) ∙ < id1 A a , ○ a > ) ∙ π')  * ,  Poly.x φ  > ≈↑⟨ cdr (π-cong (*-cong (car assoc))  refl-hom) ⟩
+        ε ∙ < (((k (Poly.x φ) (Poly.phi φ) ∙ < id1  A _ , ○ a >) ∙ (π ∙ (< id1  A _ , ○ a >))) ∙ π' ) * , Poly.x φ > ≈⟨ {!!} ⟩
+        ε ∙ <  ( (k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ (id1 A _ ∙ π' ) )  * ,  Poly.x φ  > ≈⟨ {!!} ⟩
         ε ∙ ( < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' >   ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ > ) ≈⟨ assoc ⟩ 
         (ε ∙ < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' >  ) ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ > ≈⟨ car ( IsCCC.e4a isCCC ) ⟩ 
-        k (Poly.x φ ) (Poly.phi φ) ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ >  ≈⟨ {!!} ⟩
+        k (Poly.x φ ) (Poly.phi φ) ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ >  ≈⟨ fc0 φ  ⟩
         Poly.f φ ∎
      ; isUnique = {!!} 
     }  where
@@ -192,16 +192,7 @@
               f ∙  id1 A _ ≈⟨ idR ⟩
               f ∎  ) where
           fc1 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p)  ≈ k x {hom p} i ]    -- it looks like (*) in page 60
-          fc1 {b} {c} p with phi p
-          ... | i = refl-hom
-          ... | ii = {!!}  -- it doesn't look good
-          ... | iii t t₁ = {!!}
-          ... | iv t t₁ = {!!}
-          ... | v t = {!!}
-          ... | φ-cong x t = {!!}
-          -- fc1 {b} {c} p = uniq record { hom =  hom p ; phi = i }  ( k x (phi p)) ( begin -- non terminating because of the record, which we may avoid
-          --      k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈⟨ fc0 p ⟩
-          --      hom p ∎  )
+          fc1 {b} {c} p = {!!}
         
 
 -- end