--- a/src/Polynominal.agda	Sun Apr 18 20:45:44 2021 +0900
+++ b/src/Polynominal.agda	Mon Apr 19 04:49:28 2021 +0900
@@ -93,16 +93,27 @@
       isUnique : (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , Poly.x φ  > ]  ≈  Poly.f φ  ]
         →  A [ g   ≈ f ]
 
+  π-cong = IsCCC.π-cong isCCC
+  *-cong = IsCCC.*-cong isCCC
+  e2 = IsCCC.e2 isCCC
+
   -- functional completeness
   FC : {a b : Obj A}  → (φ  : Poly a b １ )  → Fc {a} {b} φ 
   FC {a} {b} φ = record {
      sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ ,  ○ a  > ] 
-     ; isSelect = {!!} 
+     ; 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 φ) * ) ∙ π ) , π' >   ∙ <  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 １ >  ≈⟨ {!!} ⟩
+        Poly.f φ ∎
      ; isUnique = {!!} 
-    } 
+    }  where
+        fc0 :  {b c : Obj A} (p : Poly b c １) → A [  k (Poly.x p ) (Poly.phi p) ∙ <  Poly.x p  ∙  ○ １  , id1 A １ >  ≈ Poly.f p ]
+        fc0 = {!!}
 
-  π-cong = IsCCC.π-cong isCCC
-  e2 = IsCCC.e2 isCCC
   -- {-# TERMINATING #-}
   functional-completeness : {a : Obj A} ( x : Hom A １ a ) → Functional-completeness  x 
   functional-completeness {a} x = record {