--- a/src/Polynominal.agda	Sun May 16 13:46:39 2021 +0900
+++ b/src/Polynominal.agda	Sun May 16 22:01:28 2021 +0900
@@ -234,10 +234,15 @@
                f' ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
                f' ∙  id1 A _ ≈⟨ idR ⟩
                f' ∎  )  where
-                   xf :  (fp : φ x (x ∙ ○ b)) → xnef x fp
-                   xf = {!!}
+                   --  (phi : φ x f) → xnef x phi
+                   xf :  (g : Hom A b a) → (fp : φ x g) → g ≅ (x ∙ ○ b) → xnef x fp
+                   xf .((A Category.o x) (CCC.○ C b)) (i .((A Category.o x) (CCC.○ C b))) _≅_.refl = {!!} -- x ≅ x ∙ (○ b) → ⊥
+                   xf g ii eq = lift tt
+                   xf g (iii fp fp₁) eq = {!!}
+                   xf g (iv fp fp₁) eq = {!!}
+                   xf g (v fp) eq = {!!}
                    u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) > 
-                   u2 = ki x (x ∙ ○ b) (iv ii (i _)) xf
+                   u2 = ki x (x ∙ ○ b) (iv ii (i _)) (λ gp  → xf (x ∙ ○ b) gp HE.refl )
 
   -- functional completeness ε form
   --